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 biimtrdi ⊢ 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 biimtrdi ⊢ 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