Theorem xkocnv 23980

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

Hypotheses

Ref	Expression
xkohmeo.x	⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
xkohmeo.y	⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))
xkohmeo.f	⊢ 𝐹 = (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
xkohmeo.j	⊢ (𝜑 → 𝐽 ∈ 𝑛-Locally Comp)
xkohmeo.k	⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Comp)
xkohmeo.l	⊢ (𝜑 → 𝐿 ∈ Top)

Assertion

Ref	Expression
xkocnv	⊢ (𝜑 → ◡𝐹 = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))

Distinct variable groups:   𝑓,𝑔,𝑥,𝑦,𝐽   𝑓,𝐾,𝑔,𝑥,𝑦   𝜑,𝑓,𝑔,𝑥,𝑦   𝑓,𝐿,𝑔,𝑥,𝑦   𝑓,𝑋,𝑔,𝑥,𝑦   𝑓,𝑌,𝑔,𝑥,𝑦   𝑓,𝐹,𝑔,𝑥,𝑦

Proof of Theorem xkocnv

Step	Hyp	Ref	Expression
1		simprr 784	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
2		xkohmeo.x	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
3	2	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐽 ∈ (TopOn‘𝑋))
4		xkohmeo.y	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))
5	4	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐾 ∈ (TopOn‘𝑌))
6		txtopon 23757	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
7	2, 4, 6	syl2anc 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
8	7	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
9		xkohmeo.l	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ Top)
10		toptopon2 23084	. . . . . . . . . . . . . 14 ⊢ (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘∪ 𝐿))
11	9, 10	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ (TopOn‘∪ 𝐿))
12	11	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐿 ∈ (TopOn‘∪ 𝐿))
13		simpr 489	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
14		cnf2 23415	. . . . . . . . . . . 12 ⊢ (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿) ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓:(𝑋 × 𝑌)⟶∪ 𝐿)
15	8, 12, 13, 14	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓:(𝑋 × 𝑌)⟶∪ 𝐿)
16	15	ffnd 6706	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 Fn (𝑋 × 𝑌))
17		fnov 7541	. . . . . . . . . 10 ⊢ (𝑓 Fn (𝑋 × 𝑌) ↔ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
18	16, 17	sylib 221	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
19	18, 13	eqeltrrd 2864	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
20	3, 5, 19	cnmpt2k 23854	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
21	20	adantrr 729	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
22	1, 21	eqeltrd 2863	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
23	18	adantrr 729	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
24		eqid 2763	. . . . . . 7 ⊢ 𝑋 = 𝑋
25		nfv 1944	. . . . . . . . 9 ⊢ Ⅎ𝑥𝜑
26		nfv 1944	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)
27		nfmpt1 5210	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
28	27	nfeq2 2942	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
29	26, 28	nfan 1929	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
30	25, 29	nfan 1929	. . . . . . . 8 ⊢ Ⅎ𝑥(𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))))
31		nfv 1944	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦𝜑
32		nfv 1944	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)
33		nfcv 2925	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦𝑋
34		nfmpt1 5210	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦(𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))
35	33, 34	nfmpt 5209	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦(𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
36	35	nfeq2 2942	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
37	32, 36	nfan 1929	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
38	31, 37	nfan 1929	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))))
39		nfv 1944	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑥 ∈ 𝑋
40	38, 39	nfan 1929	. . . . . . . . . . 11 ⊢ Ⅎ𝑦((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋)
41		simplrr 789	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
42	41	fveq1d 6883	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑔‘𝑥) = ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥))
43		simprl 782	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑥 ∈ 𝑋)
44		toponmax 23092	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 ∈ 𝐾)
45	4, 44	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑌 ∈ 𝐾)
46	45	ad2antrr 738	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑌 ∈ 𝐾)
47	46	mptexd 7222	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) ∈ V)
48		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
49	48	fvmpt2 7001	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) ∈ V) → ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
50	43, 47, 49	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
51	42, 50	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑔‘𝑥) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
52	51	fveq1d 6883	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑔‘𝑥)‘𝑦) = ((𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))‘𝑦))
53		simprr 784	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ∈ 𝑌)
54		ovex 7443	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑓𝑦) ∈ V
55		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))
56	55	fvmpt2 7001	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝑌 ∧ (𝑥𝑓𝑦) ∈ V) → ((𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))‘𝑦) = (𝑥𝑓𝑦))
57	53, 54, 56	sylancl 597	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))‘𝑦) = (𝑥𝑓𝑦))
58	52, 57	eqtrd 2798	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))
59	58	expr 461	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 → ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦)))
60	40, 59	ralrimi 3263	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))
61		eqid 2763	. . . . . . . . . 10 ⊢ 𝑌 = 𝑌
62	60, 61	jctil 528	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋) → (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦)))
63	62	ex 417	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥 ∈ 𝑋 → (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))))
64	30, 63	ralrimi 3263	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → ∀𝑥 ∈ 𝑋 (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦)))
65		mpoeq123 7482	. . . . . . 7 ⊢ ((𝑋 = 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
66	24, 64, 65	sylancr 598	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
67	23, 66	eqtr4d 2801	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
68	22, 67	jca 520	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
69		simprr 784	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
70	2	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐽 ∈ (TopOn‘𝑋))
71	4	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐾 ∈ (TopOn‘𝑌))
72	11	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐿 ∈ (TopOn‘∪ 𝐿))
73		xkohmeo.k	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Comp)
74	73	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐾 ∈ 𝑛-Locally Comp)
75		nllytop 23639	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ 𝑛-Locally Comp → 𝐾 ∈ Top)
76	74, 75	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐾 ∈ Top)
77	9	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐿 ∈ Top)
78		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (𝐿 ↑ko 𝐾) = (𝐿 ↑ko 𝐾)
79	78	xkotopon 23766	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)))
80	76, 77, 79	syl2anc 595	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)))
81		simpr 489	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
82		cnf2 23415	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)) ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔:𝑋⟶(𝐾 Cn 𝐿))
83	70, 80, 81, 82	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔:𝑋⟶(𝐾 Cn 𝐿))
84	83	feqmptd 6949	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑔‘𝑥)))
85	4	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → 𝐾 ∈ (TopOn‘𝑌))
86	11	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → 𝐿 ∈ (TopOn‘∪ 𝐿))
87	83	ffvelcdmda 7079	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → (𝑔‘𝑥) ∈ (𝐾 Cn 𝐿))
88		cnf2 23415	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿) ∧ (𝑔‘𝑥) ∈ (𝐾 Cn 𝐿)) → (𝑔‘𝑥):𝑌⟶∪ 𝐿)
89	85, 86, 87, 88	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → (𝑔‘𝑥):𝑌⟶∪ 𝐿)
90	89	feqmptd 6949	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → (𝑔‘𝑥) = (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
91	90	mpteq2dva 5204	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝑥 ∈ 𝑋 ↦ (𝑔‘𝑥)) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
92	84, 91	eqtrd 2798	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
93	92, 81	eqeltrrd 2864	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
94	70, 71, 72, 74, 93	cnmptk2 23852	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
95	94	adantrr 729	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
96	69, 95	eqeltrd 2863	. . . . 5 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
97	92	adantrr 729	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
98		nfv 1944	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))
99		nfmpo1 7490	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))
100	99	nfeq2 2942	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))
101	98, 100	nfan 1929	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
102	25, 101	nfan 1929	. . . . . . 7 ⊢ Ⅎ𝑥(𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
103		nfv 1944	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))
104		nfmpo2 7491	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))
105	104	nfeq2 2942	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))
106	103, 105	nfan 1929	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
107	31, 106	nfan 1929	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
108	107, 39	nfan 1929	. . . . . . . . 9 ⊢ Ⅎ𝑦((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋)
109	69	oveqd 7427	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑥𝑓𝑦) = (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))𝑦))
110		fvex 6894	. . . . . . . . . . . 12 ⊢ ((𝑔‘𝑥)‘𝑦) ∈ V
111		eqid 2763	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))
112	111	ovmpt4g 7557	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ ((𝑔‘𝑥)‘𝑦) ∈ V) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))𝑦) = ((𝑔‘𝑥)‘𝑦))
113	110, 112	mp3an3 1479	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))𝑦) = ((𝑔‘𝑥)‘𝑦))
114	109, 113	sylan9eq 2818	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦))
115	114	expr 461	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 → (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦)))
116	108, 115	ralrimi 3263	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦))
117		mpteq12 5199	. . . . . . . 8 ⊢ ((𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
118	61, 116, 117	sylancr 598	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
119	102, 118	mpteq2da 5203	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
120	97, 119	eqtr4d 2801	. . . . 5 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
121	96, 120	jca 520	. . . 4 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))))
122	68, 121	impbida 812	. . 3 ⊢ (𝜑 → ((𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) ↔ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))))
123	122	opabbidv 5177	. 2 ⊢ (𝜑 → {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))} = {⟨𝑔, 𝑓⟩ ∣ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))})
124		xkohmeo.f	. . . . 5 ⊢ 𝐹 = (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
125		df-mpt 5193	. . . . 5 ⊢ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))}
126	124, 125	eqtri 2786	. . . 4 ⊢ 𝐹 = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))}
127	126	cnveqi 5860	. . 3 ⊢ ◡𝐹 = ◡{⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))}
128		cnvopab 6137	. . 3 ⊢ ◡{⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))} = {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))}
129	127, 128	eqtri 2786	. 2 ⊢ ◡𝐹 = {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))}
130		df-mpt 5193	. 2 ⊢ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) = {⟨𝑔, 𝑓⟩ ∣ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))}
131	123, 129, 130	3eqtr4g 2823	1 ⊢ (𝜑 → ◡𝐹 = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∀wral 3079  Vcvv 3455  ∪ cuni 4872  {copab 5173   ↦ cmpt 5192   × cxp 5659  ^◡ccnv 5660   Fn wfn 6531  ⟶wf 6532  ‘cfv 6536  (class class class)co 7410   ∈ cmpo 7412  Topctop 23059  TopOnctopon 23076   Cn ccn 23390  Compccmp 23552  𝑛-Locally cnlly 23631   ×_t ctx 23726   ↑_ko cxko 23727

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-int 4913  df-iun 4958  df-iin 4959  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-1st 7982  df-2nd 7983  df-1o 8449  df-2o 8450  df-map 8822  df-ixp 8892  df-en 8940  df-dom 8941  df-fin 8943  df-fi 9367  df-rest 17479  df-topgen 17500  df-pt 17501  df-top 23060  df-topon 23077  df-bases 23112  df-ntr 23186  df-nei 23264  df-cn 23393  df-cnp 23394  df-cmp 23553  df-nlly 23633  df-tx 23728  df-xko 23729

This theorem is used by:  xkohmeo  23981