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 ) ) )