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 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
xkohmeo.y ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
xkohmeo.f ⊢ 𝐹 = ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) )
xkohmeo.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑛-Locally Comp )
xkohmeo.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑛-Locally Comp )
xkohmeo.l ⊢ ( 𝜑 → 𝐿 ∈ Top )
Assertion xkocnv ( 𝜑 → ◡ 𝐹 = ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ↦ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 xkohmeo.x ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 xkohmeo.y ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3 xkohmeo.f ⊢ 𝐹 = ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) )
4 xkohmeo.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑛-Locally Comp )
5 xkohmeo.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑛-Locally Comp )
6 xkohmeo.l ⊢ ( 𝜑 → 𝐿 ∈ Top )
7 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) → 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) )
8 1 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
9 2 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
10 txtopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
11 1 2 10 syl2anc ⊢ ( 𝜑 → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ) → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
13 toptopon2 ⊢ ( 𝐿 ∈ Top ↔ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
14 6 13 sylib ⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ) → 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
16 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ) → 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )
17 cnf2 ⊢ ( ( ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) ∧ 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ) → 𝑓 : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝐿 )
18 12 15 16 17 syl3anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ) → 𝑓 : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝐿 )
19 18 ffnd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ) → 𝑓 Fn ( 𝑋 × 𝑌 ) )
20 fnov ⊢ ( 𝑓 Fn ( 𝑋 × 𝑌 ) ↔ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) )
21 19 20 sylib ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ) → 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) )
22 21 16 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )
23 8 9 22 cnmpt2k ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) )
24 23 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) )
25 7 24 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) → 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) )
26 21 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) → 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) )
27 eqid ⊢ 𝑋 = 𝑋
28 nfv ⊢ Ⅎ 𝑥 𝜑
29 nfv ⊢ Ⅎ 𝑥 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 )
30 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) )
31 30 nfeq2 ⊢ Ⅎ 𝑥 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) )
32 29 31 nfan ⊢ Ⅎ 𝑥 ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) )
33 28 32 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) )
34 nfv ⊢ Ⅎ 𝑦 𝜑
35 nfv ⊢ Ⅎ 𝑦 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 )
36 nfcv ⊢ Ⅎ 𝑦 𝑋
37 nfmpt1 ⊢ Ⅎ 𝑦 ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) )
38 36 37 nfmpt ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) )
39 38 nfeq2 ⊢ Ⅎ 𝑦 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) )
40 35 39 nfan ⊢ Ⅎ 𝑦 ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) )
41 34 40 nfan ⊢ Ⅎ 𝑦 ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) )
42 nfv ⊢ Ⅎ 𝑦 𝑥 ∈ 𝑋
43 41 42 nfan ⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) ∧ 𝑥 ∈ 𝑋 )
44 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) )
45 44 fveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑔 ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ‘ 𝑥 ) )
46 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → 𝑥 ∈ 𝑋 )
47 toponmax ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 ∈ 𝐾 )
48 2 47 syl ⊢ ( 𝜑 → 𝑌 ∈ 𝐾 )
49 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → 𝑌 ∈ 𝐾 )
50 49 mptexd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ∈ V )
51 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) )
52 51 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ∈ V ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ‘ 𝑥 ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) )
53 46 50 52 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ‘ 𝑥 ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) )
54 45 53 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑔 ‘ 𝑥 ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) )
55 54 fveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) = ( ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ‘ 𝑦 ) )
56 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → 𝑦 ∈ 𝑌 )
57 ovex ⊢ ( 𝑥 𝑓 𝑦 ) ∈ V
58 eqid ⊢ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) )
59 58 fvmpt2 ⊢ ( ( 𝑦 ∈ 𝑌 ∧ ( 𝑥 𝑓 𝑦 ) ∈ V ) → ( ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ‘ 𝑦 ) = ( 𝑥 𝑓 𝑦 ) )
60 56 57 59 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → ( ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ‘ 𝑦 ) = ( 𝑥 𝑓 𝑦 ) )
61 55 60 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) = ( 𝑥 𝑓 𝑦 ) )
62 61 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑌 → ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) = ( 𝑥 𝑓 𝑦 ) ) )
63 43 62 ralrimi ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑌 ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) = ( 𝑥 𝑓 𝑦 ) )
64 eqid ⊢ 𝑌 = 𝑌
65 63 64 jctil ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑌 = 𝑌 ∧ ∀ 𝑦 ∈ 𝑌 ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) = ( 𝑥 𝑓 𝑦 ) ) )
66 65 ex ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) → ( 𝑥 ∈ 𝑋 → ( 𝑌 = 𝑌 ∧ ∀ 𝑦 ∈ 𝑌 ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) = ( 𝑥 𝑓 𝑦 ) ) ) )
67 33 66 ralrimi ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑌 = 𝑌 ∧ ∀ 𝑦 ∈ 𝑌 ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) = ( 𝑥 𝑓 𝑦 ) ) )
68 mpoeq123 ⊢ ( ( 𝑋 = 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑌 = 𝑌 ∧ ∀ 𝑦 ∈ 𝑌 ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) = ( 𝑥 𝑓 𝑦 ) ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) )
69 27 67 68 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) )
70 26 69 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) → 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) )
71 25 70 jca ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ) → ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ∧ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) )
72 simprr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ∧ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) ) → 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) )
73 1 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
74 2 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
75 14 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) → 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
76 5 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) → 𝐾 ∈ 𝑛-Locally Comp )
77 nllytop ⊢ ( 𝐾 ∈ 𝑛-Locally Comp → 𝐾 ∈ Top )
78 76 77 syl ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) → 𝐾 ∈ Top )
79 6 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) → 𝐿 ∈ Top )
80 eqid ⊢ ( 𝐿 ↑ko 𝐾 ) = ( 𝐿 ↑ko 𝐾 )
81 80 xkotopon ⊢ ( ( 𝐾 ∈ Top ∧ 𝐿 ∈ Top ) → ( 𝐿 ↑ko 𝐾 ) ∈ ( TopOn ‘ ( 𝐾 Cn 𝐿 ) ) )
82 78 79 81 syl2anc ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) → ( 𝐿 ↑ko 𝐾 ) ∈ ( TopOn ‘ ( 𝐾 Cn 𝐿 ) ) )
83 simpr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) → 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) )
84 cnf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐿 ↑ko 𝐾 ) ∈ ( TopOn ‘ ( 𝐾 Cn 𝐿 ) ) ∧ 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) → 𝑔 : 𝑋 ⟶ ( 𝐾 Cn 𝐿 ) )
85 73 82 83 84 syl3anc ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) → 𝑔 : 𝑋 ⟶ ( 𝐾 Cn 𝐿 ) )
86 85 feqmptd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) → 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑥 ) ) )
87 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
88 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
89 85 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑔 ‘ 𝑥 ) ∈ ( 𝐾 Cn 𝐿 ) )
90 cnf2 ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) ∧ ( 𝑔 ‘ 𝑥 ) ∈ ( 𝐾 Cn 𝐿 ) ) → ( 𝑔 ‘ 𝑥 ) : 𝑌 ⟶ ∪ 𝐿 )
91 87 88 89 90 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑔 ‘ 𝑥 ) : 𝑌 ⟶ ∪ 𝐿 )
92 91 feqmptd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑔 ‘ 𝑥 ) = ( 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) )
93 92 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) )
94 86 93 eqtrd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) → 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) )
95 94 83 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) )
96 73 74 75 76 95 cnmptk2 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )
97 96 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ∧ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )
98 72 97 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ∧ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) ) → 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )
99 94 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ∧ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) ) → 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) )
100 nfv ⊢ Ⅎ 𝑥 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) )
101 nfmpo1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) )
102 101 nfeq2 ⊢ Ⅎ 𝑥 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) )
103 100 102 nfan ⊢ Ⅎ 𝑥 ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ∧ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) )
104 28 103 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ∧ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) )
105 nfv ⊢ Ⅎ 𝑦 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) )
106 nfmpo2 ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) )
107 106 nfeq2 ⊢ Ⅎ 𝑦 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) )
108 105 107 nfan ⊢ Ⅎ 𝑦 ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ∧ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) )
109 34 108 nfan ⊢ Ⅎ 𝑦 ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ∧ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) )
110 109 42 nfan ⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ∧ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) ) ∧ 𝑥 ∈ 𝑋 )
111 72 oveqd ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ∧ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) ) → ( 𝑥 𝑓 𝑦 ) = ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) 𝑦 ) )
112 fvex ⊢ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ∈ V
113 eqid ⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) )
114 113 ovmpt4g ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ∈ V ) → ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) 𝑦 ) = ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) )
115 112 114 mp3an3 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) 𝑦 ) = ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) )
116 111 115 sylan9eq ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ∧ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 𝑓 𝑦 ) = ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) )
117 116 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ∧ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑌 → ( 𝑥 𝑓 𝑦 ) = ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) )
118 110 117 ralrimi ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ∧ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝑓 𝑦 ) = ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) )
119 mpteq12 ⊢ ( ( 𝑌 = 𝑌 ∧ ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝑓 𝑦 ) = ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) → ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) = ( 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) )
120 64 118 119 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ∧ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) = ( 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) )
121 104 120 mpteq2da ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ∧ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) )
122 99 121 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ∧ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) ) → 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) )
123 98 122 jca ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ∧ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) ) → ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) )
124 71 123 impbida ⊢ ( 𝜑 → ( ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ↔ ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ∧ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) ) )
125 124 opabbidv ⊢ ( 𝜑 → { ⟨ 𝑔 , 𝑓 ⟩ ∣ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) } = { ⟨ 𝑔 , 𝑓 ⟩ ∣ ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ∧ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) } )
126 df-mpt ⊢ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) }
127 3 126 eqtri ⊢ 𝐹 = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) }
128 127 cnveqi ⊢ ◡ 𝐹 = ◡ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) }
129 cnvopab ⊢ ◡ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) } = { ⟨ 𝑔 , 𝑓 ⟩ ∣ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) }
130 128 129 eqtri ⊢ ◡ 𝐹 = { ⟨ 𝑔 , 𝑓 ⟩ ∣ ( 𝑓 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ 𝑔 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) }
131 df-mpt ⊢ ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ↦ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) = { ⟨ 𝑔 , 𝑓 ⟩ ∣ ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ∧ 𝑓 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) }
132 125 130 131 3eqtr4g ⊢ ( 𝜑 → ◡ 𝐹 = ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ↦ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) )