Metamath Proof Explorer


Theorem alephf1ALT

Description: Alternate proof of alephf1 . (Contributed by Mario Carneiro, 15-Mar-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion alephf1ALT
|- aleph : On -1-1-> On

Proof

Step Hyp Ref Expression
1 alephfnon
 |-  aleph Fn On
2 alephon
 |-  ( aleph ` x ) e. On
3 2 a1i
 |-  ( x e. On -> ( aleph ` x ) e. On )
4 3 rgen
 |-  A. x e. On ( aleph ` x ) e. On
5 ffnfv
 |-  ( aleph : On --> On <-> ( aleph Fn On /\ A. x e. On ( aleph ` x ) e. On ) )
6 1 4 5 mpbir2an
 |-  aleph : On --> On
7 alephsmo
 |-  Smo aleph
8 smo11
 |-  ( ( aleph : On --> On /\ Smo aleph ) -> aleph : On -1-1-> On )
9 6 7 8 mp2an
 |-  aleph : On -1-1-> On