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

Metamath Proof Explorer

Theorem abfmpunirn

Description: Membership in a union of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 28-Sep-2016)

Ref Expression
Hypotheses abfmpunirn.1 
|- F = ( x e. V |-> { y | ph } )
abfmpunirn.2 
|- { y | ph } e. _V
abfmpunirn.3 
|- ( y = B -> ( ph <-> ps ) )
Assertion abfmpunirn 
|- ( B e. U. ran F <-> ( B e. _V /\ E. x e. V ps ) )

Proof

Step Hyp Ref Expression
1 abfmpunirn.1 
 |-  F = ( x e. V |-> { y | ph } )
2 abfmpunirn.2 
 |-  { y | ph } e. _V
3 abfmpunirn.3 
 |-  ( y = B -> ( ph <-> ps ) )
4 elex 
 |-  ( B e. U. ran F -> B e. _V )
5 2 1 fnmpti 
 |-  F Fn V
6 fnunirn 
 |-  ( F Fn V -> ( B e. U. ran F <-> E. x e. V B e. ( F ` x ) ) )
7 5 6 ax-mp 
 |-  ( B e. U. ran F <-> E. x e. V B e. ( F ` x ) )
8 1 fvmpt2 
 |-  ( ( x e. V /\ { y | ph } e. _V ) -> ( F ` x ) = { y | ph } )
9 2 8 mpan2 
 |-  ( x e. V -> ( F ` x ) = { y | ph } )
10 9 eleq2d 
 |-  ( x e. V -> ( B e. ( F ` x ) <-> B e. { y | ph } ) )
11 10 rexbiia 
 |-  ( E. x e. V B e. ( F ` x ) <-> E. x e. V B e. { y | ph } )
12 7 11 bitri 
 |-  ( B e. U. ran F <-> E. x e. V B e. { y | ph } )
13 3 elabg 
 |-  ( B e. _V -> ( B e. { y | ph } <-> ps ) )
14 13 rexbidv 
 |-  ( B e. _V -> ( E. x e. V B e. { y | ph } <-> E. x e. V ps ) )
15 12 14 bitrid 
 |-  ( B e. _V -> ( B e. U. ran F <-> E. x e. V ps ) )
16 4 15 biadanii 
 |-  ( B e. U. ran F <-> ( B e. _V /\ E. x e. V ps ) )