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 𝐴 ) ) )