Theorem cardiun

Description: The indexed union of a set of cardinals is a cardinal. (Contributed by NM, 3-Nov-2003)

	Ref	Expression
Assertion	cardiun	$$⊢A\in V\to \left(\forall x\in A\mathrm{card}\left(B\right)=B\to \mathrm{card}\left(\bigcup _{x\in A}B\right)=\bigcup _{x\in A}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		abrexexg	$$⊢A\in V\to \left\{z|\exists x\in Az=\mathrm{card}\left(B\right)\right\}\in \mathrm{V}$$
2		vex	$$⊢y\in \mathrm{V}$$
3		eqeq1	$$⊢z=y\to \left(z=\mathrm{card}\left(B\right)\leftrightarrow y=\mathrm{card}\left(B\right)\right)$$
4	3	rexbidv	$$⊢z=y\to \left(\exists x\in Az=\mathrm{card}\left(B\right)\leftrightarrow \exists x\in Ay=\mathrm{card}\left(B\right)\right)$$
5	2 4	elab	$$⊢y\in \left\{z|\exists x\in Az=\mathrm{card}\left(B\right)\right\}\leftrightarrow \exists x\in Ay=\mathrm{card}\left(B\right)$$
6		cardidm	$$⊢\mathrm{card}\left(\mathrm{card}\left(B\right)\right)=\mathrm{card}\left(B\right)$$
7		fveq2	$$⊢y=\mathrm{card}\left(B\right)\to \mathrm{card}\left(y\right)=\mathrm{card}\left(\mathrm{card}\left(B\right)\right)$$
8		id	$$⊢y=\mathrm{card}\left(B\right)\to y=\mathrm{card}\left(B\right)$$
9	6 7 8	3eqtr4a	$$⊢y=\mathrm{card}\left(B\right)\to \mathrm{card}\left(y\right)=y$$
10	9	rexlimivw	$$⊢\exists x\in Ay=\mathrm{card}\left(B\right)\to \mathrm{card}\left(y\right)=y$$
11	5 10	sylbi	$$⊢y\in \left\{z|\exists x\in Az=\mathrm{card}\left(B\right)\right\}\to \mathrm{card}\left(y\right)=y$$
12	11	rgen	$$⊢\forall y\in \left\{z|\exists x\in Az=\mathrm{card}\left(B\right)\right\}\mathrm{card}\left(y\right)=y$$
13		carduni	$$⊢\left\{z|\exists x\in Az=\mathrm{card}\left(B\right)\right\}\in \mathrm{V}\to \left(\forall y\in \left\{z|\exists x\in Az=\mathrm{card}\left(B\right)\right\}\mathrm{card}\left(y\right)=y\to \mathrm{card}\left(\bigcup \left\{z|\exists x\in Az=\mathrm{card}\left(B\right)\right\}\right)=\bigcup \left\{z|\exists x\in Az=\mathrm{card}\left(B\right)\right\}\right)$$
14	1 12 13	mpisyl	$$⊢A\in V\to \mathrm{card}\left(\bigcup \left\{z|\exists x\in Az=\mathrm{card}\left(B\right)\right\}\right)=\bigcup \left\{z|\exists x\in Az=\mathrm{card}\left(B\right)\right\}$$
15		fvex	$$⊢\mathrm{card}\left(B\right)\in \mathrm{V}$$
16	15	dfiun2	$$⊢\bigcup _{x\in A}\mathrm{card}\left(B\right)=\bigcup \left\{z|\exists x\in Az=\mathrm{card}\left(B\right)\right\}$$
17	16	fveq2i	$$⊢\mathrm{card}\left(\bigcup _{x\in A}\mathrm{card}\left(B\right)\right)=\mathrm{card}\left(\bigcup \left\{z|\exists x\in Az=\mathrm{card}\left(B\right)\right\}\right)$$
18	14 17 16	3eqtr4g	$$⊢A\in V\to \mathrm{card}\left(\bigcup _{x\in A}\mathrm{card}\left(B\right)\right)=\bigcup _{x\in A}\mathrm{card}\left(B\right)$$
19	18	adantr	$$⊢\left(A\in V\wedge \forall x\in A\mathrm{card}\left(B\right)=B\right)\to \mathrm{card}\left(\bigcup _{x\in A}\mathrm{card}\left(B\right)\right)=\bigcup _{x\in A}\mathrm{card}\left(B\right)$$
20		iuneq2	$$⊢\forall x\in A\mathrm{card}\left(B\right)=B\to \bigcup _{x\in A}\mathrm{card}\left(B\right)=\bigcup _{x\in A}B$$
21	20	adantl	$$⊢\left(A\in V\wedge \forall x\in A\mathrm{card}\left(B\right)=B\right)\to \bigcup _{x\in A}\mathrm{card}\left(B\right)=\bigcup _{x\in A}B$$
22	21	fveq2d	$$⊢\left(A\in V\wedge \forall x\in A\mathrm{card}\left(B\right)=B\right)\to \mathrm{card}\left(\bigcup _{x\in A}\mathrm{card}\left(B\right)\right)=\mathrm{card}\left(\bigcup _{x\in A}B\right)$$
23	19 22 21	3eqtr3d	$$⊢\left(A\in V\wedge \forall x\in A\mathrm{card}\left(B\right)=B\right)\to \mathrm{card}\left(\bigcup _{x\in A}B\right)=\bigcup _{x\in A}B$$
24	23	ex	$$⊢A\in V\to \left(\forall x\in A\mathrm{card}\left(B\right)=B\to \mathrm{card}\left(\bigcup _{x\in A}B\right)=\bigcup _{x\in A}B\right)$$