Metamath Proof Explorer

Theorem alephnbtwn2

Description: No set has equinumerosity between an aleph and its successor aleph. (Contributed by NM, 3-Nov-2003) (Revised by Mario Carneiro, 2-Feb-2013)

Ref Expression
Assertion alephnbtwn2 ⊢ ¬ ℵ ⁡ A ≺ B ∧ B ≺ ℵ ⁡ suc ⁡ A

Proof

Step Hyp Ref Expression
1 cardidm ⊢ card ⁡ card ⁡ B = card ⁡ B
2 alephnbtwn ⊢ card ⁡ card ⁡ B = card ⁡ B → ¬ ℵ ⁡ A ∈ card ⁡ B ∧ card ⁡ B ∈ ℵ ⁡ suc ⁡ A
3 1 2 ax-mp ⊢ ¬ ℵ ⁡ A ∈ card ⁡ B ∧ card ⁡ B ∈ ℵ ⁡ suc ⁡ A
4 alephon ⊢ ℵ ⁡ suc ⁡ A ∈ On
5 sdomdom ⊢ B ≺ ℵ ⁡ suc ⁡ A → B ≼ ℵ ⁡ suc ⁡ A
6 ondomen ⊢ ℵ ⁡ suc ⁡ A ∈ On ∧ B ≼ ℵ ⁡ suc ⁡ A → B ∈ dom ⁡ card
7 4 5 6 sylancr ⊢ B ≺ ℵ ⁡ suc ⁡ A → B ∈ dom ⁡ card
8 cardid2 ⊢ B ∈ dom ⁡ card → card ⁡ B ≈ B
9 7 8 syl ⊢ B ≺ ℵ ⁡ suc ⁡ A → card ⁡ B ≈ B
10 9 ensymd ⊢ B ≺ ℵ ⁡ suc ⁡ A → B ≈ card ⁡ B
11 sdomentr ⊢ ℵ ⁡ A ≺ B ∧ B ≈ card ⁡ B → ℵ ⁡ A ≺ card ⁡ B
12 10 11 sylan2 ⊢ ℵ ⁡ A ≺ B ∧ B ≺ ℵ ⁡ suc ⁡ A → ℵ ⁡ A ≺ card ⁡ B
13 alephon ⊢ ℵ ⁡ A ∈ On
14 cardon ⊢ card ⁡ B ∈ On
15 onenon ⊢ card ⁡ B ∈ On → card ⁡ B ∈ dom ⁡ card
16 14 15 ax-mp ⊢ card ⁡ B ∈ dom ⁡ card
17 cardsdomel ⊢ ℵ ⁡ A ∈ On ∧ card ⁡ B ∈ dom ⁡ card → ℵ ⁡ A ≺ card ⁡ B ↔ ℵ ⁡ A ∈ card ⁡ card ⁡ B
18 13 16 17 mp2an ⊢ ℵ ⁡ A ≺ card ⁡ B ↔ ℵ ⁡ A ∈ card ⁡ card ⁡ B
19 1 eleq2i ⊢ ℵ ⁡ A ∈ card ⁡ card ⁡ B ↔ ℵ ⁡ A ∈ card ⁡ B
20 18 19 bitri ⊢ ℵ ⁡ A ≺ card ⁡ B ↔ ℵ ⁡ A ∈ card ⁡ B
21 12 20 sylib ⊢ ℵ ⁡ A ≺ B ∧ B ≺ ℵ ⁡ suc ⁡ A → ℵ ⁡ A ∈ card ⁡ B
22 ensdomtr ⊢ card ⁡ B ≈ B ∧ B ≺ ℵ ⁡ suc ⁡ A → card ⁡ B ≺ ℵ ⁡ suc ⁡ A
23 9 22 mpancom ⊢ B ≺ ℵ ⁡ suc ⁡ A → card ⁡ B ≺ ℵ ⁡ suc ⁡ A
24 23 adantl ⊢ ℵ ⁡ A ≺ B ∧ B ≺ ℵ ⁡ suc ⁡ A → card ⁡ B ≺ ℵ ⁡ suc ⁡ A
25 onenon ⊢ ℵ ⁡ suc ⁡ A ∈ On → ℵ ⁡ suc ⁡ A ∈ dom ⁡ card
26 4 25 ax-mp ⊢ ℵ ⁡ suc ⁡ A ∈ dom ⁡ card
27 cardsdomel ⊢ card ⁡ B ∈ On ∧ ℵ ⁡ suc ⁡ A ∈ dom ⁡ card → card ⁡ B ≺ ℵ ⁡ suc ⁡ A ↔ card ⁡ B ∈ card ⁡ ℵ ⁡ suc ⁡ A
28 14 26 27 mp2an ⊢ card ⁡ B ≺ ℵ ⁡ suc ⁡ A ↔ card ⁡ B ∈ card ⁡ ℵ ⁡ suc ⁡ A
29 alephcard ⊢ card ⁡ ℵ ⁡ suc ⁡ A = ℵ ⁡ suc ⁡ A
30 29 eleq2i ⊢ card ⁡ B ∈ card ⁡ ℵ ⁡ suc ⁡ A ↔ card ⁡ B ∈ ℵ ⁡ suc ⁡ A
31 28 30 bitri ⊢ card ⁡ B ≺ ℵ ⁡ suc ⁡ A ↔ card ⁡ B ∈ ℵ ⁡ suc ⁡ A
32 24 31 sylib ⊢ ℵ ⁡ A ≺ B ∧ B ≺ ℵ ⁡ suc ⁡ A → card ⁡ B ∈ ℵ ⁡ suc ⁡ A
33 21 32 jca ⊢ ℵ ⁡ A ≺ B ∧ B ≺ ℵ ⁡ suc ⁡ A → ℵ ⁡ A ∈ card ⁡ B ∧ card ⁡ B ∈ ℵ ⁡ suc ⁡ A
34 3 33 mto ⊢ ¬ ℵ ⁡ A ≺ B ∧ B ≺ ℵ ⁡ suc ⁡ A