Metamath Proof Explorer

Theorem alephord3

Description: Ordering property of the aleph function. (Contributed by NM, 11-Nov-2003)

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

Proof

Step Hyp Ref Expression
1 alephord2 
 |-  ( ( B e. On /\ A e. On ) -> ( B e. A <-> ( aleph ` B ) e. ( aleph ` A ) ) )
2 1 ancoms 
 |-  ( ( A e. On /\ B e. On ) -> ( B e. A <-> ( aleph ` B ) e. ( aleph ` A ) ) )
3 2 notbid 
 |-  ( ( A e. On /\ B e. On ) -> ( -. B e. A <-> -. ( aleph ` B ) e. ( aleph ` A ) ) )
4 ontri1 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B <-> -. B e. A ) )
5 alephon 
 |-  ( aleph ` A ) e. On
6 alephon 
 |-  ( aleph ` B ) e. On
7 ontri1 
 |-  ( ( ( aleph ` A ) e. On /\ ( aleph ` B ) e. On ) -> ( ( aleph ` A ) C_ ( aleph ` B ) <-> -. ( aleph ` B ) e. ( aleph ` A ) ) )
8 5 6 7 mp2an 
 |-  ( ( aleph ` A ) C_ ( aleph ` B ) <-> -. ( aleph ` B ) e. ( aleph ` A ) )
9 8 a1i 
 |-  ( ( A e. On /\ B e. On ) -> ( ( aleph ` A ) C_ ( aleph ` B ) <-> -. ( aleph ` B ) e. ( aleph ` A ) ) )
10 3 4 9 3bitr4d 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B <-> ( aleph ` A ) C_ ( aleph ` B ) ) )