This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem alephdom

Description: Relationship between inclusion of ordinal numbers and dominance of infinite initial ordinals. (Contributed by Jeff Hankins, 23-Oct-2009)

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

Proof

Step Hyp Ref Expression
1 onsseleq 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B <-> ( A e. B \/ A = B ) ) )
2 alephord 
 |-  ( ( A e. On /\ B e. On ) -> ( A e. B <-> ( aleph ` A ) ~< ( aleph ` B ) ) )
3 sdomdom 
 |-  ( ( aleph ` A ) ~< ( aleph ` B ) -> ( aleph ` A ) ~<_ ( aleph ` B ) )
4 2 3 biimtrdi 
 |-  ( ( A e. On /\ B e. On ) -> ( A e. B -> ( aleph ` A ) ~<_ ( aleph ` B ) ) )
5 fvex 
 |-  ( aleph ` A ) e. _V
6 fveq2 
 |-  ( A = B -> ( aleph ` A ) = ( aleph ` B ) )
7 eqeng 
 |-  ( ( aleph ` A ) e. _V -> ( ( aleph ` A ) = ( aleph ` B ) -> ( aleph ` A ) ~~ ( aleph ` B ) ) )
8 5 6 7 mpsyl 
 |-  ( A = B -> ( aleph ` A ) ~~ ( aleph ` B ) )
9 8 a1i 
 |-  ( ( A e. On /\ B e. On ) -> ( A = B -> ( aleph ` A ) ~~ ( aleph ` B ) ) )
10 endom 
 |-  ( ( aleph ` A ) ~~ ( aleph ` B ) -> ( aleph ` A ) ~<_ ( aleph ` B ) )
11 9 10 syl6 
 |-  ( ( A e. On /\ B e. On ) -> ( A = B -> ( aleph ` A ) ~<_ ( aleph ` B ) ) )
12 4 11 jaod 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A e. B \/ A = B ) -> ( aleph ` A ) ~<_ ( aleph ` B ) ) )
13 1 12 sylbid 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( aleph ` A ) ~<_ ( aleph ` B ) ) )
14 eloni 
 |-  ( B e. On -> Ord B )
15 eloni 
 |-  ( A e. On -> Ord A )
16 ordtri2or 
 |-  ( ( Ord B /\ Ord A ) -> ( B e. A \/ A C_ B ) )
17 14 15 16 syl2anr 
 |-  ( ( A e. On /\ B e. On ) -> ( B e. A \/ A C_ B ) )
18 17 ord 
 |-  ( ( A e. On /\ B e. On ) -> ( -. B e. A -> A C_ B ) )
19 18 con1d 
 |-  ( ( A e. On /\ B e. On ) -> ( -. A C_ B -> B e. A ) )
20 alephord 
 |-  ( ( B e. On /\ A e. On ) -> ( B e. A <-> ( aleph ` B ) ~< ( aleph ` A ) ) )
21 20 ancoms 
 |-  ( ( A e. On /\ B e. On ) -> ( B e. A <-> ( aleph ` B ) ~< ( aleph ` A ) ) )
22 sdomnen 
 |-  ( ( aleph ` B ) ~< ( aleph ` A ) -> -. ( aleph ` B ) ~~ ( aleph ` A ) )
23 sdomdom 
 |-  ( ( aleph ` B ) ~< ( aleph ` A ) -> ( aleph ` B ) ~<_ ( aleph ` A ) )
24 sbth 
 |-  ( ( ( aleph ` B ) ~<_ ( aleph ` A ) /\ ( aleph ` A ) ~<_ ( aleph ` B ) ) -> ( aleph ` B ) ~~ ( aleph ` A ) )
25 24 ex 
 |-  ( ( aleph ` B ) ~<_ ( aleph ` A ) -> ( ( aleph ` A ) ~<_ ( aleph ` B ) -> ( aleph ` B ) ~~ ( aleph ` A ) ) )
26 23 25 syl 
 |-  ( ( aleph ` B ) ~< ( aleph ` A ) -> ( ( aleph ` A ) ~<_ ( aleph ` B ) -> ( aleph ` B ) ~~ ( aleph ` A ) ) )
27 22 26 mtod 
 |-  ( ( aleph ` B ) ~< ( aleph ` A ) -> -. ( aleph ` A ) ~<_ ( aleph ` B ) )
28 21 27 biimtrdi 
 |-  ( ( A e. On /\ B e. On ) -> ( B e. A -> -. ( aleph ` A ) ~<_ ( aleph ` B ) ) )
29 19 28 syld 
 |-  ( ( A e. On /\ B e. On ) -> ( -. A C_ B -> -. ( aleph ` A ) ~<_ ( aleph ` B ) ) )
30 13 29 impcon4bid 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B <-> ( aleph ` A ) ~<_ ( aleph ` B ) ) )