Metamath Proof Explorer

Theorem marypha2lem4

Description: Lemma for marypha2 . Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015)

Ref Expression
Hypothesis marypha2lem.t 
|- T = U_ x e. A ( { x } X. ( F ` x ) )
Assertion marypha2lem4 
|- ( ( F Fn A /\ X C_ A ) -> ( T " X ) = U. ( F " X ) )

Proof

Step Hyp Ref Expression
1 marypha2lem.t 
 |-  T = U_ x e. A ( { x } X. ( F ` x ) )
2 1 marypha2lem2 
 |-  T = { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) }
3 2 imaeq1i 
 |-  ( T " X ) = ( { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) } " X )
4 df-ima 
 |-  ( { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) } " X ) = ran ( { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) } |` X )
5 3 4 eqtri 
 |-  ( T " X ) = ran ( { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) } |` X )
6 resopab2 
 |-  ( X C_ A -> ( { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) } |` X ) = { <. x , y >. | ( x e. X /\ y e. ( F ` x ) ) } )
7 6 adantl 
 |-  ( ( F Fn A /\ X C_ A ) -> ( { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) } |` X ) = { <. x , y >. | ( x e. X /\ y e. ( F ` x ) ) } )
8 7 rneqd 
 |-  ( ( F Fn A /\ X C_ A ) -> ran ( { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) } |` X ) = ran { <. x , y >. | ( x e. X /\ y e. ( F ` x ) ) } )
9 rnopab 
 |-  ran { <. x , y >. | ( x e. X /\ y e. ( F ` x ) ) } = { y | E. x ( x e. X /\ y e. ( F ` x ) ) }
10 df-rex 
 |-  ( E. x e. X y e. ( F ` x ) <-> E. x ( x e. X /\ y e. ( F ` x ) ) )
11 10 bicomi 
 |-  ( E. x ( x e. X /\ y e. ( F ` x ) ) <-> E. x e. X y e. ( F ` x ) )
12 11 abbii 
 |-  { y | E. x ( x e. X /\ y e. ( F ` x ) ) } = { y | E. x e. X y e. ( F ` x ) }
13 df-iun 
 |-  U_ x e. X ( F ` x ) = { y | E. x e. X y e. ( F ` x ) }
14 12 13 eqtr4i 
 |-  { y | E. x ( x e. X /\ y e. ( F ` x ) ) } = U_ x e. X ( F ` x )
15 14 a1i 
 |-  ( ( F Fn A /\ X C_ A ) -> { y | E. x ( x e. X /\ y e. ( F ` x ) ) } = U_ x e. X ( F ` x ) )
16 9 15 syl5eq 
 |-  ( ( F Fn A /\ X C_ A ) -> ran { <. x , y >. | ( x e. X /\ y e. ( F ` x ) ) } = U_ x e. X ( F ` x ) )
17 8 16 eqtrd 
 |-  ( ( F Fn A /\ X C_ A ) -> ran ( { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) } |` X ) = U_ x e. X ( F ` x ) )
18 5 17 syl5eq 
 |-  ( ( F Fn A /\ X C_ A ) -> ( T " X ) = U_ x e. X ( F ` x ) )
19 fnfun 
 |-  ( F Fn A -> Fun F )
20 19 adantr 
 |-  ( ( F Fn A /\ X C_ A ) -> Fun F )
21 funiunfv 
 |-  ( Fun F -> U_ x e. X ( F ` x ) = U. ( F " X ) )
22 20 21 syl 
 |-  ( ( F Fn A /\ X C_ A ) -> U_ x e. X ( F ` x ) = U. ( F " X ) )
23 18 22 eqtrd 
 |-  ( ( F Fn A /\ X C_ A ) -> ( T " X ) = U. ( F " X ) )