Theorem alephcard

Description: Every aleph is a cardinal number. Theorem 65 of Suppes p. 229. (Contributed by NM, 25-Oct-2003) (Revised by Mario Carneiro, 2-Feb-2013)

	Ref	Expression
Assertion	alephcard	⊢ ( card ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		2fveq3	⊢ ( 𝑥 = ∅ → ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( card ‘ ( ℵ ‘ ∅ ) ) )
2		fveq2	⊢ ( 𝑥 = ∅ → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ ∅ ) )
3	1 2	eqeq12d	⊢ ( 𝑥 = ∅ → ( ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( ℵ ‘ 𝑥 ) ↔ ( card ‘ ( ℵ ‘ ∅ ) ) = ( ℵ ‘ ∅ ) ) )
4		2fveq3	⊢ ( 𝑥 = 𝑦 → ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( card ‘ ( ℵ ‘ 𝑦 ) ) )
5		fveq2	⊢ ( 𝑥 = 𝑦 → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ 𝑦 ) )
6	4 5	eqeq12d	⊢ ( 𝑥 = 𝑦 → ( ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( ℵ ‘ 𝑥 ) ↔ ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) )
7		2fveq3	⊢ ( 𝑥 = suc 𝑦 → ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( card ‘ ( ℵ ‘ suc 𝑦 ) ) )
8		fveq2	⊢ ( 𝑥 = suc 𝑦 → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ suc 𝑦 ) )
9	7 8	eqeq12d	⊢ ( 𝑥 = suc 𝑦 → ( ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( ℵ ‘ 𝑥 ) ↔ ( card ‘ ( ℵ ‘ suc 𝑦 ) ) = ( ℵ ‘ suc 𝑦 ) ) )
10		2fveq3	⊢ ( 𝑥 = 𝐴 → ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( card ‘ ( ℵ ‘ 𝐴 ) ) )
11		fveq2	⊢ ( 𝑥 = 𝐴 → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ 𝐴 ) )
12	10 11	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( ℵ ‘ 𝑥 ) ↔ ( card ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 ) ) )
13		cardom	⊢ ( card ‘ ω ) = ω
14		aleph0	⊢ ( ℵ ‘ ∅ ) = ω
15	14	fveq2i	⊢ ( card ‘ ( ℵ ‘ ∅ ) ) = ( card ‘ ω )
16	13 15 14	3eqtr4i	⊢ ( card ‘ ( ℵ ‘ ∅ ) ) = ( ℵ ‘ ∅ )
17		harcard	⊢ ( card ‘ ( har ‘ ( ℵ ‘ 𝑦 ) ) ) = ( har ‘ ( ℵ ‘ 𝑦 ) )
18		alephsuc	⊢ ( 𝑦 ∈ On → ( ℵ ‘ suc 𝑦 ) = ( har ‘ ( ℵ ‘ 𝑦 ) ) )
19	18	fveq2d	⊢ ( 𝑦 ∈ On → ( card ‘ ( ℵ ‘ suc 𝑦 ) ) = ( card ‘ ( har ‘ ( ℵ ‘ 𝑦 ) ) ) )
20	17 19 18	3eqtr4a	⊢ ( 𝑦 ∈ On → ( card ‘ ( ℵ ‘ suc 𝑦 ) ) = ( ℵ ‘ suc 𝑦 ) )
21	20	a1d	⊢ ( 𝑦 ∈ On → ( ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) → ( card ‘ ( ℵ ‘ suc 𝑦 ) ) = ( ℵ ‘ suc 𝑦 ) ) )
22		cardiun	⊢ ( 𝑥 ∈ V → ( ∀ 𝑦 ∈ 𝑥 ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) → ( card ‘ ∪ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) ) = ∪ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) ) )
23	22	elv	⊢ ( ∀ 𝑦 ∈ 𝑥 ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) → ( card ‘ ∪ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) ) = ∪ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) )
24	23	adantl	⊢ ( ( Lim 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) → ( card ‘ ∪ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) ) = ∪ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) )
25		vex	⊢ 𝑥 ∈ V
26		alephlim	⊢ ( ( 𝑥 ∈ V ∧ Lim 𝑥 ) → ( ℵ ‘ 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) )
27	25 26	mpan	⊢ ( Lim 𝑥 → ( ℵ ‘ 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) )
28	27	adantr	⊢ ( ( Lim 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) → ( ℵ ‘ 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) )
29	28	fveq2d	⊢ ( ( Lim 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) → ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( card ‘ ∪ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) ) )
30	24 29 28	3eqtr4d	⊢ ( ( Lim 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) → ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( ℵ ‘ 𝑥 ) )
31	30	ex	⊢ ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) → ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( ℵ ‘ 𝑥 ) ) )
32	3 6 9 12 16 21 31	tfinds	⊢ ( 𝐴 ∈ On → ( card ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 ) )
33		card0	⊢ ( card ‘ ∅ ) = ∅
34		alephfnon	⊢ ℵ Fn On
35	34	fndmi	⊢ dom ℵ = On
36	35	eleq2i	⊢ ( 𝐴 ∈ dom ℵ ↔ 𝐴 ∈ On )
37		ndmfv	⊢ ( ¬ 𝐴 ∈ dom ℵ → ( ℵ ‘ 𝐴 ) = ∅ )
38	36 37	sylnbir	⊢ ( ¬ 𝐴 ∈ On → ( ℵ ‘ 𝐴 ) = ∅ )
39	38	fveq2d	⊢ ( ¬ 𝐴 ∈ On → ( card ‘ ( ℵ ‘ 𝐴 ) ) = ( card ‘ ∅ ) )
40	33 39 38	3eqtr4a	⊢ ( ¬ 𝐴 ∈ On → ( card ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 ) )
41	32 40	pm2.61i	⊢ ( card ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 )