Metamath Proof Explorer

Theorem fparlem3

Description: Lemma for fpar . (Contributed by NM, 22-Dec-2008) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion fparlem3 
|- ( F Fn A -> ( `' ( 1st |` ( _V X. _V ) ) o. ( F o. ( 1st |` ( _V X. _V ) ) ) ) = U_ x e. A ( ( { x } X. _V ) X. ( { ( F ` x ) } X. _V ) ) )

Proof

Step Hyp Ref Expression
1 coiun 
 |-  ( `' ( 1st |` ( _V X. _V ) ) o. U_ x e. A ( ( `' ( 1st |` ( _V X. _V ) ) " { x } ) X. ( F " { x } ) ) ) = U_ x e. A ( `' ( 1st |` ( _V X. _V ) ) o. ( ( `' ( 1st |` ( _V X. _V ) ) " { x } ) X. ( F " { x } ) ) )
2 inss1 
 |-  ( dom F i^i ran ( 1st |` ( _V X. _V ) ) ) C_ dom F
3 fndm 
 |-  ( F Fn A -> dom F = A )
4 2 3 sseqtrid 
 |-  ( F Fn A -> ( dom F i^i ran ( 1st |` ( _V X. _V ) ) ) C_ A )
5 dfco2a 
 |-  ( ( dom F i^i ran ( 1st |` ( _V X. _V ) ) ) C_ A -> ( F o. ( 1st |` ( _V X. _V ) ) ) = U_ x e. A ( ( `' ( 1st |` ( _V X. _V ) ) " { x } ) X. ( F " { x } ) ) )
