Metamath Proof Explorer

Theorem alephsucdom

Description: A set dominated by an aleph is strictly dominated by its successor aleph and vice-versa. (Contributed by NM, 3-Nov-2003) (Revised by Mario Carneiro, 2-Feb-2013)

Ref Expression
Assertion alephsucdom ( 𝐵 ∈ On → ( 𝐴 ≼ ( ℵ ‘ 𝐵 ) ↔ 𝐴 ≺ ( ℵ ‘ suc 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 alephordilem1 ⊢ ( 𝐵 ∈ On → ( ℵ ‘ 𝐵 ) ≺ ( ℵ ‘ suc 𝐵 ) )
2 domsdomtr ⊢ ( ( 𝐴 ≼ ( ℵ ‘ 𝐵 ) ∧ ( ℵ ‘ 𝐵 ) ≺ ( ℵ ‘ suc 𝐵 ) ) → 𝐴 ≺ ( ℵ ‘ suc 𝐵 ) )
3 2 ex ⊢ ( 𝐴 ≼ ( ℵ ‘ 𝐵 ) → ( ( ℵ ‘ 𝐵 ) ≺ ( ℵ ‘ suc 𝐵 ) → 𝐴 ≺ ( ℵ ‘ suc 𝐵 ) ) )
4 1 3 syl5com ⊢ ( 𝐵 ∈ On → ( 𝐴 ≼ ( ℵ ‘ 𝐵 ) → 𝐴 ≺ ( ℵ ‘ suc 𝐵 ) ) )
5 sdomdom ⊢ ( 𝐴 ≺ ( ℵ ‘ suc 𝐵 ) → 𝐴 ≼ ( ℵ ‘ suc 𝐵 ) )
6 alephon ⊢ ( ℵ ‘ suc 𝐵 ) ∈ On
7 ondomen ⊢ ( ( ( ℵ ‘ suc 𝐵 ) ∈ On ∧ 𝐴 ≼ ( ℵ ‘ suc 𝐵 ) ) → 𝐴 ∈ dom card )
8 6 7 mpan ⊢ ( 𝐴 ≼ ( ℵ ‘ suc 𝐵 ) → 𝐴 ∈ dom card )
9 cardid2 ⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) ≈ 𝐴 )
10 5 8 9 3syl ⊢ ( 𝐴 ≺ ( ℵ ‘ suc 𝐵 ) → ( card ‘ 𝐴 ) ≈ 𝐴 )
11 10 ensymd ⊢ ( 𝐴 ≺ ( ℵ ‘ suc 𝐵 ) → 𝐴 ≈ ( card ‘ 𝐴 ) )
12 alephnbtwn2 ⊢ ¬ ( ( ℵ ‘ 𝐵 ) ≺ ( card ‘ 𝐴 ) ∧ ( card ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝐵 ) )
13 12 imnani ⊢ ( ( ℵ ‘ 𝐵 ) ≺ ( card ‘ 𝐴 ) → ¬ ( card ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝐵 ) )
14 ensdomtr ⊢ ( ( ( card ‘ 𝐴 ) ≈ 𝐴 ∧ 𝐴 ≺ ( ℵ ‘ suc 𝐵 ) ) → ( card ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝐵 ) )
15 10 14 mpancom ⊢ ( 𝐴 ≺ ( ℵ ‘ suc 𝐵 ) → ( card ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝐵 ) )
16 13 15 nsyl3 ⊢ ( 𝐴 ≺ ( ℵ ‘ suc 𝐵 ) → ¬ ( ℵ ‘ 𝐵 ) ≺ ( card ‘ 𝐴 ) )
17 cardon ⊢ ( card ‘ 𝐴 ) ∈ On
18 alephon ⊢ ( ℵ ‘ 𝐵 ) ∈ On
19 domtriord ⊢ ( ( ( card ‘ 𝐴 ) ∈ On ∧ ( ℵ ‘ 𝐵 ) ∈ On ) → ( ( card ‘ 𝐴 ) ≼ ( ℵ ‘ 𝐵 ) ↔ ¬ ( ℵ ‘ 𝐵 ) ≺ ( card ‘ 𝐴 ) ) )
20 17 18 19 mp2an ⊢ ( ( card ‘ 𝐴 ) ≼ ( ℵ ‘ 𝐵 ) ↔ ¬ ( ℵ ‘ 𝐵 ) ≺ ( card ‘ 𝐴 ) )
21 16 20 sylibr ⊢ ( 𝐴 ≺ ( ℵ ‘ suc 𝐵 ) → ( card ‘ 𝐴 ) ≼ ( ℵ ‘ 𝐵 ) )
22 endomtr ⊢ ( ( 𝐴 ≈ ( card ‘ 𝐴 ) ∧ ( card ‘ 𝐴 ) ≼ ( ℵ ‘ 𝐵 ) ) → 𝐴 ≼ ( ℵ ‘ 𝐵 ) )
23 11 21 22 syl2anc ⊢ ( 𝐴 ≺ ( ℵ ‘ suc 𝐵 ) → 𝐴 ≼ ( ℵ ‘ 𝐵 ) )
24 4 23 impbid1 ⊢ ( 𝐵 ∈ On → ( 𝐴 ≼ ( ℵ ‘ 𝐵 ) ↔ 𝐴 ≺ ( ℵ ‘ suc 𝐵 ) ) )