Theorem alephf1

Description: The aleph function is a one-to-one mapping from the ordinals to the infinite cardinals. See also alephf1ALT . (Contributed by Mario Carneiro, 2-Feb-2013)

	Ref	Expression
Assertion	alephf1	$$⊢\aleph :\mathrm{On}\underset{1-1}{⟶}\mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		alephfnon	$$⊢\aleph Fn\mathrm{On}$$
2		alephon	$$⊢\aleph \left(x\right)\in \mathrm{On}$$
3	2	rgenw	$$⊢\forall x\in \mathrm{On}\aleph \left(x\right)\in \mathrm{On}$$
4		ffnfv	$$⊢\aleph :\mathrm{On}⟶\mathrm{On}\leftrightarrow \left(\aleph Fn\mathrm{On}\wedge \forall x\in \mathrm{On}\aleph \left(x\right)\in \mathrm{On}\right)$$
5	1 3 4	mpbir2an	$$⊢\aleph :\mathrm{On}⟶\mathrm{On}$$
6		aleph11	$$⊢\left(x\in \mathrm{On}\wedge y\in \mathrm{On}\right)\to \left(\aleph \left(x\right)=\aleph \left(y\right)\leftrightarrow x=y\right)$$
7	6	biimpd	$$⊢\left(x\in \mathrm{On}\wedge y\in \mathrm{On}\right)\to \left(\aleph \left(x\right)=\aleph \left(y\right)\to x=y\right)$$
8	7	rgen2	$$⊢\forall x\in \mathrm{On}\forall y\in \mathrm{On}\left(\aleph \left(x\right)=\aleph \left(y\right)\to x=y\right)$$
9		dff13	$$⊢\aleph :\mathrm{On}\underset{1-1}{⟶}\mathrm{On}\leftrightarrow \left(\aleph :\mathrm{On}⟶\mathrm{On}\wedge \forall x\in \mathrm{On}\forall y\in \mathrm{On}\left(\aleph \left(x\right)=\aleph \left(y\right)\to x=y\right)\right)$$
10	5 8 9	mpbir2an	$$⊢\aleph :\mathrm{On}\underset{1-1}{⟶}\mathrm{On}$$