Metamath Proof Explorer

Theorem alephord2i

Description: Ordering property of the aleph function. Theorem 66 of Suppes p. 229. (Contributed by NM, 25-Oct-2003)

Ref Expression
Assertion alephord2i 
|- ( B e. On -> ( A e. B -> ( aleph ` A ) e. ( aleph ` B ) ) )

Proof

Step Hyp Ref Expression
1 onelon 
 |-  ( ( B e. On /\ A e. B ) -> A e. On )
2 alephord2 
 |-  ( ( A e. On /\ B e. On ) -> ( A e. B <-> ( aleph ` A ) e. ( aleph ` B ) ) )
3 2 biimpd 
 |-  ( ( A e. On /\ B e. On ) -> ( A e. B -> ( aleph ` A ) e. ( aleph ` B ) ) )
4 3 expimpd 
 |-  ( A e. On -> ( ( B e. On /\ A e. B ) -> ( aleph ` A ) e. ( aleph ` B ) ) )
5 1 4 mpcom 
 |-  ( ( B e. On /\ A e. B ) -> ( aleph ` A ) e. ( aleph ` B ) )
6 5 ex 
 |-  ( B e. On -> ( A e. B -> ( aleph ` A ) e. ( aleph ` B ) ) )