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∈On∧B∈On→A⊆B↔ℵ⁡A≼ℵ⁡B

Proof

Step Hyp Ref Expression
1 onsseleq ⊢A∈On∧B∈On→A⊆B↔A∈B∨A=B
2 alephord ⊢A∈On∧B∈On→A∈B↔ℵ⁡A≺ℵ⁡B
3 sdomdom ⊢ℵ⁡A≺ℵ⁡B→ℵ⁡A≼ℵ⁡B
4 2 3 syl6bi ⊢A∈On∧B∈On→A∈B→ℵ⁡A≼ℵ⁡B
5 fvex ⊢ℵ⁡A∈V
6 fveq2 ⊢A=B→ℵ⁡A=ℵ⁡B
7 eqeng ⊢ℵ⁡A∈V→ℵ⁡A=ℵ⁡B→ℵ⁡A≈ℵ⁡B
8 5 6 7 mpsyl ⊢A=B→ℵ⁡A≈ℵ⁡B
9 8 a1i ⊢A∈On∧B∈On→A=B→ℵ⁡A≈ℵ⁡B
10 endom ⊢ℵ⁡A≈ℵ⁡B→ℵ⁡A≼ℵ⁡B
11 9 10 syl6 ⊢A∈On∧B∈On→A=B→ℵ⁡A≼ℵ⁡B
12 4 11 jaod ⊢A∈On∧B∈On→A∈B∨A=B→ℵ⁡A≼ℵ⁡B
13 1 12 sylbid ⊢A∈On∧B∈On→A⊆B→ℵ⁡A≼ℵ⁡B
14 eloni ⊢B∈On→Ord⁡B
15 eloni ⊢A∈On→Ord⁡A
16 ordtri2or ⊢Ord⁡B∧Ord⁡A→B∈A∨A⊆B
17 14 15 16 syl2anr ⊢A∈On∧B∈On→B∈A∨A⊆B
18 17 ord ⊢A∈On∧B∈On→¬B∈A→A⊆B
19 18 con1d ⊢A∈On∧B∈On→¬A⊆B→B∈A
20 alephord ⊢B∈On∧A∈On→B∈A↔ℵ⁡B≺ℵ⁡A
21 20 ancoms ⊢A∈On∧B∈On→B∈A↔ℵ⁡B≺ℵ⁡A
22 sdomnen ⊢ℵ⁡B≺ℵ⁡A→¬ℵ⁡B≈ℵ⁡A
23 sdomdom ⊢ℵ⁡B≺ℵ⁡A→ℵ⁡B≼ℵ⁡A
24 sbth ⊢ℵ⁡B≼ℵ⁡A∧ℵ⁡A≼ℵ⁡B→ℵ⁡B≈ℵ⁡A
25 24 ex ⊢ℵ⁡B≼ℵ⁡A→ℵ⁡A≼ℵ⁡B→ℵ⁡B≈ℵ⁡A
26 23 25 syl ⊢ℵ⁡B≺ℵ⁡A→ℵ⁡A≼ℵ⁡B→ℵ⁡B≈ℵ⁡A
27 22 26 mtod ⊢ℵ⁡B≺ℵ⁡A→¬ℵ⁡A≼ℵ⁡B
28 21 27 syl6bi ⊢A∈On∧B∈On→B∈A→¬ℵ⁡A≼ℵ⁡B
29 19 28 syld ⊢A∈On∧B∈On→¬A⊆B→¬ℵ⁡A≼ℵ⁡B
30 13 29 impcon4bid ⊢A∈On∧B∈On→A⊆B↔ℵ⁡A≼ℵ⁡B