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