Theorem uniimadomf

Description: An upper bound for the cardinality of the union of an image. Theorem 10.48 of TakeutiZaring p. 99. This version of uniimadom uses a bound-variable hypothesis in place of a distinct variable condition. (Contributed by NM, 26-Mar-2006)

	Ref	Expression
Hypotheses	uniimadomf.1	$$⊢\underset{\_}{Ⅎ}xF$$
	uniimadomf.2	$$⊢A\in \mathrm{V}$$
	uniimadomf.3	$$⊢B\in \mathrm{V}$$
Assertion	uniimadomf	$$⊢\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		uniimadomf.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		uniimadomf.2	$$⊢A\in \mathrm{V}$$
3		uniimadomf.3	$$⊢B\in \mathrm{V}$$
4		nfv	$$⊢ℲzF\left(x\right)\preccurlyeq B$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}xz$$
6	1 5	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(z\right)$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}x\preccurlyeq$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}xB$$
9	6 7 8	nfbr	$$⊢ℲxF\left(z\right)\preccurlyeq B$$
10		fveq2	$$⊢x=z\to F\left(x\right)=F\left(z\right)$$
11	10	breq1d	$$⊢x=z\to \left(F\left(x\right)\preccurlyeq B\leftrightarrow F\left(z\right)\preccurlyeq B\right)$$
12	4 9 11	cbvralw	$$⊢\forall x\in AF\left(x\right)\preccurlyeq B\leftrightarrow \forall z\in AF\left(z\right)\preccurlyeq B$$
13	2 3	uniimadom	$$⊢\left(\mathrm{Fun}F\wedge \forall z\in AF\left(z\right)\preccurlyeq B\right)\to \bigcup F\left[A\right]\preccurlyeq \left(A\times B\right)$$
14	12 13	sylan2b	$$⊢\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)$$