6 4 5 syl 
 |-  ( F Fn A -> ( F o. ( 1st |` ( _V X. _V ) ) ) = U_ x e. A ( ( `' ( 1st |` ( _V X. _V ) ) " { x } ) X. ( F " { x } ) ) )
7 6 coeq2d 
 |-  ( F Fn A -> ( `' ( 1st |` ( _V X. _V ) ) o. ( F o. ( 1st |` ( _V X. _V ) ) ) ) = ( `' ( 1st |` ( _V X. _V ) ) o. U_ x e. A ( ( `' ( 1st |` ( _V X. _V ) ) " { x } ) X. ( F " { x } ) ) ) )
8 inss1 
 |-  ( dom ( { ( F ` x ) } X. ( { x } X. _V ) ) i^i ran ( 1st |` ( _V X. _V ) ) ) C_ dom ( { ( F ` x ) } X. ( { x } X. _V ) )
9 dmxpss 
 |-  dom ( { ( F ` x ) } X. ( { x } X. _V ) ) C_ { ( F ` x ) }
10 8 9 sstri 
 |-  ( dom ( { ( F ` x ) } X. ( { x } X. _V ) ) i^i ran ( 1st |` ( _V X. _V ) ) ) C_ { ( F ` x ) }
11 dfco2a 
 |-  ( ( dom ( { ( F ` x ) } X. ( { x } X. _V ) ) i^i ran ( 1st |` ( _V X. _V ) ) ) C_ { ( F ` x ) } -> ( ( { ( F ` x ) } X. ( { x } X. _V ) ) o. ( 1st |` ( _V X. _V ) ) ) = U_ y e. { ( F ` x ) } ( ( `' ( 1st |` ( _V X. _V ) ) " { y } ) X. ( ( { ( F ` x ) } X. ( { x } X. _V ) ) " { y } ) ) )
12 10 11 ax-mp 
 |-  ( ( { ( F ` x ) } X. ( { x } X. _V ) ) o. ( 1st |` ( _V X. _V ) ) ) = U_ y e. { ( F ` x ) } ( ( `' ( 1st |` ( _V X. _V ) ) " { y } ) X. ( ( { ( F ` x ) } X. ( { x } X. _V ) ) " { y } ) )
13 fvex 
 |-  ( F ` x ) e. _V
14 fparlem1 
 |-  ( `' ( 1st |` ( _V X. _V ) ) " { y } ) = ( { y } X. _V )
15 sneq 
 |-  ( y = ( F ` x ) -> { y } = { ( F ` x ) } )
16 15 xpeq1d 
 |-  ( y = ( F ` x ) -> ( { y } X. _V ) = ( { ( F ` x ) } X. _V ) )
17 14 16 eqtrid 
 |-  ( y = ( F ` x ) -> ( `' ( 1st |` ( _V X. _V ) ) " { y } ) = ( { ( F ` x ) } X. _V ) )
18 15 imaeq2d 
 |-  ( y = ( F ` x ) -> ( ( { ( F ` x ) } X. ( { x } X. _V ) ) " { y } ) = ( ( { ( F ` x ) } X. ( { x } X. _V ) ) " { ( F ` x ) } ) )
19 df-ima 
 |-  ( ( { ( F ` x ) } X. ( { x } X. _V ) ) " { ( F ` x ) } ) = ran ( ( { ( F ` x ) } X. ( { x } X. _V ) ) |` { ( F ` x ) } )
20 ssid 
 |-  { ( F ` x ) } C_ { ( F ` x ) }
21 xpssres 
 |-  ( { ( F ` x ) } C_ { ( F ` x ) } -> ( ( { ( F ` x ) } X. ( { x } X. _V ) ) |` { ( F ` x ) } ) = ( { ( F ` x ) } X. ( { x } X. _V ) ) )
22 20 21 ax-mp 
 |-  ( ( { ( F ` x ) } X. ( { x } X. _V ) ) |` { ( F ` x ) } ) = ( { ( F ` x ) } X. ( { x } X. _V ) )
23 22 rneqi 
 |-  ran ( ( { ( F ` x ) } X. ( { x } X. _V ) ) |` { ( F ` x ) } ) = ran ( { ( F ` x ) } X. ( { x } X. _V ) )
24 13 snnz 
 |-  { ( F ` x ) } =/= (/)
25 rnxp 
 |-  ( { ( F ` x ) } =/= (/) -> ran ( { ( F ` x ) } X. ( { x } X. _V ) ) = ( { x } X. _V ) )
26 24 25 ax-mp 
 |-  ran ( { ( F ` x ) } X. ( { x } X. _V ) ) = ( { x } X. _V )
27 23 26 eqtri 
 |-  ran ( ( { ( F ` x ) } X. ( { x } X. _V ) ) |` { ( F ` x ) } ) = ( { x } X. _V )
28 19 27 eqtri 
 |-  ( ( { ( F ` x ) } X. ( { x } X. _V ) ) " { ( F ` x ) } ) = ( { x } X. _V )
29 18 28 eqtrdi 
 |-  ( y = ( F ` x ) -> ( ( { ( F ` x ) } X. ( { x } X. _V ) ) " { y } ) = ( { x } X. _V ) )
30 17 29 xpeq12d 
 |-  ( y = ( F ` x ) -> ( ( `' ( 1st |` ( _V X. _V ) ) " { y } ) X. ( ( { ( F ` x ) } X. ( { x } X. _V ) ) " { y } ) ) = ( ( { ( F ` x ) } X. _V ) X. ( { x } X. _V ) ) )
31 13 30 iunxsn 
 |-  U_ y e. { ( F ` x ) } ( ( `' ( 1st |` ( _V X. _V ) ) " { y } ) X. ( ( { ( F ` x ) } X. ( { x } X. _V ) ) " { y } ) ) = ( ( { ( F ` x ) } X. _V ) X. ( { x } X. _V ) )
32 12 31 eqtri 
 |-  ( ( { ( F ` x ) } X. ( { x } X. _V ) ) o. ( 1st |` ( _V X. _V ) ) ) = ( ( { ( F ` x ) } X. _V ) X. ( { x } X. _V ) )
33 32 cnveqi 
 |-  `' ( ( { ( F ` x ) } X. ( { x } X. _V ) ) o. ( 1st |` ( _V X. _V ) ) ) = `' ( ( { ( F ` x ) } X. _V ) X. ( { x } X. _V ) )
34 cnvco 
 |-  `' ( ( { ( F ` x ) } X. ( { x } X. _V ) ) o. ( 1st |` ( _V X. _V ) ) ) = ( `' ( 1st |` ( _V X. _V ) ) o. `' ( { ( F ` x ) } X. ( { x } X. _V ) ) )
35 cnvxp 
 |-  `' ( ( { ( F ` x ) } X. _V ) X. ( { x } X. _V ) ) = ( ( { x } X. _V ) X. ( { ( F ` x ) } X. _V ) )
36 33 34 35 3eqtr3i 
 |-  ( `' ( 1st |` ( _V X. _V ) ) o. `' ( { ( F ` x ) } X. ( { x } X. _V ) ) ) = ( ( { x } X. _V ) X. ( { ( F ` x ) } X. _V ) )
37 fparlem1 
 |-  ( `' ( 1st |` ( _V X. _V ) ) " { x } ) = ( { x } X. _V )
38 37 xpeq2i 
 |-  ( { ( F ` x ) } X. ( `' ( 1st |` ( _V X. _V ) ) " { x } ) ) = ( { ( F ` x ) } X. ( { x } X. _V ) )
39 fnsnfv 
 |-  ( ( F Fn A /\ x e. A ) -> { ( F ` x ) } = ( F " { x } ) )
40 39 xpeq1d 
 |-  ( ( F Fn A /\ x e. A ) -> ( { ( F ` x ) } X. ( `' ( 1st |` ( _V X. _V ) ) " { x } ) ) = ( ( F " { x } ) X. ( `' ( 1st |` ( _V X. _V ) ) " { x } ) ) )
41 38 40 eqtr3id 
 |-  ( ( F Fn A /\ x e. A ) -> ( { ( F ` x ) } X. ( { x } X. _V ) ) = ( ( F " { x } ) X. ( `' ( 1st |` ( _V X. _V ) ) " { x } ) ) )
42 41 cnveqd 
 |-  ( ( F Fn A /\ x e. A ) -> `' ( { ( F ` x ) } X. ( { x } X. _V ) ) = `' ( ( F " { x } ) X. ( `' ( 1st |` ( _V X. _V ) ) " { x } ) ) )
43 cnvxp 
 |-  `' ( ( F " { x } ) X. ( `' ( 1st |` ( _V X. _V ) ) " { x } ) ) = ( ( `' ( 1st |` ( _V X. _V ) ) " { x } ) X. ( F " { x } ) )
44 42 43 eqtrdi 
 |-  ( ( F Fn A /\ x e. A ) -> `' ( { ( F ` x ) } X. ( { x } X. _V ) ) = ( ( `' ( 1st |` ( _V X. _V ) ) " { x } ) X. ( F " { x } ) ) )
45 44 coeq2d 
 |-  ( ( F Fn A /\ x e. A ) -> ( `' ( 1st |` ( _V X. _V ) ) o. `' ( { ( F ` x ) } X. ( { x } X. _V ) ) ) = ( `' ( 1st |` ( _V X. _V ) ) o. ( ( `' ( 1st |` ( _V X. _V ) ) " { x } ) X. ( F " { x } ) ) ) )
46 36 45 eqtr3id 
 |-  ( ( F Fn A /\ x e. A ) -> ( ( { x } X. _V ) X. ( { ( F ` x ) } X. _V ) ) = ( `' ( 1st |` ( _V X. _V ) ) o. ( ( `' ( 1st |` ( _V X. _V ) ) " { x } ) X. ( F " { x } ) ) ) )
47 46 iuneq2dv 
 |-  ( F Fn A -> U_ x e. A ( ( { x } X. _V ) X. ( { ( F ` x ) } X. _V ) ) = U_ x e. A ( `' ( 1st |` ( _V X. _V ) ) o. ( ( `' ( 1st |` ( _V X. _V ) ) " { x } ) X. ( F " { x } ) ) ) )
48 1 7 47 3eqtr4a 
 |-  ( F Fn A -> ( `' ( 1st |` ( _V X. _V ) ) o. ( F o. ( 1st |` ( _V X. _V ) ) ) ) = U_ x e. A ( ( { x } X. _V ) X. ( { ( F ` x ) } X. _V ) ) )