Theorem alephcard 10176

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

Assertion

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

Proof of Theorem alephcard

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		2fveq3 6913	. . . 4 ⊢ (𝑥 = ∅ → (card‘(ℵ‘𝑥)) = (card‘(ℵ‘∅)))
2		fveq2 6908	. . . 4 ⊢ (𝑥 = ∅ → (ℵ‘𝑥) = (ℵ‘∅))
3	1, 2	eqeq12d 2779	. . 3 ⊢ (𝑥 = ∅ → ((card‘(ℵ‘𝑥)) = (ℵ‘𝑥) ↔ (card‘(ℵ‘∅)) = (ℵ‘∅)))
4		2fveq3 6913	. . . 4 ⊢ (𝑥 = 𝑦 → (card‘(ℵ‘𝑥)) = (card‘(ℵ‘𝑦)))
5		fveq2 6908	. . . 4 ⊢ (𝑥 = 𝑦 → (ℵ‘𝑥) = (ℵ‘𝑦))
6	4, 5	eqeq12d 2779	. . 3 ⊢ (𝑥 = 𝑦 → ((card‘(ℵ‘𝑥)) = (ℵ‘𝑥) ↔ (card‘(ℵ‘𝑦)) = (ℵ‘𝑦)))
7		2fveq3 6913	. . . 4 ⊢ (𝑥 = suc 𝑦 → (card‘(ℵ‘𝑥)) = (card‘(ℵ‘suc 𝑦)))
8		fveq2 6908	. . . 4 ⊢ (𝑥 = suc 𝑦 → (ℵ‘𝑥) = (ℵ‘suc 𝑦))
9	7, 8	eqeq12d 2779	. . 3 ⊢ (𝑥 = suc 𝑦 → ((card‘(ℵ‘𝑥)) = (ℵ‘𝑥) ↔ (card‘(ℵ‘suc 𝑦)) = (ℵ‘suc 𝑦)))
10		2fveq3 6913	. . . 4 ⊢ (𝑥 = 𝐴 → (card‘(ℵ‘𝑥)) = (card‘(ℵ‘𝐴)))
11		fveq2 6908	. . . 4 ⊢ (𝑥 = 𝐴 → (ℵ‘𝑥) = (ℵ‘𝐴))
12	10, 11	eqeq12d 2779	. . 3 ⊢ (𝑥 = 𝐴 → ((card‘(ℵ‘𝑥)) = (ℵ‘𝑥) ↔ (card‘(ℵ‘𝐴)) = (ℵ‘𝐴)))
13		cardom 10094	. . . 4 ⊢ (card‘ω) = ω
14		aleph0 10172	. . . . 5 ⊢ (ℵ‘∅) = ω
15	14	fveq2i 6911	. . . 4 ⊢ (card‘(ℵ‘∅)) = (card‘ω)
16	13, 15, 14	3eqtr4i 2796	. . 3 ⊢ (card‘(ℵ‘∅)) = (ℵ‘∅)
17		harcard 10086	. . . . 5 ⊢ (card‘(har‘(ℵ‘𝑦))) = (har‘(ℵ‘𝑦))
18		alephsuc 10174	. . . . . 6 ⊢ (𝑦 ∈ On → (ℵ‘suc 𝑦) = (har‘(ℵ‘𝑦)))
19	18	fveq2d 6912	. . . . 5 ⊢ (𝑦 ∈ On → (card‘(ℵ‘suc 𝑦)) = (card‘(har‘(ℵ‘𝑦))))
20	17, 19, 18	3eqtr4a 2824	. . . 4 ⊢ (𝑦 ∈ On → (card‘(ℵ‘suc 𝑦)) = (ℵ‘suc 𝑦))
21	20	a1d 26	. . 3 ⊢ (𝑦 ∈ On → ((card‘(ℵ‘𝑦)) = (ℵ‘𝑦) → (card‘(ℵ‘suc 𝑦)) = (ℵ‘suc 𝑦)))
22		cardiun 10090	. . . . . . 7 ⊢ (𝑥 ∈ V → (∀𝑦 ∈ 𝑥 (card‘(ℵ‘𝑦)) = (ℵ‘𝑦) → (card‘∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦)) = ∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦)))
23	22	elv 3459	. . . . . 6 ⊢ (∀𝑦 ∈ 𝑥 (card‘(ℵ‘𝑦)) = (ℵ‘𝑦) → (card‘∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦)) = ∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦))
24	23	adantl 487	. . . . 5 ⊢ ((Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 (card‘(ℵ‘𝑦)) = (ℵ‘𝑦)) → (card‘∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦)) = ∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦))
25		vex 3458	. . . . . . . 8 ⊢ 𝑥 ∈ V
26		alephlim 10173	. . . . . . . 8 ⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → (ℵ‘𝑥) = ∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦))
27	25, 26	mpan 703	. . . . . . 7 ⊢ (Lim 𝑥 → (ℵ‘𝑥) = ∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦))
28	27	adantr 486	. . . . . 6 ⊢ ((Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 (card‘(ℵ‘𝑦)) = (ℵ‘𝑦)) → (ℵ‘𝑥) = ∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦))
29	28	fveq2d 6912	. . . . 5 ⊢ ((Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 (card‘(ℵ‘𝑦)) = (ℵ‘𝑦)) → (card‘(ℵ‘𝑥)) = (card‘∪ 𝑦 ∈ 𝑥 (ℵ‘𝑦)))
30	24, 29, 28	3eqtr4d 2808	. . . 4 ⊢ ((Lim 𝑥 ∧ ∀𝑦 ∈ 𝑥 (card‘(ℵ‘𝑦)) = (ℵ‘𝑦)) → (card‘(ℵ‘𝑥)) = (ℵ‘𝑥))
31	30	ex 418	. . 3 ⊢ (Lim 𝑥 → (∀𝑦 ∈ 𝑥 (card‘(ℵ‘𝑦)) = (ℵ‘𝑦) → (card‘(ℵ‘𝑥)) = (ℵ‘𝑥)))
32	3, 6, 9, 12, 16, 21, 31	tfinds 7895	. 2 ⊢ (𝐴 ∈ On → (card‘(ℵ‘𝐴)) = (ℵ‘𝐴))
33		card0 10066	. . 3 ⊢ (card‘∅) = ∅
34		alephfnon 10171	. . . . . . 7 ⊢ ℵ Fn On
35	34	fndmi 6665	. . . . . 6 ⊢ dom ℵ = On
36	35	eleq2i 2856	. . . . 5 ⊢ (𝐴 ∈ dom ℵ ↔ 𝐴 ∈ On)
37		ndmfv 6940	. . . . 5 ⊢ (¬ 𝐴 ∈ dom ℵ → (ℵ‘𝐴) = ∅)
38	36, 37	sylnbir 334	. . . 4 ⊢ (¬ 𝐴 ∈ On → (ℵ‘𝐴) = ∅)
39	38	fveq2d 6912	. . 3 ⊢ (¬ 𝐴 ∈ On → (card‘(ℵ‘𝐴)) = (card‘∅))
40	33, 39, 38	3eqtr4a 2824	. 2 ⊢ (¬ 𝐴 ∈ On → (card‘(ℵ‘𝐴)) = (ℵ‘𝐴))
41	32, 40	pm2.61i 184	1 ⊢ (card‘(ℵ‘𝐴)) = (ℵ‘𝐴)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∀wral 3080  Vcvv 3454  ∅c0 4281  ∪ ciun 4954  dom cdm 5655  Oncon0 6380  Lim wlim 6381  suc csuc 6382  ‘cfv 6558  ωcom 7901  harchar 9577  cardccrd 10043  ℵcale 10044

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-inf2 9669

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6322  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-isom 6567  df-riota 7400  df-ov 7446  df-om 7902  df-2nd 8026  df-frecs 8327  df-wrecs 8358  df-recs 8407  df-rdg 8446  df-1o 8504  df-er 8745  df-en 9002  df-dom 9003  df-sdom 9004  df-fin 9005  df-oi 9531  df-har 9578  df-card 10047  df-aleph 10048

This theorem is used by:  alephnbtwn2  10178  alephord2  10182  alephsuc2  10186  alephislim  10189  alephsdom  10192  cardaleph  10195  cardalephex  10196  alephval3  10216  alephval2  10684  alephsuc3  10692  alephreg  10694  pwcfsdom  10695  minregex2  44728