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	|- F/_ x F
	uniimadomf.2	|- A e. _V
	uniimadomf.3	|- B e. _V
Assertion	uniimadomf	|- ( ( Fun F /\ A. x e. A ( F ` x ) ~<_ B ) -> U. ( F " A ) ~<_ ( A X. B ) )

Proof

Step	Hyp	Ref	Expression
1		uniimadomf.1	|- F/_ x F
2		uniimadomf.2	|- A e. _V
3		uniimadomf.3	|- B e. _V
4		nfv	|- F/ z ( F ` x ) ~<_ B
5		nfcv	|- F/_ x z
6	1 5	nffv	|- F/_ x ( F ` z )
7		nfcv	|- F/_ x ~<_
8		nfcv	|- F/_ x B
9	6 7 8	nfbr	|- F/ x ( F ` z ) ~<_ B
10		fveq2	|- ( x = z -> ( F ` x ) = ( F ` z ) )
11	10	breq1d	|- ( x = z -> ( ( F ` x ) ~<_ B <-> ( F ` z ) ~<_ B ) )
12	4 9 11	cbvralw	|- ( A. x e. A ( F ` x ) ~<_ B <-> A. z e. A ( F ` z ) ~<_ B )
13	2 3	uniimadom	|- ( ( Fun F /\ A. z e. A ( F ` z ) ~<_ B ) -> U. ( F " A ) ~<_ ( A X. B ) )
14	12 13	sylan2b	|- ( ( Fun F /\ A. x e. A ( F ` x ) ~<_ B ) -> U. ( F " A ) ~<_ ( A X. B ) )