Metamath Proof Explorer

Theorem alephnbtwn

Description: No cardinal can be sandwiched between an aleph and its successor aleph. Theorem 67 of Suppes p. 229. (Contributed by NM, 10-Nov-2003) (Revised by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion alephnbtwn ⊢ card ⁡ B = B → ¬ ℵ ⁡ A ∈ B ∧ B ∈ ℵ ⁡ suc ⁡ A

Proof

Step Hyp Ref Expression
1 alephon ⊢ ℵ ⁡ A ∈ On
2 id ⊢ card ⁡ B = B → card ⁡ B = B
3 cardon ⊢ card ⁡ B ∈ On
4 2 3 eqeltrrdi ⊢ card ⁡ B = B → B ∈ On
5 onenon ⊢ B ∈ On → B ∈ dom ⁡ card
6 4 5 syl ⊢ card ⁡ B = B → B ∈ dom ⁡ card
7 cardsdomel ⊢ ℵ ⁡ A ∈ On ∧ B ∈ dom ⁡ card → ℵ ⁡ A ≺ B ↔ ℵ ⁡ A ∈ card ⁡ B
8 1 6 7 sylancr ⊢ card ⁡ B = B → ℵ ⁡ A ≺ B ↔ ℵ ⁡ A ∈ card ⁡ B
9 eleq2 ⊢ card ⁡ B = B → ℵ ⁡ A ∈ card ⁡ B ↔ ℵ ⁡ A ∈ B
10 8 9 bitrd ⊢ card ⁡ B = B → ℵ ⁡ A ≺ B ↔ ℵ ⁡ A ∈ B
11 10 adantl ⊢ A ∈ On ∧ card ⁡ B = B → ℵ ⁡ A ≺ B ↔ ℵ ⁡ A ∈ B
12 alephsuc ⊢ A ∈ On → ℵ ⁡ suc ⁡ A = har ⁡ ℵ ⁡ A
13 onenon ⊢ ℵ ⁡ A ∈ On → ℵ ⁡ A ∈ dom ⁡ card
14 harval2 ⊢ ℵ ⁡ A ∈ dom ⁡ card → har ⁡ ℵ ⁡ A = ⋂ x ∈ On | ℵ ⁡ A ≺ x
15 1 13 14 mp2b ⊢ har ⁡ ℵ ⁡ A = ⋂ x ∈ On | ℵ ⁡ A ≺ x
16 12 15 syl6eq ⊢ A ∈ On → ℵ ⁡ suc ⁡ A = ⋂ x ∈ On | ℵ ⁡ A ≺ x
17 16 eleq2d ⊢ A ∈ On → B ∈ ℵ ⁡ suc ⁡ A ↔ B ∈ ⋂ x ∈ On | ℵ ⁡ A ≺ x
18 17 biimpd ⊢ A ∈ On → B ∈ ℵ ⁡ suc ⁡ A → B ∈ ⋂ x ∈ On | ℵ ⁡ A ≺ x
19 breq2 ⊢ x = B → ℵ ⁡ A ≺ x ↔ ℵ ⁡ A ≺ B
20 19 onnminsb ⊢ B ∈ On → B ∈ ⋂ x ∈ On | ℵ ⁡ A ≺ x → ¬ ℵ ⁡ A ≺ B
21 18 20 sylan9 ⊢ A ∈ On ∧ B ∈ On → B ∈ ℵ ⁡ suc ⁡ A → ¬ ℵ ⁡ A ≺ B
22 21 con2d ⊢ A ∈ On ∧ B ∈ On → ℵ ⁡ A ≺ B → ¬ B ∈ ℵ ⁡ suc ⁡ A
23 4 22 sylan2 ⊢ A ∈ On ∧ card ⁡ B = B → ℵ ⁡ A ≺ B → ¬ B ∈ ℵ ⁡ suc ⁡ A
24 11 23 sylbird ⊢ A ∈ On ∧ card ⁡ B = B → ℵ ⁡ A ∈ B → ¬ B ∈ ℵ ⁡ suc ⁡ A
25 imnan ⊢ ℵ ⁡ A ∈ B → ¬ B ∈ ℵ ⁡ suc ⁡ A ↔ ¬ ℵ ⁡ A ∈ B ∧ B ∈ ℵ ⁡ suc ⁡ A
26 24 25 sylib ⊢ A ∈ On ∧ card ⁡ B = B → ¬ ℵ ⁡ A ∈ B ∧ B ∈ ℵ ⁡ suc ⁡ A
27 26 ex ⊢ A ∈ On → card ⁡ B = B → ¬ ℵ ⁡ A ∈ B ∧ B ∈ ℵ ⁡ suc ⁡ A
28 n0i ⊢ B ∈ ℵ ⁡ suc ⁡ A → ¬ ℵ ⁡ suc ⁡ A = ∅
29 alephfnon ⊢ ℵ Fn On
30 fndm ⊢ ℵ Fn On → dom ⁡ ℵ = On
31 29 30 ax-mp ⊢ dom ⁡ ℵ = On
32 31 eleq2i ⊢ suc ⁡ A ∈ dom ⁡ ℵ ↔ suc ⁡ A ∈ On
33 ndmfv ⊢ ¬ suc ⁡ A ∈ dom ⁡ ℵ → ℵ ⁡ suc ⁡ A = ∅
34 32 33 sylnbir ⊢ ¬ suc ⁡ A ∈ On → ℵ ⁡ suc ⁡ A = ∅
35 28 34 nsyl2 ⊢ B ∈ ℵ ⁡ suc ⁡ A → suc ⁡ A ∈ On
36 sucelon ⊢ A ∈ On ↔ suc ⁡ A ∈ On
37 35 36 sylibr ⊢ B ∈ ℵ ⁡ suc ⁡ A → A ∈ On
38 37 adantl ⊢ ℵ ⁡ A ∈ B ∧ B ∈ ℵ ⁡ suc ⁡ A → A ∈ On
39 38 con3i ⊢ ¬ A ∈ On → ¬ ℵ ⁡ A ∈ B ∧ B ∈ ℵ ⁡ suc ⁡ A
40 39 a1d ⊢ ¬ A ∈ On → card ⁡ B = B → ¬ ℵ ⁡ A ∈ B ∧ B ∈ ℵ ⁡ suc ⁡ A
41 27 40 pm2.61i ⊢ card ⁡ B = B → ¬ ℵ ⁡ A ∈ B ∧ B ∈ ℵ ⁡ suc ⁡ A