Theorem xkocnv 24133

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 785	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
2		xkohmeo.x	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
3	2	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐽 ∈ (TopOn‘𝑋))
4		xkohmeo.y	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))
5	4	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐾 ∈ (TopOn‘𝑌))
6		txtopon 23910	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
7	2, 4, 6	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
8	7	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
9		xkohmeo.l	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ Top)
10		toptopon2 23236	. . . . . . . . . . . . . 14 ⊢ (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘∪ 𝐿))
11	9, 10	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ (TopOn‘∪ 𝐿))
12	11	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐿 ∈ (TopOn‘∪ 𝐿))
13		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
14		cnf2 23567	. . . . . . . . . . . 12 ⊢ (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿) ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓:(𝑋 × 𝑌)⟶∪ 𝐿)
15	8, 12, 13, 14	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓:(𝑋 × 𝑌)⟶∪ 𝐿)
16	15	ffnd 6710	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 Fn (𝑋 × 𝑌))
17		fnov 7551	. . . . . . . . . 10 ⊢ (𝑓 Fn (𝑋 × 𝑌) ↔ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
18	16, 17	sylib 221	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
19	18, 13	eqeltrrd 2861	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
20	3, 5, 19	cnmpt2k 24007	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
21	20	adantrr 730	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
22	1, 21	eqeltrd 2860	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
23	18	adantrr 730	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
24		eqid 2760	. . . . . . 7 ⊢ 𝑋 = 𝑋
25		nfv 1946	. . . . . . . . 9 ⊢ Ⅎ𝑥𝜑
26		nfv 1946	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)
27		nfmpt1 5203	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
28	27	nfeq2 2939	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
29	26, 28	nfan 1931	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
30	25, 29	nfan 1931	. . . . . . . 8 ⊢ Ⅎ𝑥(𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))))
31		nfv 1946	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦𝜑
32		nfv 1946	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)
33		nfcv 2922	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦𝑋
34		nfmpt1 5203	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦(𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))
35	33, 34	nfmpt 5202	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦(𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
36	35	nfeq2 2939	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
37	32, 36	nfan 1931	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
38	31, 37	nfan 1931	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))))
39		nfv 1946	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑥 ∈ 𝑋
40	38, 39	nfan 1931	. . . . . . . . . . 11 ⊢ Ⅎ𝑦((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋)
41		simplrr 790	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
42	41	fveq1d 6887	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑔‘𝑥) = ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥))
43		simprl 783	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑥 ∈ 𝑋)
44		toponmax 23244	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 ∈ 𝐾)
45	4, 44	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑌 ∈ 𝐾)
46	45	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑌 ∈ 𝐾)
47	46	mptexd 7230	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) ∈ V)
48		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
49	48	fvmpt2 7005	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) ∈ V) → ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
50	43, 47, 49	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
51	42, 50	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑔‘𝑥) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
52	51	fveq1d 6887	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑔‘𝑥)‘𝑦) = ((𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))‘𝑦))
53		simprr 785	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ∈ 𝑌)
54		ovex 7453	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑓𝑦) ∈ V
55		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))
56	55	fvmpt2 7005	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝑌 ∧ (𝑥𝑓𝑦) ∈ V) → ((𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))‘𝑦) = (𝑥𝑓𝑦))
57	53, 54, 56	sylancl 598	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))‘𝑦) = (𝑥𝑓𝑦))
58	52, 57	eqtrd 2795	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))
59	58	expr 462	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 → ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦)))
60	40, 59	ralrimi 3260	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))
61		eqid 2760	. . . . . . . . . 10 ⊢ 𝑌 = 𝑌
62	60, 61	jctil 529	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋) → (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦)))
63	62	ex 418	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥 ∈ 𝑋 → (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))))
64	30, 63	ralrimi 3260	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → ∀𝑥 ∈ 𝑋 (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦)))
65		mpoeq123 7492	. . . . . . 7 ⊢ ((𝑋 = 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
66	24, 64, 65	sylancr 599	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
67	23, 66	eqtr4d 2798	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
68	22, 67	jca 521	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
69		simprr 785	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
70	2	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐽 ∈ (TopOn‘𝑋))
71	4	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐾 ∈ (TopOn‘𝑌))
72	11	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐿 ∈ (TopOn‘∪ 𝐿))
73		xkohmeo.k	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Comp)
74	73	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐾 ∈ 𝑛-Locally Comp)
75		nllytop 23792	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ 𝑛-Locally Comp → 𝐾 ∈ Top)
76	74, 75	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐾 ∈ Top)
77	9	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐿 ∈ Top)
78		eqid 2760	. . . . . . . . . . . . . 14 ⊢ (𝐿 ↑ko 𝐾) = (𝐿 ↑ko 𝐾)
79	78	xkotopon 23919	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)))
80	76, 77, 79	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)))
81		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
82		cnf2 23567	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)) ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔:𝑋⟶(𝐾 Cn 𝐿))
83	70, 80, 81, 82	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔:𝑋⟶(𝐾 Cn 𝐿))
84	83	feqmptd 6953	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑔‘𝑥)))
85	4	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → 𝐾 ∈ (TopOn‘𝑌))
86	11	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → 𝐿 ∈ (TopOn‘∪ 𝐿))
87	83	ffvelcdmda 7084	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → (𝑔‘𝑥) ∈ (𝐾 Cn 𝐿))
88		cnf2 23567	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿) ∧ (𝑔‘𝑥) ∈ (𝐾 Cn 𝐿)) → (𝑔‘𝑥):𝑌⟶∪ 𝐿)
89	85, 86, 87, 88	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → (𝑔‘𝑥):𝑌⟶∪ 𝐿)
90	89	feqmptd 6953	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → (𝑔‘𝑥) = (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
91	90	mpteq2dva 5197	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝑥 ∈ 𝑋 ↦ (𝑔‘𝑥)) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
92	84, 91	eqtrd 2795	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
93	92, 81	eqeltrrd 2861	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
94	70, 71, 72, 74, 93	cnmptk2 24005	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
95	94	adantrr 730	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
96	69, 95	eqeltrd 2860	. . . . 5 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
97	92	adantrr 730	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
98		nfv 1946	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))
99		nfmpo1 7500	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))
100	99	nfeq2 2939	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))
101	98, 100	nfan 1931	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
102	25, 101	nfan 1931	. . . . . . 7 ⊢ Ⅎ𝑥(𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
103		nfv 1946	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))
104		nfmpo2 7501	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))
105	104	nfeq2 2939	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))
106	103, 105	nfan 1931	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
107	31, 106	nfan 1931	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
108	107, 39	nfan 1931	. . . . . . . . 9 ⊢ Ⅎ𝑦((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋)
109	69	oveqd 7437	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑥𝑓𝑦) = (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))𝑦))
110		fvex 6898	. . . . . . . . . . . 12 ⊢ ((𝑔‘𝑥)‘𝑦) ∈ V
111		eqid 2760	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))
112	111	ovmpt4g 7567	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ ((𝑔‘𝑥)‘𝑦) ∈ V) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))𝑦) = ((𝑔‘𝑥)‘𝑦))
113	110, 112	mp3an3 1479	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))𝑦) = ((𝑔‘𝑥)‘𝑦))
114	109, 113	sylan9eq 2815	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦))
115	114	expr 462	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 → (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦)))
116	108, 115	ralrimi 3260	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦))
117		mpteq12 5192	. . . . . . . 8 ⊢ ((𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
118	61, 116, 117	sylancr 599	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
119	102, 118	mpteq2da 5196	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
120	97, 119	eqtr4d 2798	. . . . 5 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
121	96, 120	jca 521	. . . 4 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))))
122	68, 121	impbida 813	. . 3 ⊢ (𝜑 → ((𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) ↔ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))))
123	122	opabbidv 5170	. 2 ⊢ (𝜑 → {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))} = {⟨𝑔, 𝑓⟩ ∣ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))})
124		xkohmeo.f	. . . . 5 ⊢ 𝐹 = (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
125		df-mpt 5186	. . . . 5 ⊢ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))}
126	124, 125	eqtri 2783	. . . 4 ⊢ 𝐹 = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))}
127	126	cnveqi 5851	. . 3 ⊢ ◡𝐹 = ◡{⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))}
128		cnvopab 6130	. . 3 ⊢ ◡{⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))} = {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))}
129	127, 128	eqtri 2783	. 2 ⊢ ◡𝐹 = {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))}
130		df-mpt 5186	. 2 ⊢ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) = {⟨𝑔, 𝑓⟩ ∣ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))}
131	123, 129, 130	3eqtr4g 2820	1 ⊢ (𝜑 → ◡𝐹 = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∀wral 3076  Vcvv 3450  ∪ cuni 4866  {copab 5166   ↦ cmpt 5185   × cxp 5648  ^◡ccnv 5649   Fn wfn 6533  ⟶wf 6534  ‘cfv 6538  (class class class)co 7420   ∈ cmpo 7422  Topctop 23211  TopOnctopon 23228   Cn ccn 23542  Compccmp 23704  𝑛-Locally cnlly 23784   ×_t ctx 23879   ↑_ko cxko 23880

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-int 4907  df-iun 4952  df-iin 4953  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-1o 8476  df-2o 8477  df-map 8849  df-ixp 8926  df-en 8974  df-dom 8975  df-fin 8977  df-fi 9403  df-rest 17593  df-topgen 17614  df-pt 17615  df-top 23212  df-topon 23229  df-bases 23264  df-ntr 23338  df-nei 23416  df-cn 23545  df-cnp 23546  df-cmp 23705  df-nlly 23786  df-tx 23881  df-xko 23882

This theorem is used by:  xkohmeo  24134