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 ) ) ) )
8 1 adantr 
 |-  ( ( ph /\ f e. ( ( J tX K ) Cn L ) ) -> J e. ( TopOn ` X ) )
9 2 adantr 
 |-  ( ( 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 ) ) )
12 11 adantr 
 |-  ( ( 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 ) )
15 14 adantr 
 |-  ( ( 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 ) ) )
24 23 adantrr 
 |-  ( ( 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 ) ) )
26 21 adantrr 
 |-  ( ( 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 )
49 48 ad2antrr 
 |-  ( ( ( 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 ) ) )
73 1 adantr 
 |-  ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) -> J e. ( TopOn ` X ) )
74 2 adantr 
 |-  ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) -> K e. ( TopOn ` Y ) )
75 14 adantr 
 |-  ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) -> L e. ( TopOn ` U. L ) )
76 5 adantr 
 |-  ( ( 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 )
79 6 adantr 
 |-  ( ( 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 ) ) )
87 2 ad2antrr 
 |-  ( ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) /\ x e. X ) -> K e. ( TopOn ` Y ) )
88 14 ad2antrr 
 |-  ( ( ( ph /\ g e. ( J Cn ( L ^ko K ) ) ) /\ x e. X ) -> L e. ( TopOn ` U. L ) )
89 85 ffvelcdmda 
 |-  ( ( ( 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 ) )
97 96 adantrr 
 |-  ( ( 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 ) )
99 94 adantrr 
 |-  ( ( 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 ) ) ) )