Metamath Proof Explorer

Theorem fpar

Description: Merge two functions in parallel. Use as the second argument of a composition with a binary operation to build compound functions such as ( x e. ( 0 [,) +oo ) , y e. RR |-> ( ( sqrtx ) + ( siny ) ) ) , see also ex-fpar . (Contributed by NM, 17-Sep-2007) (Proof shortened by Mario Carneiro, 28-Apr-2015)

Ref Expression
Hypothesis fpar.1 
|- H = ( ( `' ( 1st |` ( _V X. _V ) ) o. ( F o. ( 1st |` ( _V X. _V ) ) ) ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. ( G o. ( 2nd |` ( _V X. _V ) ) ) ) )
Assertion fpar 
|- ( ( F Fn A /\ G Fn B ) -> H = ( x e. A , y e. B |-> <. ( F ` x ) , ( G ` y ) >. ) )

Proof

Step Hyp Ref Expression
1 fpar.1 
 |-  H = ( ( `' ( 1st |` ( _V X. _V ) ) o. ( F o. ( 1st |` ( _V X. _V ) ) ) ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. ( G o. ( 2nd |` ( _V X. _V ) ) ) ) )
2 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 ) ) )
3 fparlem4 
 |-  ( G Fn B -> ( `' ( 2nd |` ( _V X. _V ) ) o. ( G o. ( 2nd |` ( _V X. _V ) ) ) ) = U_ y e. B ( ( _V X. { y } ) X. ( _V X. { ( G ` y ) } ) ) )
4 2 3 ineqan12d 
 |-  ( ( F Fn A /\ G Fn B ) -> ( ( `' ( 1st |` ( _V X. _V ) ) o. ( F o. ( 1st |` ( _V X. _V ) ) ) ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. ( G o. ( 2nd |` ( _V X. _V ) ) ) ) ) = ( U_ x e. A ( ( { x } X. _V ) X. ( { ( F ` x ) } X. _V ) ) i^i U_ y e. B ( ( _V X. { y } ) X. ( _V X. { ( G ` y ) } ) ) ) )
5 opex 
 |-  <. ( F ` x ) , ( G ` y ) >. e. _V
6 5 dfmpo 
 |-  ( x e. A , y e. B |-> <. ( F ` x ) , ( G ` y ) >. ) = U_ x e. A U_ y e. B { <. <. x , y >. , <. ( F ` x ) , ( G ` y ) >. >. }
7 inxp 
 |-  ( ( ( { x } X. _V ) X. ( { ( F ` x ) } X. _V ) ) i^i ( ( _V X. { y } ) X. ( _V X. { ( G ` y ) } ) ) ) = ( ( ( { x } X. _V ) i^i ( _V X. { y } ) ) X. ( ( { ( F ` x ) } X. _V ) i^i ( _V X. { ( G ` y ) } ) ) )
8 inxp 
 |-  ( ( { x } X. _V ) i^i ( _V X. { y } ) ) = ( ( { x } i^i _V ) X. ( _V i^i { y } ) )
9 inv1 
 |-  ( { x } i^i _V ) = { x }
10 incom 
 |-  ( _V i^i { y } ) = ( { y } i^i _V )
11 inv1 
 |-  ( { y } i^i _V ) = { y }
12 10 11 eqtri 
 |-  ( _V i^i { y } ) = { y }
13 9 12 xpeq12i 
 |-  ( ( { x } i^i _V ) X. ( _V i^i { y } ) ) = ( { x } X. { y } )
14 vex 
 |-  x e. _V
15 vex 
 |-  y e. _V
16 14 15 xpsn 
 |-  ( { x } X. { y } ) = { <. x , y >. }
17 8 13 16 3eqtri 
 |-  ( ( { x } X. _V ) i^i ( _V X. { y } ) ) = { <. x , y >. }
18 inxp 
 |-  ( ( { ( F ` x ) } X. _V ) i^i ( _V X. { ( G ` y ) } ) ) = ( ( { ( F ` x ) } i^i _V ) X. ( _V i^i { ( G ` y ) } ) )
