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 ‘ 𝐵 ) = 𝐵 → ¬ ( ( ℵ ‘ 𝐴 ) ∈ 𝐵 ∧ 𝐵 ∈ ( ℵ ‘ suc 𝐴 ) ) )

Proof

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