Metamath Proof Explorer

Theorem alephord

Description: Ordering property of the aleph function. (Contributed by NM, 26-Oct-2003) (Revised by Mario Carneiro, 9-Feb-2013)

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

Proof

Step Hyp Ref Expression
1 alephordi 
 |-  ( B e. On -> ( A e. B -> ( aleph ` A ) ~< ( aleph ` B ) ) )
2 1 adantl 
 |-  ( ( A e. On /\ B e. On ) -> ( A e. B -> ( aleph ` A ) ~< ( aleph ` B ) ) )
3 brsdom 
 |-  ( ( aleph ` A ) ~< ( aleph ` B ) <-> ( ( aleph ` A ) ~<_ ( aleph ` B ) /\ -. ( aleph ` A ) ~~ ( aleph ` B ) ) )
4 alephon 
 |-  ( aleph ` A ) e. On
5 alephon 
 |-  ( aleph ` B ) e. On
6 domtriord 
 |-  ( ( ( aleph ` A ) e. On /\ ( aleph ` B ) e. On ) -> ( ( aleph ` A ) ~<_ ( aleph ` B ) <-> -. ( aleph ` B ) ~< ( aleph ` A ) ) )
7 4 5 6 mp2an 
 |-  ( ( aleph ` A ) ~<_ ( aleph ` B ) <-> -. ( aleph ` B ) ~< ( aleph ` A ) )
8 alephordi 
 |-  ( A e. On -> ( B e. A -> ( aleph ` B ) ~< ( aleph ` A ) ) )
9 8 con3d 
 |-  ( A e. On -> ( -. ( aleph ` B ) ~< ( aleph ` A ) -> -. B e. A ) )
10 7 9 syl5bi 
 |-  ( A e. On -> ( ( aleph ` A ) ~<_ ( aleph ` B ) -> -. B e. A ) )
11 10 adantr 
 |-  ( ( A e. On /\ B e. On ) -> ( ( aleph ` A ) ~<_ ( aleph ` B ) -> -. B e. A ) )
12 ontri1 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B <-> -. B e. A ) )
13 11 12 sylibrd 
 |-  ( ( A e. On /\ B e. On ) -> ( ( aleph ` A ) ~<_ ( aleph ` B ) -> A C_ B ) )
14 fveq2 
 |-  ( A = B -> ( aleph ` A ) = ( aleph ` B ) )
15 eqeng 
 |-  ( ( aleph ` A ) e. On -> ( ( aleph ` A ) = ( aleph ` B ) -> ( aleph ` A ) ~~ ( aleph ` B ) ) )
16 4 14 15 mpsyl 
 |-  ( A = B -> ( aleph ` A ) ~~ ( aleph ` B ) )
17 16 necon3bi 
 |-  ( -. ( aleph ` A ) ~~ ( aleph ` B ) -> A =/= B )
18 13 17 anim12d1 
 |-  ( ( A e. On /\ B e. On ) -> ( ( ( aleph ` A ) ~<_ ( aleph ` B ) /\ -. ( aleph ` A ) ~~ ( aleph ` B ) ) -> ( A C_ B /\ A =/= B ) ) )
19 onelpss 
 |-  ( ( A e. On /\ B e. On ) -> ( A e. B <-> ( A C_ B /\ A =/= B ) ) )
20 18 19 sylibrd 
 |-  ( ( A e. On /\ B e. On ) -> ( ( ( aleph ` A ) ~<_ ( aleph ` B ) /\ -. ( aleph ` A ) ~~ ( aleph ` B ) ) -> A e. B ) )
21 3 20 syl5bi 
 |-  ( ( A e. On /\ B e. On ) -> ( ( aleph ` A ) ~< ( aleph ` B ) -> A e. B ) )
22 2 21 impbid 
 |-  ( ( A e. On /\ B e. On ) -> ( A e. B <-> ( aleph ` A ) ~< ( aleph ` B ) ) )