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

Metamath Proof Explorer

Theorem mpomptxf

Description: Express a two-argument function as a one-argument function, or vice-versa. In this version B ( x ) is not assumed to be constant w.r.t x . (Contributed by Mario Carneiro, 29-Dec-2014) (Revised by Thierry Arnoux, 31-Mar-2018)

Ref Expression
Hypotheses mpomptxf.0 
|- F/_ x C
mpomptxf.1 
|- F/_ y C
mpomptxf.2 
|- ( z = <. x , y >. -> C = D )
Assertion mpomptxf 
|- ( z e. U_ x e. A ( { x } X. B ) |-> C ) = ( x e. A , y e. B |-> D )

Proof

Step Hyp Ref Expression
1 mpomptxf.0 
 |-  F/_ x C
2 mpomptxf.1 
 |-  F/_ y C
3 mpomptxf.2 
 |-  ( z = <. x , y >. -> C = D )
4 df-mpt 
 |-  ( z e. U_ x e. A ( { x } X. B ) |-> C ) = { <. z , w >. | ( z e. U_ x e. A ( { x } X. B ) /\ w = C ) }
5 df-mpo 
 |-  ( x e. A , y e. B |-> D ) = { <. <. x , y >. , w >. | ( ( x e. A /\ y e. B ) /\ w = D ) }
6 eliunxp 
 |-  ( z e. U_ x e. A ( { x } X. B ) <-> E. x E. y ( z = <. x , y >. /\ ( x e. A /\ y e. B ) ) )
7 6 anbi1i 
 |-  ( ( z e. U_ x e. A ( { x } X. B ) /\ w = C ) <-> ( E. x E. y ( z = <. x , y >. /\ ( x e. A /\ y e. B ) ) /\ w = C ) )
8 2 nfeq2 
 |-  F/ y w = C
9 8 19.41 
 |-  ( E. y ( ( z = <. x , y >. /\ ( x e. A /\ y e. B ) ) /\ w = C ) <-> ( E. y ( z = <. x , y >. /\ ( x e. A /\ y e. B ) ) /\ w = C ) )
10 9 exbii 
 |-  ( E. x E. y ( ( z = <. x , y >. /\ ( x e. A /\ y e. B ) ) /\ w = C ) <-> E. x ( E. y ( z = <. x , y >. /\ ( x e. A /\ y e. B ) ) /\ w = C ) )
11 1 nfeq2 
 |-  F/ x w = C
12 11 19.41 
 |-  ( E. x ( E. y ( z = <. x , y >. /\ ( x e. A /\ y e. B ) ) /\ w = C ) <-> ( E. x E. y ( z = <. x , y >. /\ ( x e. A /\ y e. B ) ) /\ w = C ) )
13 10 12 bitri 
 |-  ( E. x E. y ( ( z = <. x , y >. /\ ( x e. A /\ y e. B ) ) /\ w = C ) <-> ( E. x E. y ( z = <. x , y >. /\ ( x e. A /\ y e. B ) ) /\ w = C ) )
14 anass 
 |-  ( ( ( z = <. x , y >. /\ ( x e. A /\ y e. B ) ) /\ w = C ) <-> ( z = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) )
15 3 eqeq2d 
 |-  ( z = <. x , y >. -> ( w = C <-> w = D ) )
16 15 anbi2d 
 |-  ( z = <. x , y >. -> ( ( ( x e. A /\ y e. B ) /\ w = C ) <-> ( ( x e. A /\ y e. B ) /\ w = D ) ) )
17 16 pm5.32i 
 |-  ( ( z = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) <-> ( z = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ w = D ) ) )
18 14 17 bitri 
 |-  ( ( ( z = <. x , y >. /\ ( x e. A /\ y e. B ) ) /\ w = C ) <-> ( z = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ w = D ) ) )
19 18 2exbii 
 |-  ( E. x E. y ( ( z = <. x , y >. /\ ( x e. A /\ y e. B ) ) /\ w = C ) <-> E. x E. y ( z = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ w = D ) ) )
20 7 13 19 3bitr2i 
 |-  ( ( z e. U_ x e. A ( { x } X. B ) /\ w = C ) <-> E. x E. y ( z = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ w = D ) ) )
21 20 opabbii 
 |-  { <. z , w >. | ( z e. U_ x e. A ( { x } X. B ) /\ w = C ) } = { <. z , w >. | E. x E. y ( z = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ w = D ) ) }
22 dfoprab2 
 |-  { <. <. x , y >. , w >. | ( ( x e. A /\ y e. B ) /\ w = D ) } = { <. z , w >. | E. x E. y ( z = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ w = D ) ) }
23 21 22 eqtr4i 
 |-  { <. z , w >. | ( z e. U_ x e. A ( { x } X. B ) /\ w = C ) } = { <. <. x , y >. , w >. | ( ( x e. A /\ y e. B ) /\ w = D ) }
24 5 23 eqtr4i 
 |-  ( x e. A , y e. B |-> D ) = { <. z , w >. | ( z e. U_ x e. A ( { x } X. B ) /\ w = C ) }
25 4 24 eqtr4i 
 |-  ( z e. U_ x e. A ( { x } X. B ) |-> C ) = ( x e. A , y e. B |-> D )