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

Metamath Proof Explorer

Theorem mpomptsx

Description: Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion mpomptsx 
|- ( x e. A , y e. B |-> C ) = ( z e. U_ x e. A ( { x } X. B ) |-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C )

Proof

Step Hyp Ref Expression
1 vex 
 |-  u e. _V
2 vex 
 |-  v e. _V
3 1 2 op1std 
 |-  ( z = <. u , v >. -> ( 1st ` z ) = u )
4 3 csbeq1d 
 |-  ( z = <. u , v >. -> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C = [_ u / x ]_ [_ ( 2nd ` z ) / y ]_ C )
5 1 2 op2ndd 
 |-  ( z = <. u , v >. -> ( 2nd ` z ) = v )
6 5 csbeq1d 
 |-  ( z = <. u , v >. -> [_ ( 2nd ` z ) / y ]_ C = [_ v / y ]_ C )
7 6 csbeq2dv 
 |-  ( z = <. u , v >. -> [_ u / x ]_ [_ ( 2nd ` z ) / y ]_ C = [_ u / x ]_ [_ v / y ]_ C )
8 4 7 eqtrd 
 |-  ( z = <. u , v >. -> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C = [_ u / x ]_ [_ v / y ]_ C )
9 8 mpomptx 
 |-  ( z e. U_ u e. A ( { u } X. [_ u / x ]_ B ) |-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C ) = ( u e. A , v e. [_ u / x ]_ B |-> [_ u / x ]_ [_ v / y ]_ C )
10 nfcv 
 |-  F/_ u ( { x } X. B )
11 nfcv 
 |-  F/_ x { u }
12 nfcsb1v 
 |-  F/_ x [_ u / x ]_ B
13 11 12 nfxp 
 |-  F/_ x ( { u } X. [_ u / x ]_ B )
14 sneq 
 |-  ( x = u -> { x } = { u } )
15 csbeq1a 
 |-  ( x = u -> B = [_ u / x ]_ B )
16 14 15 xpeq12d 
 |-  ( x = u -> ( { x } X. B ) = ( { u } X. [_ u / x ]_ B ) )
17 10 13 16 cbviun 
 |-  U_ x e. A ( { x } X. B ) = U_ u e. A ( { u } X. [_ u / x ]_ B )
18 17 mpteq1i 
 |-  ( z e. U_ x e. A ( { x } X. B ) |-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C ) = ( z e. U_ u e. A ( { u } X. [_ u / x ]_ B ) |-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C )
19 nfcv 
 |-  F/_ u B
20 nfcv 
 |-  F/_ u C
21 nfcv 
 |-  F/_ v C
22 nfcsb1v 
 |-  F/_ x [_ u / x ]_ [_ v / y ]_ C
23 nfcv 
 |-  F/_ y u
24 nfcsb1v 
 |-  F/_ y [_ v / y ]_ C
25 23 24 nfcsbw 
 |-  F/_ y [_ u / x ]_ [_ v / y ]_ C
26 csbeq1a 
 |-  ( y = v -> C = [_ v / y ]_ C )
27 csbeq1a 
 |-  ( x = u -> [_ v / y ]_ C = [_ u / x ]_ [_ v / y ]_ C )
28 26 27 sylan9eqr 
 |-  ( ( x = u /\ y = v ) -> C = [_ u / x ]_ [_ v / y ]_ C )
29 19 12 20 21 22 25 15 28 cbvmpox 
 |-  ( x e. A , y e. B |-> C ) = ( u e. A , v e. [_ u / x ]_ B |-> [_ u / x ]_ [_ v / y ]_ C )
30 9 18 29 3eqtr4ri 
 |-  ( x e. A , y e. B |-> C ) = ( z e. U_ x e. A ( { x } X. B ) |-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C )