Theorem uniimadom

Description: An upper bound for the cardinality of the union of an image. Theorem 10.48 of TakeutiZaring p. 99. (Contributed by NM, 25-Mar-2006)

	Ref	Expression
Hypotheses	uniimadom.1	$$⊢A\in \mathrm{V}$$
	uniimadom.2	$$⊢B\in \mathrm{V}$$
Assertion	uniimadom	$$⊢\left(\mathrm{Fun}F\wedge \forall x\in AF\left(x\right)\preccurlyeq B\right)\to \bigcup F\left[A\right]\preccurlyeq \left(A\times B\right)$$

Proof

Step	Hyp	Ref	Expression
1		uniimadom.1	$$⊢A\in \mathrm{V}$$
2		uniimadom.2	$$⊢B\in \mathrm{V}$$
3	1	funimaex	$$⊢\mathrm{Fun}F\to F\left[A\right]\in \mathrm{V}$$
4	3	adantr	$$⊢\left(\mathrm{Fun}F\wedge \forall x\in AF\left(x\right)\preccurlyeq B\right)\to F\left[A\right]\in \mathrm{V}$$
5		fvelima	$$⊢\left(\mathrm{Fun}F\wedge y\in F\left[A\right]\right)\to \exists x\in AF\left(x\right)=y$$
6	5	ex	$$⊢\mathrm{Fun}F\to \left(y\in F\left[A\right]\to \exists x\in AF\left(x\right)=y\right)$$
7		breq1	$$⊢F\left(x\right)=y\to \left(F\left(x\right)\preccurlyeq B\leftrightarrow y\preccurlyeq B\right)$$
8	7	biimpd	$$⊢F\left(x\right)=y\to \left(F\left(x\right)\preccurlyeq B\to y\preccurlyeq B\right)$$
9	8	reximi	$$⊢\exists x\in AF\left(x\right)=y\to \exists x\in A\left(F\left(x\right)\preccurlyeq B\to y\preccurlyeq B\right)$$
10		r19.36v	$$⊢\exists x\in A\left(F\left(x\right)\preccurlyeq B\to y\preccurlyeq B\right)\to \left(\forall x\in AF\left(x\right)\preccurlyeq B\to y\preccurlyeq B\right)$$
11	9 10	syl	$$⊢\exists x\in AF\left(x\right)=y\to \left(\forall x\in AF\left(x\right)\preccurlyeq B\to y\preccurlyeq B\right)$$
12	6 11	syl6	$$⊢\mathrm{Fun}F\to \left(y\in F\left[A\right]\to \left(\forall x\in AF\left(x\right)\preccurlyeq B\to y\preccurlyeq B\right)\right)$$
13	12	com23	$$⊢\mathrm{Fun}F\to \left(\forall x\in AF\left(x\right)\preccurlyeq B\to \left(y\in F\left[A\right]\to y\preccurlyeq B\right)\right)$$
14	13	imp	$$⊢\left(\mathrm{Fun}F\wedge \forall x\in AF\left(x\right)\preccurlyeq B\right)\to \left(y\in F\left[A\right]\to y\preccurlyeq B\right)$$
15	14	ralrimiv	$$⊢\left(\mathrm{Fun}F\wedge \forall x\in AF\left(x\right)\preccurlyeq B\right)\to \forall y\in F\left[A\right]y\preccurlyeq B$$
16		unidom	$$⊢\left(F\left[A\right]\in \mathrm{V}\wedge \forall y\in F\left[A\right]y\preccurlyeq B\right)\to \bigcup F\left[A\right]\preccurlyeq \left(F\left[A\right]\times B\right)$$
17	4 15 16	syl2anc	$$⊢\left(\mathrm{Fun}F\wedge \forall x\in AF\left(x\right)\preccurlyeq B\right)\to \bigcup F\left[A\right]\preccurlyeq \left(F\left[A\right]\times B\right)$$
18		imadomg	$$⊢A\in \mathrm{V}\to \left(\mathrm{Fun}F\to F\left[A\right]\preccurlyeq A\right)$$
19	1 18	ax-mp	$$⊢\mathrm{Fun}F\to F\left[A\right]\preccurlyeq A$$
20	2	xpdom1	$$⊢F\left[A\right]\preccurlyeq A\to \left(F\left[A\right]\times B\right)\preccurlyeq \left(A\times B\right)$$
21	19 20	syl	$$⊢\mathrm{Fun}F\to \left(F\left[A\right]\times B\right)\preccurlyeq \left(A\times B\right)$$
22	21	adantr	$$⊢\left(\mathrm{Fun}F\wedge \forall x\in AF\left(x\right)\preccurlyeq B\right)\to \left(F\left[A\right]\times B\right)\preccurlyeq \left(A\times B\right)$$
23		domtr	$$⊢\left(\bigcup F\left[A\right]\preccurlyeq \left(F\left[A\right]\times B\right)\wedge \left(F\left[A\right]\times B\right)\preccurlyeq \left(A\times B\right)\right)\to \bigcup F\left[A\right]\preccurlyeq \left(A\times B\right)$$
24	17 22 23	syl2anc	$$⊢\left(\mathrm{Fun}F\wedge \forall x\in AF\left(x\right)\preccurlyeq B\right)\to \bigcup F\left[A\right]\preccurlyeq \left(A\times B\right)$$