Theorem carduniima

Description: The union of the image of a mapping to cardinals is a cardinal. Proposition 11.16 of TakeutiZaring p. 104. (Contributed by NM, 4-Nov-2004)

	Ref	Expression
Assertion	carduniima	$$⊢A\in B\to \left(F:A⟶\mathrm{\omega }\cup \mathrm{ran}\aleph \to \bigcup F\left[A\right]\in \left(\mathrm{\omega }\cup \mathrm{ran}\aleph \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ffun	$$⊢F:A⟶\mathrm{\omega }\cup \mathrm{ran}\aleph \to \mathrm{Fun}F$$
2		funimaexg	$$⊢\left(\mathrm{Fun}F\wedge A\in B\right)\to F\left[A\right]\in \mathrm{V}$$
3	1 2	sylan	$$⊢\left(F:A⟶\mathrm{\omega }\cup \mathrm{ran}\aleph \wedge A\in B\right)\to F\left[A\right]\in \mathrm{V}$$
4	3	expcom	$$⊢A\in B\to \left(F:A⟶\mathrm{\omega }\cup \mathrm{ran}\aleph \to F\left[A\right]\in \mathrm{V}\right)$$
5		fimass	$$⊢F:A⟶\mathrm{\omega }\cup \mathrm{ran}\aleph \to F\left[A\right]\subseteq \mathrm{\omega }\cup \mathrm{ran}\aleph$$
6	5	sseld	$$⊢F:A⟶\mathrm{\omega }\cup \mathrm{ran}\aleph \to \left(x\in F\left[A\right]\to x\in \left(\mathrm{\omega }\cup \mathrm{ran}\aleph \right)\right)$$
7		iscard3	$$⊢\mathrm{card}\left(x\right)=x\leftrightarrow x\in \left(\mathrm{\omega }\cup \mathrm{ran}\aleph \right)$$
8	6 7	syl6ibr	$$⊢F:A⟶\mathrm{\omega }\cup \mathrm{ran}\aleph \to \left(x\in F\left[A\right]\to \mathrm{card}\left(x\right)=x\right)$$
9	8	ralrimiv	$$⊢F:A⟶\mathrm{\omega }\cup \mathrm{ran}\aleph \to \forall x\in F\left[A\right]\mathrm{card}\left(x\right)=x$$
10		carduni	$$⊢F\left[A\right]\in \mathrm{V}\to \left(\forall x\in F\left[A\right]\mathrm{card}\left(x\right)=x\to \mathrm{card}\left(\bigcup F\left[A\right]\right)=\bigcup F\left[A\right]\right)$$
11	9 10	syl5	$$⊢F\left[A\right]\in \mathrm{V}\to \left(F:A⟶\mathrm{\omega }\cup \mathrm{ran}\aleph \to \mathrm{card}\left(\bigcup F\left[A\right]\right)=\bigcup F\left[A\right]\right)$$
12	4 11	syli	$$⊢A\in B\to \left(F:A⟶\mathrm{\omega }\cup \mathrm{ran}\aleph \to \mathrm{card}\left(\bigcup F\left[A\right]\right)=\bigcup F\left[A\right]\right)$$
13		iscard3	$$⊢\mathrm{card}\left(\bigcup F\left[A\right]\right)=\bigcup F\left[A\right]\leftrightarrow \bigcup F\left[A\right]\in \left(\mathrm{\omega }\cup \mathrm{ran}\aleph \right)$$
14	12 13	syl6ib	$$⊢A\in B\to \left(F:A⟶\mathrm{\omega }\cup \mathrm{ran}\aleph \to \bigcup F\left[A\right]\in \left(\mathrm{\omega }\cup \mathrm{ran}\aleph \right)\right)$$