Metamath Proof Explorer

Theorem xpcomco

Description: Composition with the bijection of xpcomf1o swaps the arguments to a mapping. (Contributed by Mario Carneiro, 30-May-2015)

Ref Expression
Hypotheses xpcomf1o.1 
|- F = ( x e. ( A X. B ) |-> U. `' { x } )
xpcomco.1 
|- G = ( y e. B , z e. A |-> C )
Assertion xpcomco 
|- ( G o. F ) = ( z e. A , y e. B |-> C )

Proof

Step Hyp Ref Expression
1 xpcomf1o.1 
 |-  F = ( x e. ( A X. B ) |-> U. `' { x } )
2 xpcomco.1 
 |-  G = ( y e. B , z e. A |-> C )
3 1 xpcomf1o 
 |-  F : ( A X. B ) -1-1-onto-> ( B X. A )
4 f1ofun 
 |-  ( F : ( A X. B ) -1-1-onto-> ( B X. A ) -> Fun F )
5 funbrfv2b 
 |-  ( Fun F -> ( u F w <-> ( u e. dom F /\ ( F ` u ) = w ) ) )
6 3 4 5 mp2b 
 |-  ( u F w <-> ( u e. dom F /\ ( F ` u ) = w ) )
7 ancom 
 |-  ( ( u e. dom F /\ ( F ` u ) = w ) <-> ( ( F ` u ) = w /\ u e. dom F ) )
8 eqcom 
 |-  ( ( F ` u ) = w <-> w = ( F ` u ) )
9 f1odm 
 |-  ( F : ( A X. B ) -1-1-onto-> ( B X. A ) -> dom F = ( A X. B ) )
10 3 9 ax-mp 
 |-  dom F = ( A X. B )
11 10 eleq2i 
 |-  ( u e. dom F <-> u e. ( A X. B ) )
12 8 11 anbi12i 
 |-  ( ( ( F ` u ) = w /\ u e. dom F ) <-> ( w = ( F ` u ) /\ u e. ( A X. B ) ) )
13 6 7 12 3bitri 
 |-  ( u F w <-> ( w = ( F ` u ) /\ u e. ( A X. B ) ) )
14 13 anbi1i 
 |-  ( ( u F w /\ w G v ) <-> ( ( w = ( F ` u ) /\ u e. ( A X. B ) ) /\ w G v ) )
15 anass 
 |-  ( ( ( w = ( F ` u ) /\ u e. ( A X. B ) ) /\ w G v ) <-> ( w = ( F ` u ) /\ ( u e. ( A X. B ) /\ w G v ) ) )
16 14 15 bitri 
 |-  ( ( u F w /\ w G v ) <-> ( w = ( F ` u ) /\ ( u e. ( A X. B ) /\ w G v ) ) )
17 16 exbii 
 |-  ( E. w ( u F w /\ w G v ) <-> E. w ( w = ( F ` u ) /\ ( u e. ( A X. B ) /\ w G v ) ) )
18 fvex 
 |-  ( F ` u ) e. _V
19 breq1 
 |-  ( w = ( F ` u ) -> ( w G v <-> ( F ` u ) G v ) )
20 19 anbi2d 
 |-  ( w = ( F ` u ) -> ( ( u e. ( A X. B ) /\ w G v ) <-> ( u e. ( A X. B ) /\ ( F ` u ) G v ) ) )
21 18 20 ceqsexv 
 |-  ( E. w ( w = ( F ` u ) /\ ( u e. ( A X. B ) /\ w G v ) ) <-> ( u e. ( A X. B ) /\ ( F ` u ) G v ) )
22 elxp 
 |-  ( u e. ( A X. B ) <-> E. z E. y ( u = <. z , y >. /\ ( z e. A /\ y e. B ) ) )
23 22 anbi1i 
 |-  ( ( u e. ( A X. B ) /\ ( F ` u ) G v ) <-> ( E. z E. y ( u = <. z , y >. /\ ( z e. A /\ y e. B ) ) /\ ( F ` u ) G v ) )
24 nfcv 
 |-  F/_ z ( F ` u )
25 nfmpo2 
 |-  F/_ z ( y e. B , z e. A |-> C )
26 2 25 nfcxfr 
 |-  F/_ z G
27 nfcv 
 |-  F/_ z v
28 24 26 27 nfbr 
 |-  F/ z ( F ` u ) G v
29 28 19.41 
 |-  ( E. z ( E. y ( u = <. z , y >. /\ ( z e. A /\ y e. B ) ) /\ ( F ` u ) G v ) <-> ( E. z E. y ( u = <. z , y >. /\ ( z e. A /\ y e. B ) ) /\ ( F ` u ) G v ) )
30 nfcv 
 |-  F/_ y ( F ` u )
31 nfmpo1 
 |-  F/_ y ( y e. B , z e. A |-> C )
32 2 31 nfcxfr 
 |-  F/_ y G
33 nfcv 
 |-  F/_ y v
34 30 32 33 nfbr 
 |-  F/ y ( F ` u ) G v
35 34 19.41 
 |-  ( E. y ( ( u = <. z , y >. /\ ( z e. A /\ y e. B ) ) /\ ( F ` u ) G v ) <-> ( E. y ( u = <. z , y >. /\ ( z e. A /\ y e. B ) ) /\ ( F ` u ) G v ) )
36 anass 
 |-  ( ( ( u = <. z , y >. /\ ( z e. A /\ y e. B ) ) /\ ( F ` u ) G v ) <-> ( u = <. z , y >. /\ ( ( z e. A /\ y e. B ) /\ ( F ` u ) G v ) ) )
37 fveq2 
 |-  ( u = <. z , y >. -> ( F ` u ) = ( F ` <. z , y >. ) )
38 opelxpi 
 |-  ( ( z e. A /\ y e. B ) -> <. z , y >. e. ( A X. B ) )
39 sneq 
 |-  ( x = <. z , y >. -> { x } = { <. z , y >. } )
40 39 cnveqd 
 |-  ( x = <. z , y >. -> `' { x } = `' { <. z , y >. } )
41 40 unieqd 
 |-  ( x = <. z , y >. -> U. `' { x } = U. `' { <. z , y >. } )
42 opswap 
 |-  U. `' { <. z , y >. } = <. y , z >.
43 41 42 eqtrdi 
 |-  ( x = <. z , y >. -> U. `' { x } = <. y , z >. )
44 opex 
 |-  <. y , z >. e. _V
45 43 1 44 fvmpt 
 |-  ( <. z , y >. e. ( A X. B ) -> ( F ` <. z , y >. ) = <. y , z >. )
46 38 45 syl 
 |-  ( ( z e. A /\ y e. B ) -> ( F ` <. z , y >. ) = <. y , z >. )
47 37 46 sylan9eq 
 |-  ( ( u = <. z , y >. /\ ( z e. A /\ y e. B ) ) -> ( F ` u ) = <. y , z >. )
48 47 breq1d 
 |-  ( ( u = <. z , y >. /\ ( z e. A /\ y e. B ) ) -> ( ( F ` u ) G v <-> <. y , z >. G v ) )
49 df-br 
 |-  ( <. y , z >. G v <-> <. <. y , z >. , v >. e. G )
50 df-mpo 
 |-  ( y e. B , z e. A |-> C ) = { <. <. y , z >. , v >. | ( ( y e. B /\ z e. A ) /\ v = C ) }
51 2 50 eqtri 
 |-  G = { <. <. y , z >. , v >. | ( ( y e. B /\ z e. A ) /\ v = C ) }
52 51 eleq2i 
 |-  ( <. <. y , z >. , v >. e. G <-> <. <. y , z >. , v >. e. { <. <. y , z >. , v >. | ( ( y e. B /\ z e. A ) /\ v = C ) } )
53 oprabidw 
 |-  ( <. <. y , z >. , v >. e. { <. <. y , z >. , v >. | ( ( y e. B /\ z e. A ) /\ v = C ) } <-> ( ( y e. B /\ z e. A ) /\ v = C ) )
54 49 52 53 3bitri 
 |-  ( <. y , z >. G v <-> ( ( y e. B /\ z e. A ) /\ v = C ) )
55 54 baib 
 |-  ( ( y e. B /\ z e. A ) -> ( <. y , z >. G v <-> v = C ) )
56 55 ancoms 
 |-  ( ( z e. A /\ y e. B ) -> ( <. y , z >. G v <-> v = C ) )
57 56 adantl 
 |-  ( ( u = <. z , y >. /\ ( z e. A /\ y e. B ) ) -> ( <. y , z >. G v <-> v = C ) )
58 48 57 bitrd 
 |-  ( ( u = <. z , y >. /\ ( z e. A /\ y e. B ) ) -> ( ( F ` u ) G v <-> v = C ) )
59 58 pm5.32da 
 |-  ( u = <. z , y >. -> ( ( ( z e. A /\ y e. B ) /\ ( F ` u ) G v ) <-> ( ( z e. A /\ y e. B ) /\ v = C ) ) )
60 59 pm5.32i 
 |-  ( ( u = <. z , y >. /\ ( ( z e. A /\ y e. B ) /\ ( F ` u ) G v ) ) <-> ( u = <. z , y >. /\ ( ( z e. A /\ y e. B ) /\ v = C ) ) )
61 36 60 bitri 
 |-  ( ( ( u = <. z , y >. /\ ( z e. A /\ y e. B ) ) /\ ( F ` u ) G v ) <-> ( u = <. z , y >. /\ ( ( z e. A /\ y e. B ) /\ v = C ) ) )
62 61 exbii 
 |-  ( E. y ( ( u = <. z , y >. /\ ( z e. A /\ y e. B ) ) /\ ( F ` u ) G v ) <-> E. y ( u = <. z , y >. /\ ( ( z e. A /\ y e. B ) /\ v = C ) ) )
63 35 62 bitr3i 
 |-  ( ( E. y ( u = <. z , y >. /\ ( z e. A /\ y e. B ) ) /\ ( F ` u ) G v ) <-> E. y ( u = <. z , y >. /\ ( ( z e. A /\ y e. B ) /\ v = C ) ) )
64 63 exbii 
 |-  ( E. z ( E. y ( u = <. z , y >. /\ ( z e. A /\ y e. B ) ) /\ ( F ` u ) G v ) <-> E. z E. y ( u = <. z , y >. /\ ( ( z e. A /\ y e. B ) /\ v = C ) ) )
65 23 29 64 3bitr2i 
 |-  ( ( u e. ( A X. B ) /\ ( F ` u ) G v ) <-> E. z E. y ( u = <. z , y >. /\ ( ( z e. A /\ y e. B ) /\ v = C ) ) )
66 17 21 65 3bitri 
 |-  ( E. w ( u F w /\ w G v ) <-> E. z E. y ( u = <. z , y >. /\ ( ( z e. A /\ y e. B ) /\ v = C ) ) )
67 66 opabbii 
 |-  { <. u , v >. | E. w ( u F w /\ w G v ) } = { <. u , v >. | E. z E. y ( u = <. z , y >. /\ ( ( z e. A /\ y e. B ) /\ v = C ) ) }
68 df-co 
 |-  ( G o. F ) = { <. u , v >. | E. w ( u F w /\ w G v ) }
69 df-mpo 
 |-  ( z e. A , y e. B |-> C ) = { <. <. z , y >. , v >. | ( ( z e. A /\ y e. B ) /\ v = C ) }
70 dfoprab2 
 |-  { <. <. z , y >. , v >. | ( ( z e. A /\ y e. B ) /\ v = C ) } = { <. u , v >. | E. z E. y ( u = <. z , y >. /\ ( ( z e. A /\ y e. B ) /\ v = C ) ) }
71 69 70 eqtri 
 |-  ( z e. A , y e. B |-> C ) = { <. u , v >. | E. z E. y ( u = <. z , y >. /\ ( ( z e. A /\ y e. B ) /\ v = C ) ) }
72 67 68 71 3eqtr4i 
 |-  ( G o. F ) = ( z e. A , y e. B |-> C )