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 A × B x -1
xpcomco.1 G = y B , z A C
Assertion xpcomco G F = z A , y B C

Proof

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