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