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 ⊢B∈On→A≼ℵ⁡B↔A≺ℵ⁡suc⁡B

Proof

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