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 : On -1-1-> On

Proof

Step	Hyp	Ref	Expression
1		alephfnon	|- aleph Fn On
2		alephon	|- ( aleph ` x ) e. On
3	2	rgenw	|- A. x e. On ( aleph ` x ) e. On
4		ffnfv	|- ( aleph : On --> On <-> ( aleph Fn On /\ A. x e. On ( aleph ` x ) e. On ) )
5	1 3 4	mpbir2an	|- aleph : On --> On
6		aleph11	|- ( ( x e. On /\ y e. On ) -> ( ( aleph ` x ) = ( aleph ` y ) <-> x = y ) )
7	6	biimpd	|- ( ( x e. On /\ y e. On ) -> ( ( aleph ` x ) = ( aleph ` y ) -> x = y ) )
8	7	rgen2	|- A. x e. On A. y e. On ( ( aleph ` x ) = ( aleph ` y ) -> x = y )
9		dff13	|- ( aleph : On -1-1-> On <-> ( aleph : On --> On /\ A. x e. On A. y e. On ( ( aleph ` x ) = ( aleph ` y ) -> x = y ) ) )
10	5 8 9	mpbir2an	|- aleph : On -1-1-> On