Every injection yields a bijection onto its image
Contents
Statement
[ilmath]\newcommand{\f}{\overline{f}}[/ilmath]Let [ilmath]X[/ilmath] and [ilmath]Y[/ilmath] be sets and suppose [ilmath]f:X\rightarrow Y[/ilmath] is any injective map between them. Then we claim that there is a map:
 [ilmath]\overline{f}:X\rightarrow f(X)[/ilmath] given by [ilmath]\overline{f}:x\mapsto f(x)[/ilmath] where [ilmath]f(X)[/ilmath] denotes the image of [ilmath]X[/ilmath] under [ilmath]f[/ilmath]^{[Note 1]}
that is a bijection between [ilmath]X[/ilmath] and [ilmath]f(X)[/ilmath] (that is to say, we claim that [ilmath]\f[/ilmath] is a bijection, a bijection is any map that is both injective and surjective)
Proof
We must show that [ilmath]\f:X\rightarrow f(X)[/ilmath] is a bijection (that means [ilmath]\f[/ilmath] 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 firstyear friendly
 Injectivity of [ilmath]\f:X\rightarrow f(X)[/ilmath] given by [ilmath]\f:x\mapsto f(x)[/ilmath]
 We will take injectivity to mean: [ilmath]\forall x_1,x_2\in X[\f(x_1)=\f(x_2)\implies x_1=x_2][/ilmath] (rather than other equivalent conditions documented on the injection page)
 Let [ilmath]x_1,x_2\in X[/ilmath] be given
 Suppose [ilmath]\f(x_1)\ne\f(x_2)[/ilmath]
 By the nature of logical implication we do not care if the RHS ([ilmath]x_1=x_2[/ilmath]) is true or false.
 By the principle of excluded middle [ilmath]x_1=x_2[/ilmath] must be true xor false^{[Note 2]}, so we're done in either case.
 By the nature of logical implication we do not care if the RHS ([ilmath]x_1=x_2[/ilmath]) is true or false.
 Suppose [ilmath]\f(x_1)=\f(x_2)[/ilmath]
 In order for the implication to be true, we require that this means [ilmath]x_1=x_2[/ilmath]
 Notice that [ilmath]\f(x_1)=f(x_1)[/ilmath] and [ilmath]\f(x_2)=f(x_2)[/ilmath] (by definition of [ilmath]\f[/ilmath])
 As [ilmath]f:X\rightarrow Y[/ilmath] was injective itself, this means:
 [ilmath]\forall x_1,x_2\in X[\f(x_1)=\f(x_2)\implies x_1=x_2][/ilmath]
 By hypothesis, [ilmath]\f(x_1)=\f(x_2)[/ilmath] so [ilmath]f(x_1)=f(x_2)[/ilmath]
 This means that [ilmath]x_1=x_2[/ilmath] by injectivity of [ilmath]f[/ilmath]
 So [ilmath]\f(x_1)=\f(x_2)\implies f(x_1)=f(x_2)\implies x_1=x_2[/ilmath] (then by transitivity of implies [ilmath]\f(x_1)=\f(x_2)\implies x_1=x_2[/ilmath])
 We know [ilmath]\f(x_1)=\f(x_2)[/ilmath] to be true, therefore, by definition of implies and by knowing [ilmath]\f(x_1)=\f(x_2)\implies x_1=x_2[/ilmath] we must have:
 [ilmath]x_1=x_2[/ilmath]
 We know [ilmath]\f(x_1)=\f(x_2)[/ilmath] to be true, therefore, by definition of implies and by knowing [ilmath]\f(x_1)=\f(x_2)\implies x_1=x_2[/ilmath] we must have:
 This completes the first part of the proof
 Suppose [ilmath]\f(x_1)\ne\f(x_2)[/ilmath]
 Surjectivity of [ilmath]\f:X\rightarrow f(X)[/ilmath] given by [ilmath]\f:x\mapsto f(x)[/ilmath]
 To be surjective we require: [ilmath]\forall y\in f(X)\exists x\in X[\f(x)=y][/ilmath]
 Let [ilmath]y\in f(X)[/ilmath] be given
 By definition of [ilmath]f(X)[/ilmath] (that is [ilmath]f(X):=\{y\in Y\ \vert\ \exists x\in X[f(x)=y]\}[/ilmath] remember) we see:
 [ilmath]y\in f(X)\iff\exists x\in X[f(x)=y][/ilmath]
 Choose [ilmath]x\in X[/ilmath] such that [ilmath]f(x)=y[/ilmath] (which we can do thanks to the above)
 Now [ilmath]\f(x)=f(x)[/ilmath] by definition of [ilmath]\f[/ilmath] and
 [ilmath]f(x)=y[/ilmath] by our choice of [ilmath]x[/ilmath]
 So [ilmath]\f(x)=f(x)=y[/ilmath] or just [ilmath]\f(x)=y[/ilmath]
 Now [ilmath]\f(x)=f(x)[/ilmath] by definition of [ilmath]\f[/ilmath] and
 We have shown there exists an [ilmath]x\in X[/ilmath] such that [ilmath]\f(x)=y[/ilmath] for our given [ilmath]y[/ilmath]
 By definition of [ilmath]f(X)[/ilmath] (that is [ilmath]f(X):=\{y\in Y\ \vert\ \exists x\in X[f(x)=y]\}[/ilmath] remember) we see:
 Since [ilmath]y\in f(X)[/ilmath] was arbitrary we have shown this for all [ilmath]y[/ilmath]
 That completes the surjectivity part of the proof
TODO: Check, I should have left this blank and marked it as lowhanging fruit....
Thus we have shown that [ilmath]\f:X\rightarrow f(X)[/ilmath] given by [ilmath]\f:x\mapsto f(x)[/ilmath] is a bijection
See also
Notes
 ↑ Formally:
 for [ilmath]A\in\mathcal{P}(X)[/ilmath] we define [ilmath]f(A):=\{y\in Y\ \vert\ \exists a\in A[f(a)=y]\}[/ilmath]
 [ilmath]f(X):=\{y\in Y\ \vert \exists x\in X[f(x)=y] \}[/ilmath]  the set of all things in [ilmath]Y[/ilmath] that are mapped to by [ilmath]f[/ilmath] for some [ilmath]x\in X[/ilmath]
 ↑ Xor means "exclusive or", [ilmath]A\text{ XOR }B[/ilmath] means [ilmath]A[/ilmath] or [ilmath]B[/ilmath] is true and [ilmath]A\text{ AND }B[/ilmath] is false. That is to say we have [ilmath]A[/ilmath] or [ilmath]B[/ilmath] but not both
References
