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