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 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ( ℵ ‘ 𝐴 ) ≼ ( ℵ ‘ 𝐵 ) ) )

Proof

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