This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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