Theorem iundomg

Description: An upper bound for the cardinality of an indexed union, with explicit choice principles. B depends on x and should be thought of as B ( x ) . (Contributed by Mario Carneiro, 1-Sep-2015)

	Ref	Expression
Hypotheses	iunfo.1	$$⊢T=\bigcup _{x\in A}\left(\left\{x\right\}\times B\right)$$
	iundomg.2	$$⊢\phi \to \bigcup _{x\in A}\left(C^B\right)\in \underset{\_}{\mathrm{AC}}A$$
	iundomg.3	$$⊢\phi \to \forall x\in AB\preccurlyeq C$$
	iundomg.4	$$⊢\phi \to A\times C\in \underset{\_}{\mathrm{AC}}\bigcup _{x\in A}B$$
Assertion	iundomg	$$⊢\phi \to \bigcup _{x\in A}B\preccurlyeq \left(A\times C\right)$$

Proof

Step	Hyp	Ref	Expression
1		iunfo.1	$$⊢T=\bigcup _{x\in A}\left(\left\{x\right\}\times B\right)$$
2		iundomg.2	$$⊢\phi \to \bigcup _{x\in A}\left(C^B\right)\in \underset{\_}{\mathrm{AC}}A$$
3		iundomg.3	$$⊢\phi \to \forall x\in AB\preccurlyeq C$$
4		iundomg.4	$$⊢\phi \to A\times C\in \underset{\_}{\mathrm{AC}}\bigcup _{x\in A}B$$
5	1 2 3	iundom2g	$$⊢\phi \to T\preccurlyeq \left(A\times C\right)$$
6		acndom2	$$⊢T\preccurlyeq \left(A\times C\right)\to \left(A\times C\in \underset{\_}{\mathrm{AC}}\bigcup _{x\in A}B\to T\in \underset{\_}{\mathrm{AC}}\bigcup _{x\in A}B\right)$$
7	5 4 6	sylc	$$⊢\phi \to T\in \underset{\_}{\mathrm{AC}}\bigcup _{x\in A}B$$
8	1	iunfo	$$⊢\left({2^{nd}\upharpoonright }_T\right):T\underset{onto}{⟶}\bigcup _{x\in A}B$$
9		fodomacn	$$⊢T\in \underset{\_}{\mathrm{AC}}\bigcup _{x\in A}B\to \left(\left({2^{nd}\upharpoonright }_T\right):T\underset{onto}{⟶}\bigcup _{x\in A}B\to \bigcup _{x\in A}B\preccurlyeq T\right)$$
10	7 8 9	mpisyl	$$⊢\phi \to \bigcup _{x\in A}B\preccurlyeq T$$
11		domtr	$$⊢\left(\bigcup _{x\in A}B\preccurlyeq T\wedge T\preccurlyeq \left(A\times C\right)\right)\to \bigcup _{x\in A}B\preccurlyeq \left(A\times C\right)$$
12	10 5 11	syl2anc	$$⊢\phi \to \bigcup _{x\in A}B\preccurlyeq \left(A\times C\right)$$