View source for Every injection yields a bijection onto its image

{{Stub page|grade=B|msg=Make sure this page is up to scratch before removing this. It should be pretty good; it'd be wrong to not mark it as a stub when it was made simply to be linked to}}
__TOC__
==Statement==
<m>\newcommand{\f}{\overline{f}}</m>Let {{M|X}} and {{M|Y}} be [[sets]] and suppose {{M|f:X\rightarrow Y}} is any ''[[injective]]'' [[map]] between them. Then we claim that there is a map:
* {{M|\overline{f}:X\rightarrow f(X)}} given by {{M|\overline{f}:x\mapsto f(x)}}- where {{M|f(X)}} denotes the {{link|image|map}} of {{M|X}} under {{M|f}}<ref name="imageDef" group="Note" /><!--body of note declared in note references tag -->
that is a [[bijection]] between {{M|X}} and {{M|f(X)}} (that is to say, we claim that {{M|\f}} is a bijection, a bijection is any map that is both [[injective]] and [[surjective]])
==Proof==
We must show that {{M|\f:X\rightarrow f(X)}} is a [[bijection]] (that means {{M|\f}} is both [[injective]] and [[surjective]]), even though injectiveness is (even more than surjectiveness) trivial, we do it anyway. That's why this page is marked as [[:Category:First-year friendly|first-year friendly]]
# [[Injection|Injectivity]] of {{M|\f:X\rightarrow f(X)}} given by {{M|\f:x\mapsto f(x)}}
#* We will take injectivity to mean: {{M|1=\forall x_1,x_2\in X[\f(x_1)=\f(x_2)\implies x_1=x_2]}} (rather than other equivalent conditions documented on the [[injection]] page)
#* Let {{M|x_1,x_2\in X}} be given
#** Suppose {{M|1=\f(x_1)\ne\f(x_2)}}
#*** By the nature of [[logical implication]] we do not care if the RHS ({{M|1=x_1=x_2}}) is true or false.
#**** By the [[principle of excluded middle]] {{M|1=x_1=x_2}} must be true [[xor]] false<ref group="Note">Xor means "exclusive or", {{M|A\text{ XOR }B}} means {{M|A}} or {{M|B}} is true ''and'' {{M|A\text{ AND }B}} is false. That is to say we have {{M|A}} or {{M|B}} but not both</ref>, so we're done in either case.
#** Suppose {{M|1=\f(x_1)=\f(x_2)}}
#*** In order for the [[implication]] to be true, we require that this means {{M|1=x_1=x_2}}
#*** Notice that {{M|1=\f(x_1)=f(x_1)}} and {{M|1=\f(x_2)=f(x_2)}} (by definition of {{M|\f}})
#*** As {{M|f:X\rightarrow Y}} was injective itself, this means:
#**** {{M|1=\forall x_1,x_2\in X[\f(x_1)=\f(x_2)\implies x_1=x_2]}}
#*** By hypothesis, {{M|1=\f(x_1)=\f(x_2)}} so {{M|1=f(x_1)=f(x_2)}} 
#**** This means that {{M|1=x_1=x_2}} by injectivity of {{M|f}}
#*** So {{M|1=\f(x_1)=\f(x_2)\implies f(x_1)=f(x_2)\implies x_1=x_2}} (then by [[transitivity of implies]] {{M|1=\f(x_1)=\f(x_2)\implies x_1=x_2}})
#**** We know {{M|1=\f(x_1)=\f(x_2)}} to be true, therefore, by definition of [[implies]] and by knowing  {{M|1=\f(x_1)=\f(x_2)\implies x_1=x_2}} we must have:
#***** {{M|1=x_1=x_2}}
#** This completes the first part of the proof
# [[Surjection|Surjectivity]] of {{M|\f:X\rightarrow f(X)}} given by {{M|\f:x\mapsto f(x)}}
#* To be [[surjective]] we require: {{M|1=\forall y\in f(X)\exists x\in X[\f(x)=y]}}
#* Let {{M|y\in f(X)}} be given
#** By definition of {{M|1=f(X)}} (that is {{M|1=f(X):=\{y\in Y\ \vert\ \exists x\in X[f(x)=y]\} }} remember) we see:
#*** {{M|1=y\in f(X)\iff\exists x\in X[f(x)=y]}}
#** Choose {{M|x\in X}} such that {{M|1=f(x)=y}} (which we can do thanks to the above)
#*** Now {{M|1=\f(x)=f(x)}} by definition of {{M|\f}} and
#**** {{M|1=f(x)=y}} by our choice of {{M|x}}
#*** So {{M|1=\f(x)=f(x)=y}} or just {{M|1=\f(x)=y}}
#** We have shown there exists an {{M|x\in X}} such that {{M|1=\f(x)=y}} for our given {{M|y}}
#* Since {{M|y\in f(X)}} was arbitrary we have shown this for all {{M|y}}
#* That completes the surjectivity part of the proof
{{Todo|Check, I should have left this blank and marked it as low-hanging fruit.... }}
Thus we have shown that {{M|\f:X\rightarrow f(X)}} given by {{M|\f:x\mapsto f(x)}} is a [[bijection]]
==See also==
* [[Bijection]]
* [[Surjection]]
==Notes==
<references group="Note">
<ref group="Note" name="imageDef">Formally:
* for {{M|A\in\mathcal{P}(X)}} we define {{M|1=f(A):=\{y\in Y\ \vert\ \exists a\in A[f(a)=y]\} }}
So:
* {{M|1=f(X):=\{y\in Y\ \vert \exists x\in X[f(x)=y] \} }} - the set of all things in {{M|Y}} that are mapped to by {{M|f}} for some {{M|x\in X}}</ref>
</references>
==References==
<references/>
{{Function terminology navbox|plain}}
{{Definition|Set Theory|Elementary Set Theory}}[[Category:First-year friendly]]