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	$$⊢\mathrm{card}\left(\aleph \left(A\right)\right)=\aleph \left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		2fveq3	$$⊢x=\varnothing \to \mathrm{card}\left(\aleph \left(x\right)\right)=\mathrm{card}\left(\aleph \left(\varnothing \right)\right)$$
2		fveq2	$$⊢x=\varnothing \to \aleph \left(x\right)=\aleph \left(\varnothing \right)$$
3	1 2	eqeq12d	$$⊢x=\varnothing \to \left(\mathrm{card}\left(\aleph \left(x\right)\right)=\aleph \left(x\right)\leftrightarrow \mathrm{card}\left(\aleph \left(\varnothing \right)\right)=\aleph \left(\varnothing \right)\right)$$
4		2fveq3	$$⊢x=y\to \mathrm{card}\left(\aleph \left(x\right)\right)=\mathrm{card}\left(\aleph \left(y\right)\right)$$
5		fveq2	$$⊢x=y\to \aleph \left(x\right)=\aleph \left(y\right)$$
6	4 5	eqeq12d	$$⊢x=y\to \left(\mathrm{card}\left(\aleph \left(x\right)\right)=\aleph \left(x\right)\leftrightarrow \mathrm{card}\left(\aleph \left(y\right)\right)=\aleph \left(y\right)\right)$$
7		2fveq3	$$⊢x=\mathrm{suc}y\to \mathrm{card}\left(\aleph \left(x\right)\right)=\mathrm{card}\left(\aleph \left(\mathrm{suc}y\right)\right)$$
8		fveq2	$$⊢x=\mathrm{suc}y\to \aleph \left(x\right)=\aleph \left(\mathrm{suc}y\right)$$
9	7 8	eqeq12d	$$⊢x=\mathrm{suc}y\to \left(\mathrm{card}\left(\aleph \left(x\right)\right)=\aleph \left(x\right)\leftrightarrow \mathrm{card}\left(\aleph \left(\mathrm{suc}y\right)\right)=\aleph \left(\mathrm{suc}y\right)\right)$$
10		2fveq3	$$⊢x=A\to \mathrm{card}\left(\aleph \left(x\right)\right)=\mathrm{card}\left(\aleph \left(A\right)\right)$$
11		fveq2	$$⊢x=A\to \aleph \left(x\right)=\aleph \left(A\right)$$
12	10 11	eqeq12d	$$⊢x=A\to \left(\mathrm{card}\left(\aleph \left(x\right)\right)=\aleph \left(x\right)\leftrightarrow \mathrm{card}\left(\aleph \left(A\right)\right)=\aleph \left(A\right)\right)$$
13		cardom	$$⊢\mathrm{card}\left(\mathrm{\omega }\right)=\mathrm{\omega }$$
14		aleph0	$$⊢\aleph \left(\varnothing \right)=\mathrm{\omega }$$
15	14	fveq2i	$$⊢\mathrm{card}\left(\aleph \left(\varnothing \right)\right)=\mathrm{card}\left(\mathrm{\omega }\right)$$
16	13 15 14	3eqtr4i	$$⊢\mathrm{card}\left(\aleph \left(\varnothing \right)\right)=\aleph \left(\varnothing \right)$$
17		harcard	$$⊢\mathrm{card}\left(\mathrm{har}\left(\aleph \left(y\right)\right)\right)=\mathrm{har}\left(\aleph \left(y\right)\right)$$
18		alephsuc	$$⊢y\in \mathrm{On}\to \aleph \left(\mathrm{suc}y\right)=\mathrm{har}\left(\aleph \left(y\right)\right)$$
19	18	fveq2d	$$⊢y\in \mathrm{On}\to \mathrm{card}\left(\aleph \left(\mathrm{suc}y\right)\right)=\mathrm{card}\left(\mathrm{har}\left(\aleph \left(y\right)\right)\right)$$
20	17 19 18	3eqtr4a	$$⊢y\in \mathrm{On}\to \mathrm{card}\left(\aleph \left(\mathrm{suc}y\right)\right)=\aleph \left(\mathrm{suc}y\right)$$
21	20	a1d	$$⊢y\in \mathrm{On}\to \left(\mathrm{card}\left(\aleph \left(y\right)\right)=\aleph \left(y\right)\to \mathrm{card}\left(\aleph \left(\mathrm{suc}y\right)\right)=\aleph \left(\mathrm{suc}y\right)\right)$$
22		cardiun	$$⊢x\in \mathrm{V}\to \left(\forall y\in x\mathrm{card}\left(\aleph \left(y\right)\right)=\aleph \left(y\right)\to \mathrm{card}\left(\bigcup _{y\in x}\aleph \left(y\right)\right)=\bigcup _{y\in x}\aleph \left(y\right)\right)$$
23	22	elv	$$⊢\forall y\in x\mathrm{card}\left(\aleph \left(y\right)\right)=\aleph \left(y\right)\to \mathrm{card}\left(\bigcup _{y\in x}\aleph \left(y\right)\right)=\bigcup _{y\in x}\aleph \left(y\right)$$
24	23	adantl	$$⊢\left(\mathrm{Lim}x\wedge \forall y\in x\mathrm{card}\left(\aleph \left(y\right)\right)=\aleph \left(y\right)\right)\to \mathrm{card}\left(\bigcup _{y\in x}\aleph \left(y\right)\right)=\bigcup _{y\in x}\aleph \left(y\right)$$
25		vex	$$⊢x\in \mathrm{V}$$
26		alephlim	$$⊢\left(x\in \mathrm{V}\wedge \mathrm{Lim}x\right)\to \aleph \left(x\right)=\bigcup _{y\in x}\aleph \left(y\right)$$
27	25 26	mpan	$$⊢\mathrm{Lim}x\to \aleph \left(x\right)=\bigcup _{y\in x}\aleph \left(y\right)$$
28	27	adantr	$$⊢\left(\mathrm{Lim}x\wedge \forall y\in x\mathrm{card}\left(\aleph \left(y\right)\right)=\aleph \left(y\right)\right)\to \aleph \left(x\right)=\bigcup _{y\in x}\aleph \left(y\right)$$
29	28	fveq2d	$$⊢\left(\mathrm{Lim}x\wedge \forall y\in x\mathrm{card}\left(\aleph \left(y\right)\right)=\aleph \left(y\right)\right)\to \mathrm{card}\left(\aleph \left(x\right)\right)=\mathrm{card}\left(\bigcup _{y\in x}\aleph \left(y\right)\right)$$
30	24 29 28	3eqtr4d	$$⊢\left(\mathrm{Lim}x\wedge \forall y\in x\mathrm{card}\left(\aleph \left(y\right)\right)=\aleph \left(y\right)\right)\to \mathrm{card}\left(\aleph \left(x\right)\right)=\aleph \left(x\right)$$
31	30	ex	$$⊢\mathrm{Lim}x\to \left(\forall y\in x\mathrm{card}\left(\aleph \left(y\right)\right)=\aleph \left(y\right)\to \mathrm{card}\left(\aleph \left(x\right)\right)=\aleph \left(x\right)\right)$$
32	3 6 9 12 16 21 31	tfinds	$$⊢A\in \mathrm{On}\to \mathrm{card}\left(\aleph \left(A\right)\right)=\aleph \left(A\right)$$
33		card0	$$⊢\mathrm{card}\left(\varnothing \right)=\varnothing$$
34		alephfnon	$$⊢\aleph Fn\mathrm{On}$$
35	34	fndmi	$$⊢\mathrm{dom}\aleph =\mathrm{On}$$
36	35	eleq2i	$$⊢A\in \mathrm{dom}\aleph \leftrightarrow A\in \mathrm{On}$$
37		ndmfv	$$⊢\neg A\in \mathrm{dom}\aleph \to \aleph \left(A\right)=\varnothing$$
38	36 37	sylnbir	$$⊢\neg A\in \mathrm{On}\to \aleph \left(A\right)=\varnothing$$
39	38	fveq2d	$$⊢\neg A\in \mathrm{On}\to \mathrm{card}\left(\aleph \left(A\right)\right)=\mathrm{card}\left(\varnothing \right)$$
40	33 39 38	3eqtr4a	$$⊢\neg A\in \mathrm{On}\to \mathrm{card}\left(\aleph \left(A\right)\right)=\aleph \left(A\right)$$
41	32 40	pm2.61i	$$⊢\mathrm{card}\left(\aleph \left(A\right)\right)=\aleph \left(A\right)$$