Metamath Proof Explorer

Theorem alephsmo

Description: The aleph function is strictly monotone. (Contributed by Mario Carneiro, 15-Mar-2013)

Ref Expression
Assertion alephsmo 
|- Smo aleph

Proof

Step Hyp Ref Expression
1 ssid 
 |-  On C_ On
2 ordon 
 |-  Ord On
3 alephord2i 
 |-  ( x e. On -> ( y e. x -> ( aleph ` y ) e. ( aleph ` x ) ) )
4 3 ralrimiv 
 |-  ( x e. On -> A. y e. x ( aleph ` y ) e. ( aleph ` x ) )
5 4 rgen 
 |-  A. x e. On A. y e. x ( aleph ` y ) e. ( aleph ` x )
6 alephfnon 
 |-  aleph Fn On
7 alephsson 
 |-  ran aleph C_ On
8 df-f 
 |-  ( aleph : On --> On <-> ( aleph Fn On /\ ran aleph C_ On ) )
9 6 7 8 mpbir2an 
 |-  aleph : On --> On
10 issmo2 
 |-  ( aleph : On --> On -> ( ( On C_ On /\ Ord On /\ A. x e. On A. y e. x ( aleph ` y ) e. ( aleph ` x ) ) -> Smo aleph ) )
11 9 10 ax-mp 
 |-  ( ( On C_ On /\ Ord On /\ A. x e. On A. y e. x ( aleph ` y ) e. ( aleph ` x ) ) -> Smo aleph )
12 1 2 5 11 mp3an 
 |-  Smo aleph