# Metamath Proof Explorer

## Theorem xkocnv

Description: The inverse of the "currying" function F is the uncurrying function. (Contributed by Mario Carneiro, 13-Apr-2015)

Ref Expression
Hypotheses xkohmeo.x
|- ( ph -> J e. ( TopOn ` X ) )
xkohmeo.y
|- ( ph -> K e. ( TopOn ` Y ) )
xkohmeo.f
|- F = ( f e. ( ( J tX K ) Cn L ) |-> ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) )
xkohmeo.j
|- ( ph -> J e. N-Locally Comp )
xkohmeo.k
|- ( ph -> K e. N-Locally Comp )
xkohmeo.l
|- ( ph -> L e. Top )
Assertion xkocnv
|- ( ph -> `' F = ( g e. ( J Cn ( L ^ko K ) ) |-> ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) )

### Proof

Step Hyp Ref Expression
1 xkohmeo.x
|-  ( ph -> J e. ( TopOn ` X ) )
2 xkohmeo.y
|-  ( ph -> K e. ( TopOn ` Y ) )
3 xkohmeo.f
|-  F = ( f e. ( ( J tX K ) Cn L ) |-> ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) )
4 xkohmeo.j
|-  ( ph -> J e. N-Locally Comp )
5 xkohmeo.k
|-  ( ph -> K e. N-Locally Comp )
6 xkohmeo.l
|-  ( ph -> L e. Top )
7 simprr
|-  ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) -> g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) )
|-  ( ( ph /\ f e. ( ( J tX K ) Cn L ) ) -> J e. ( TopOn ` X ) )
|-  ( ( ph /\ f e. ( ( J tX K ) Cn L ) ) -> K e. ( TopOn ` Y ) )
10 txtopon
|-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
11 1 2 10 syl2anc
|-  ( ph -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
|-  ( ( ph /\ f e. ( ( J tX K ) Cn L ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
13 toptopon2
|-  ( L e. Top <-> L e. ( TopOn ` U. L ) )
14 6 13 sylib
|-  ( ph -> L e. ( TopOn ` U. L ) )
|-  ( ( ph /\ f e. ( ( J tX K ) Cn L ) ) -> L e. ( TopOn ` U. L ) )
16 simpr
|-  ( ( ph /\ f e. ( ( J tX K ) Cn L ) ) -> f e. ( ( J tX K ) Cn L ) )
17 cnf2
|-  ( ( ( J tX K ) e. ( TopOn ` ( X X. Y ) ) /\ L e. ( TopOn ` U. L ) /\ f e. ( ( J tX K ) Cn L ) ) -> f : ( X X. Y ) --> U. L )
18 12 15 16 17 syl3anc
|-  ( ( ph /\ f e. ( ( J tX K ) Cn L ) ) -> f : ( X X. Y ) --> U. L )
19 18 ffnd
|-  ( ( ph /\ f e. ( ( J tX K ) Cn L ) ) -> f Fn ( X X. Y ) )
20 fnov
|-  ( f Fn ( X X. Y ) <-> f = ( x e. X , y e. Y |-> ( x f y ) ) )
21 19 20 sylib
|-  ( ( ph /\ f e. ( ( J tX K ) Cn L ) ) -> f = ( x e. X , y e. Y |-> ( x f y ) ) )
22 21 16 eqeltrrd
|-  ( ( ph /\ f e. ( ( J tX K ) Cn L ) ) -> ( x e. X , y e. Y |-> ( x f y ) ) e. ( ( J tX K ) Cn L ) )
23 8 9 22 cnmpt2k
|-  ( ( ph /\ f e. ( ( J tX K ) Cn L ) ) -> ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) e. ( J Cn ( L ^ko K ) ) )
|-  ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) -> ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) e. ( J Cn ( L ^ko K ) ) )
25 7 24 eqeltrd
|-  ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) -> g e. ( J Cn ( L ^ko K ) ) )
|-  ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) -> f = ( x e. X , y e. Y |-> ( x f y ) ) )
27 eqid
|-  X = X
28 nfv
|-  F/ x ph
29 nfv
|-  F/ x f e. ( ( J tX K ) Cn L )
30 nfmpt1
|-  F/_ x ( x e. X |-> ( y e. Y |-> ( x f y ) ) )
31 30 nfeq2
|-  F/ x g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) )
32 29 31 nfan
|-  F/ x ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) )
33 28 32 nfan
|-  F/ x ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) )
34 nfv
|-  F/ y ph
35 nfv
|-  F/ y f e. ( ( J tX K ) Cn L )
36 nfcv
|-  F/_ y X
37 nfmpt1
|-  F/_ y ( y e. Y |-> ( x f y ) )
38 36 37 nfmpt
|-  F/_ y ( x e. X |-> ( y e. Y |-> ( x f y ) ) )
39 38 nfeq2
|-  F/ y g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) )
40 35 39 nfan
|-  F/ y ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) )
41 34 40 nfan
|-  F/ y ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) )
42 nfv
|-  F/ y x e. X
43 41 42 nfan
|-  F/ y ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) /\ x e. X )
44 simplrr
|-  ( ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) /\ ( x e. X /\ y e. Y ) ) -> g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) )
45 44 fveq1d
|-  ( ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) /\ ( x e. X /\ y e. Y ) ) -> ( g ` x ) = ( ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ` x ) )
46 simprl
|-  ( ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) /\ ( x e. X /\ y e. Y ) ) -> x e. X )
47 toponmax
|-  ( K e. ( TopOn ` Y ) -> Y e. K )
48 2 47 syl
|-  ( ph -> Y e. K )
|-  ( ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) /\ ( x e. X /\ y e. Y ) ) -> Y e. K )
50 49 mptexd
|-  ( ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) /\ ( x e. X /\ y e. Y ) ) -> ( y e. Y |-> ( x f y ) ) e. _V )
51 eqid
|-  ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) = ( x e. X |-> ( y e. Y |-> ( x f y ) ) )
52 51 fvmpt2
|-  ( ( x e. X /\ ( y e. Y |-> ( x f y ) ) e. _V ) -> ( ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ` x ) = ( y e. Y |-> ( x f y ) ) )
53 46 50 52 syl2anc
|-  ( ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) /\ ( x e. X /\ y e. Y ) ) -> ( ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ` x ) = ( y e. Y |-> ( x f y ) ) )
54 45 53 eqtrd
|-  ( ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) /\ ( x e. X /\ y e. Y ) ) -> ( g ` x ) = ( y e. Y |-> ( x f y ) ) )
55 54 fveq1d
|-  ( ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) /\ ( x e. X /\ y e. Y ) ) -> ( ( g ` x ) ` y ) = ( ( y e. Y |-> ( x f y ) ) ` y ) )
56 simprr
|-  ( ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) /\ ( x e. X /\ y e. Y ) ) -> y e. Y )
57 ovex
|-  ( x f y ) e. _V
58 eqid
|-  ( y e. Y |-> ( x f y ) ) = ( y e. Y |-> ( x f y ) )
59 58 fvmpt2
|-  ( ( y e. Y /\ ( x f y ) e. _V ) -> ( ( y e. Y |-> ( x f y ) ) ` y ) = ( x f y ) )
60 56 57 59 sylancl
|-  ( ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) /\ ( x e. X /\ y e. Y ) ) -> ( ( y e. Y |-> ( x f y ) ) ` y ) = ( x f y ) )
61 55 60 eqtrd
|-  ( ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) /\ ( x e. X /\ y e. Y ) ) -> ( ( g ` x ) ` y ) = ( x f y ) )
62 61 expr
|-  ( ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) /\ x e. X ) -> ( y e. Y -> ( ( g ` x ) ` y ) = ( x f y ) ) )
63 43 62 ralrimi
|-  ( ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) /\ x e. X ) -> A. y e. Y ( ( g ` x ) ` y ) = ( x f y ) )
64 eqid
|-  Y = Y
65 63 64 jctil
|-  ( ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) /\ x e. X ) -> ( Y = Y /\ A. y e. Y ( ( g ` x ) ` y ) = ( x f y ) ) )
66 65 ex
|-  ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) -> ( x e. X -> ( Y = Y /\ A. y e. Y ( ( g ` x ) ` y ) = ( x f y ) ) ) )
67 33 66 ralrimi
|-  ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) -> A. x e. X ( Y = Y /\ A. y e. Y ( ( g ` x ) ` y ) = ( x f y ) ) )
68 mpoeq123
|-  ( ( X = X /\ A. x e. X ( Y = Y /\ A. y e. Y ( ( g ` x ) ` y ) = ( x f y ) ) ) -> ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) = ( x e. X , y e. Y |-> ( x f y ) ) )
69 27 67 68 sylancr
|-  ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) -> ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) = ( x e. X , y e. Y |-> ( x f y ) ) )
70 26 69 eqtr4d
|-  ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) -> f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) )
71 25 70 jca
|-  ( ( ph /\ ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) ) -> ( g e. ( J Cn ( L ^ko K ) ) /\ f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) )
72 simprr
|-  ( ( ph /\ ( g e. ( J Cn ( L ^ko K ) ) /\ f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) ) -> f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) )
|-  ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) -> J e. ( TopOn ` X ) )
|-  ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) -> K e. ( TopOn ` Y ) )
|-  ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) -> L e. ( TopOn ` U. L ) )
|-  ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) -> K e. N-Locally Comp )
77 nllytop
|-  ( K e. N-Locally Comp -> K e. Top )
78 76 77 syl
|-  ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) -> K e. Top )
|-  ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) -> L e. Top )
80 eqid
|-  ( L ^ko K ) = ( L ^ko K )
81 80 xkotopon
|-  ( ( K e. Top /\ L e. Top ) -> ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) )
82 78 79 81 syl2anc
|-  ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) -> ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) )
83 simpr
|-  ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) -> g e. ( J Cn ( L ^ko K ) ) )
84 cnf2
|-  ( ( J e. ( TopOn ` X ) /\ ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) /\ g e. ( J Cn ( L ^ko K ) ) ) -> g : X --> ( K Cn L ) )
85 73 82 83 84 syl3anc
|-  ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) -> g : X --> ( K Cn L ) )
86 85 feqmptd
|-  ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) -> g = ( x e. X |-> ( g ` x ) ) )
|-  ( ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) /\ x e. X ) -> K e. ( TopOn ` Y ) )
|-  ( ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) /\ x e. X ) -> L e. ( TopOn ` U. L ) )
89 85 ffvelrnda
|-  ( ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) /\ x e. X ) -> ( g ` x ) e. ( K Cn L ) )
90 cnf2
|-  ( ( K e. ( TopOn ` Y ) /\ L e. ( TopOn ` U. L ) /\ ( g ` x ) e. ( K Cn L ) ) -> ( g ` x ) : Y --> U. L )
91 87 88 89 90 syl3anc
|-  ( ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) /\ x e. X ) -> ( g ` x ) : Y --> U. L )
92 91 feqmptd
|-  ( ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) /\ x e. X ) -> ( g ` x ) = ( y e. Y |-> ( ( g ` x ) ` y ) ) )
93 92 mpteq2dva
|-  ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) -> ( x e. X |-> ( g ` x ) ) = ( x e. X |-> ( y e. Y |-> ( ( g ` x ) ` y ) ) ) )
94 86 93 eqtrd
|-  ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) -> g = ( x e. X |-> ( y e. Y |-> ( ( g ` x ) ` y ) ) ) )
95 94 83 eqeltrrd
|-  ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) -> ( x e. X |-> ( y e. Y |-> ( ( g ` x ) ` y ) ) ) e. ( J Cn ( L ^ko K ) ) )
96 73 74 75 76 95 cnmptk2
|-  ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) -> ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) e. ( ( J tX K ) Cn L ) )
|-  ( ( ph /\ ( g e. ( J Cn ( L ^ko K ) ) /\ f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) ) -> ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) e. ( ( J tX K ) Cn L ) )
98 72 97 eqeltrd
|-  ( ( ph /\ ( g e. ( J Cn ( L ^ko K ) ) /\ f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) ) -> f e. ( ( J tX K ) Cn L ) )
|-  ( ( ph /\ ( g e. ( J Cn ( L ^ko K ) ) /\ f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) ) -> g = ( x e. X |-> ( y e. Y |-> ( ( g ` x ) ` y ) ) ) )
100 nfv
|-  F/ x g e. ( J Cn ( L ^ko K ) )
101 nfmpo1
|-  F/_ x ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) )
102 101 nfeq2
|-  F/ x f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) )
103 100 102 nfan
|-  F/ x ( g e. ( J Cn ( L ^ko K ) ) /\ f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) )
104 28 103 nfan
|-  F/ x ( ph /\ ( g e. ( J Cn ( L ^ko K ) ) /\ f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) )
105 nfv
|-  F/ y g e. ( J Cn ( L ^ko K ) )
106 nfmpo2
|-  F/_ y ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) )
107 106 nfeq2
|-  F/ y f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) )
108 105 107 nfan
|-  F/ y ( g e. ( J Cn ( L ^ko K ) ) /\ f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) )
109 34 108 nfan
|-  F/ y ( ph /\ ( g e. ( J Cn ( L ^ko K ) ) /\ f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) )
110 109 42 nfan
|-  F/ y ( ( ph /\ ( g e. ( J Cn ( L ^ko K ) ) /\ f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) ) /\ x e. X )
111 72 oveqd
|-  ( ( ph /\ ( g e. ( J Cn ( L ^ko K ) ) /\ f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) ) -> ( x f y ) = ( x ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) y ) )
112 fvex
|-  ( ( g ` x ) ` y ) e. _V
113 eqid
|-  ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) )
114 113 ovmpt4g
|-  ( ( x e. X /\ y e. Y /\ ( ( g ` x ) ` y ) e. _V ) -> ( x ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) y ) = ( ( g ` x ) ` y ) )
115 112 114 mp3an3
|-  ( ( x e. X /\ y e. Y ) -> ( x ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) y ) = ( ( g ` x ) ` y ) )
116 111 115 sylan9eq
|-  ( ( ( ph /\ ( g e. ( J Cn ( L ^ko K ) ) /\ f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) ) /\ ( x e. X /\ y e. Y ) ) -> ( x f y ) = ( ( g ` x ) ` y ) )
117 116 expr
|-  ( ( ( ph /\ ( g e. ( J Cn ( L ^ko K ) ) /\ f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) ) /\ x e. X ) -> ( y e. Y -> ( x f y ) = ( ( g ` x ) ` y ) ) )
118 110 117 ralrimi
|-  ( ( ( ph /\ ( g e. ( J Cn ( L ^ko K ) ) /\ f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) ) /\ x e. X ) -> A. y e. Y ( x f y ) = ( ( g ` x ) ` y ) )
119 mpteq12
|-  ( ( Y = Y /\ A. y e. Y ( x f y ) = ( ( g ` x ) ` y ) ) -> ( y e. Y |-> ( x f y ) ) = ( y e. Y |-> ( ( g ` x ) ` y ) ) )
120 64 118 119 sylancr
|-  ( ( ( ph /\ ( g e. ( J Cn ( L ^ko K ) ) /\ f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) ) /\ x e. X ) -> ( y e. Y |-> ( x f y ) ) = ( y e. Y |-> ( ( g ` x ) ` y ) ) )
121 104 120 mpteq2da
|-  ( ( ph /\ ( g e. ( J Cn ( L ^ko K ) ) /\ f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) ) -> ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) = ( x e. X |-> ( y e. Y |-> ( ( g ` x ) ` y ) ) ) )
122 99 121 eqtr4d
|-  ( ( ph /\ ( g e. ( J Cn ( L ^ko K ) ) /\ f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) ) -> g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) )
123 98 122 jca
|-  ( ( ph /\ ( g e. ( J Cn ( L ^ko K ) ) /\ f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) ) -> ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) )
124 71 123 impbida
|-  ( ph -> ( ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) <-> ( g e. ( J Cn ( L ^ko K ) ) /\ f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) ) )
125 124 opabbidv
|-  ( ph -> { <. g , f >. | ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) } = { <. g , f >. | ( g e. ( J Cn ( L ^ko K ) ) /\ f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) } )
126 df-mpt
|-  ( f e. ( ( J tX K ) Cn L ) |-> ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) = { <. f , g >. | ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) }
127 3 126 eqtri
|-  F = { <. f , g >. | ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) }
128 127 cnveqi
|-  `' F = `' { <. f , g >. | ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) }
129 cnvopab
|-  `' { <. f , g >. | ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) } = { <. g , f >. | ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) }
130 128 129 eqtri
|-  `' F = { <. g , f >. | ( f e. ( ( J tX K ) Cn L ) /\ g = ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) }
131 df-mpt
|-  ( g e. ( J Cn ( L ^ko K ) ) |-> ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) = { <. g , f >. | ( g e. ( J Cn ( L ^ko K ) ) /\ f = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) }
132 125 130 131 3eqtr4g
|-  ( ph -> `' F = ( g e. ( J Cn ( L ^ko K ) ) |-> ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) )