19 inv1 
 |-  ( { ( F ` x ) } i^i _V ) = { ( F ` x ) }
20 incom 
 |-  ( _V i^i { ( G ` y ) } ) = ( { ( G ` y ) } i^i _V )
21 inv1 
 |-  ( { ( G ` y ) } i^i _V ) = { ( G ` y ) }
22 20 21 eqtri 
 |-  ( _V i^i { ( G ` y ) } ) = { ( G ` y ) }
23 19 22 xpeq12i 
 |-  ( ( { ( F ` x ) } i^i _V ) X. ( _V i^i { ( G ` y ) } ) ) = ( { ( F ` x ) } X. { ( G ` y ) } )
24 fvex 
 |-  ( F ` x ) e. _V
25 fvex 
 |-  ( G ` y ) e. _V
26 24 25 xpsn 
 |-  ( { ( F ` x ) } X. { ( G ` y ) } ) = { <. ( F ` x ) , ( G ` y ) >. }
27 18 23 26 3eqtri 
 |-  ( ( { ( F ` x ) } X. _V ) i^i ( _V X. { ( G ` y ) } ) ) = { <. ( F ` x ) , ( G ` y ) >. }
28 17 27 xpeq12i 
 |-  ( ( ( { x } X. _V ) i^i ( _V X. { y } ) ) X. ( ( { ( F ` x ) } X. _V ) i^i ( _V X. { ( G ` y ) } ) ) ) = ( { <. x , y >. } X. { <. ( F ` x ) , ( G ` y ) >. } )
29 opex 
 |-  <. x , y >. e. _V
30 29 5 xpsn 
 |-  ( { <. x , y >. } X. { <. ( F ` x ) , ( G ` y ) >. } ) = { <. <. x , y >. , <. ( F ` x ) , ( G ` y ) >. >. }
31 7 28 30 3eqtri 
 |-  ( ( ( { x } X. _V ) X. ( { ( F ` x ) } X. _V ) ) i^i ( ( _V X. { y } ) X. ( _V X. { ( G ` y ) } ) ) ) = { <. <. x , y >. , <. ( F ` x ) , ( G ` y ) >. >. }
32 31 a1i 
 |-  ( y e. B -> ( ( ( { x } X. _V ) X. ( { ( F ` x ) } X. _V ) ) i^i ( ( _V X. { y } ) X. ( _V X. { ( G ` y ) } ) ) ) = { <. <. x , y >. , <. ( F ` x ) , ( G ` y ) >. >. } )
33 32 iuneq2i 
 |-  U_ y e. B ( ( ( { x } X. _V ) X. ( { ( F ` x ) } X. _V ) ) i^i ( ( _V X. { y } ) X. ( _V X. { ( G ` y ) } ) ) ) = U_ y e. B { <. <. x , y >. , <. ( F ` x ) , ( G ` y ) >. >. }
34 33 a1i 
 |-  ( x e. A -> U_ y e. B ( ( ( { x } X. _V ) X. ( { ( F ` x ) } X. _V ) ) i^i ( ( _V X. { y } ) X. ( _V X. { ( G ` y ) } ) ) ) = U_ y e. B { <. <. x , y >. , <. ( F ` x ) , ( G ` y ) >. >. } )
35 34 iuneq2i 
 |-  U_ x e. A U_ y e. B ( ( ( { x } X. _V ) X. ( { ( F ` x ) } X. _V ) ) i^i ( ( _V X. { y } ) X. ( _V X. { ( G ` y ) } ) ) ) = U_ x e. A U_ y e. B { <. <. x , y >. , <. ( F ` x ) , ( G ` y ) >. >. }
36 2iunin 
 |-  U_ x e. A U_ y e. B ( ( ( { x } X. _V ) X. ( { ( F ` x ) } X. _V ) ) i^i ( ( _V X. { y } ) X. ( _V X. { ( G ` y ) } ) ) ) = ( U_ x e. A ( ( { x } X. _V ) X. ( { ( F ` x ) } X. _V ) ) i^i U_ y e. B ( ( _V X. { y } ) X. ( _V X. { ( G ` y ) } ) ) )
37 6 35 36 3eqtr2i 
 |-  ( x e. A , y e. B |-> <. ( F ` x ) , ( G ` y ) >. ) = ( U_ x e. A ( ( { x } X. _V ) X. ( { ( F ` x ) } X. _V ) ) i^i U_ y e. B ( ( _V X. { y } ) X. ( _V X. { ( G ` y ) } ) ) )
38 4 1 37 3eqtr4g 
 |-  ( ( F Fn A /\ G Fn B ) -> H = ( x e. A , y e. B |-> <. ( F ` x ) , ( G ` y ) >. ) )