This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )