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	syl6eqelr	⊢ ( ( 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	syl6eq	⊢ ( 𝐴 ∈ 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		fndm	⊢ ( ℵ Fn On → dom ℵ = On )
31	29 30	ax-mp	⊢ dom ℵ = On
32	31	eleq2i	⊢ ( suc 𝐴 ∈ dom ℵ ↔ suc 𝐴 ∈ On )
33		ndmfv	⊢ ( ¬ suc 𝐴 ∈ dom ℵ → ( ℵ ‘ suc 𝐴 ) = ∅ )
34	32 33	sylnbir	⊢ ( ¬ suc 𝐴 ∈ On → ( ℵ ‘ suc 𝐴 ) = ∅ )
35	28 34	nsyl2	⊢ ( 𝐵 ∈ ( ℵ ‘ suc 𝐴 ) → suc 𝐴 ∈ On )
36		sucelon	⊢ ( 𝐴 ∈ On ↔ suc 𝐴 ∈ On )
37	35 36	sylibr	⊢ ( 𝐵 ∈ ( ℵ ‘ suc 𝐴 ) → 𝐴 ∈ On )
38	37	adantl	⊢ ( ( ( ℵ ‘ 𝐴 ) ∈ 𝐵 ∧ 𝐵 ∈ ( ℵ ‘ suc 𝐴 ) ) → 𝐴 ∈ On )
39	38	con3i	⊢ ( ¬ 𝐴 ∈ On → ¬ ( ( ℵ ‘ 𝐴 ) ∈ 𝐵 ∧ 𝐵 ∈ ( ℵ ‘ suc 𝐴 ) ) )
40	39	a1d	⊢ ( ¬ 𝐴 ∈ On → ( ( card ‘ 𝐵 ) = 𝐵 → ¬ ( ( ℵ ‘ 𝐴 ) ∈ 𝐵 ∧ 𝐵 ∈ ( ℵ ‘ suc 𝐴 ) ) ) )
41	27 40	pm2.61i	⊢ ( ( card ‘ 𝐵 ) = 𝐵 → ¬ ( ( ℵ ‘ 𝐴 ) ∈ 𝐵 ∧ 𝐵 ∈ ( ℵ ‘ suc 𝐴 ) ) )