Metamath Proof Explorer

Theorem alephord2

Description: Ordering property of the aleph function. Theorem 8A(a) of Enderton p. 213 and its converse. (Contributed by NM, 3-Nov-2003) (Revised by Mario Carneiro, 9-Feb-2013)

Ref Expression
Assertion alephord2 
|- ( ( A e. On /\ B e. On ) -> ( A e. B <-> ( aleph ` A ) e. ( aleph ` B ) ) )

Proof

Step Hyp Ref Expression
1 alephord 
 |-  ( ( A e. On /\ B e. On ) -> ( A e. B <-> ( aleph ` A ) ~< ( aleph ` B ) ) )
2 alephon 
 |-  ( aleph ` A ) e. On
3 alephon 
 |-  ( aleph ` B ) e. On
4 onenon 
 |-  ( ( aleph ` B ) e. On -> ( aleph ` B ) e. dom card )
5 3 4 ax-mp 
 |-  ( aleph ` B ) e. dom card
6 cardsdomel 
 |-  ( ( ( aleph ` A ) e. On /\ ( aleph ` B ) e. dom card ) -> ( ( aleph ` A ) ~< ( aleph ` B ) <-> ( aleph ` A ) e. ( card ` ( aleph ` B ) ) ) )
7 2 5 6 mp2an 
 |-  ( ( aleph ` A ) ~< ( aleph ` B ) <-> ( aleph ` A ) e. ( card ` ( aleph ` B ) ) )
8 alephcard 
 |-  ( card ` ( aleph ` B ) ) = ( aleph ` B )
9 8 eleq2i 
 |-  ( ( aleph ` A ) e. ( card ` ( aleph ` B ) ) <-> ( aleph ` A ) e. ( aleph ` B ) )
10 7 9 bitri 
 |-  ( ( aleph ` A ) ~< ( aleph ` B ) <-> ( aleph ` A ) e. ( aleph ` B ) )
11 1 10 bitrdi 
 |-  ( ( A e. On /\ B e. On ) -> ( A e. B <-> ( aleph ` A ) e. ( aleph ` B ) ) )