Theorem xkocnv 23701

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 772	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
2		xkohmeo.x	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
3	2	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐽 ∈ (TopOn‘𝑋))
4		xkohmeo.y	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))
5	4	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐾 ∈ (TopOn‘𝑌))
6		txtopon 23478	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
7	2, 4, 6	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
8	7	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
9		xkohmeo.l	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ Top)
10		toptopon2 22805	. . . . . . . . . . . . . 14 ⊢ (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘∪ 𝐿))
11	9, 10	sylib 218	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ (TopOn‘∪ 𝐿))
12	11	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐿 ∈ (TopOn‘∪ 𝐿))
13		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
14		cnf2 23136	. . . . . . . . . . . 12 ⊢ (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿) ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓:(𝑋 × 𝑌)⟶∪ 𝐿)
15	8, 12, 13, 14	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓:(𝑋 × 𝑌)⟶∪ 𝐿)
16	15	ffnd 6689	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 Fn (𝑋 × 𝑌))
17		fnov 7520	. . . . . . . . . 10 ⊢ (𝑓 Fn (𝑋 × 𝑌) ↔ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
18	16, 17	sylib 218	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
19	18, 13	eqeltrrd 2829	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
20	3, 5, 19	cnmpt2k 23575	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
21	20	adantrr 717	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
22	1, 21	eqeltrd 2828	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
23	18	adantrr 717	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
24		eqid 2729	. . . . . . 7 ⊢ 𝑋 = 𝑋
25		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑥𝜑
26		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)
27		nfmpt1 5206	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
28	27	nfeq2 2909	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
29	26, 28	nfan 1899	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
30	25, 29	nfan 1899	. . . . . . . 8 ⊢ Ⅎ𝑥(𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))))
31		nfv 1914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦𝜑
32		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)
33		nfcv 2891	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦𝑋
34		nfmpt1 5206	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦(𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))
35	33, 34	nfmpt 5205	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦(𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
36	35	nfeq2 2909	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
37	32, 36	nfan 1899	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
38	31, 37	nfan 1899	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))))
39		nfv 1914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑥 ∈ 𝑋
40	38, 39	nfan 1899	. . . . . . . . . . 11 ⊢ Ⅎ𝑦((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋)
41		simplrr 777	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
42	41	fveq1d 6860	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑔‘𝑥) = ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥))
43		simprl 770	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑥 ∈ 𝑋)
44		toponmax 22813	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 ∈ 𝐾)
45	4, 44	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑌 ∈ 𝐾)
46	45	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑌 ∈ 𝐾)
47	46	mptexd 7198	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) ∈ V)
48		eqid 2729	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
49	48	fvmpt2 6979	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) ∈ V) → ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
50	43, 47, 49	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
51	42, 50	eqtrd 2764	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑔‘𝑥) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
52	51	fveq1d 6860	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑔‘𝑥)‘𝑦) = ((𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))‘𝑦))
53		simprr 772	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ∈ 𝑌)
54		ovex 7420	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑓𝑦) ∈ V
55		eqid 2729	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))
56	55	fvmpt2 6979	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝑌 ∧ (𝑥𝑓𝑦) ∈ V) → ((𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))‘𝑦) = (𝑥𝑓𝑦))
57	53, 54, 56	sylancl 586	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))‘𝑦) = (𝑥𝑓𝑦))
58	52, 57	eqtrd 2764	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))
59	58	expr 456	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 → ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦)))
60	40, 59	ralrimi 3235	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))
61		eqid 2729	. . . . . . . . . 10 ⊢ 𝑌 = 𝑌
62	60, 61	jctil 519	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋) → (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦)))
63	62	ex 412	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥 ∈ 𝑋 → (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))))
64	30, 63	ralrimi 3235	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → ∀𝑥 ∈ 𝑋 (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦)))
65		mpoeq123 7461	. . . . . . 7 ⊢ ((𝑋 = 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
66	24, 64, 65	sylancr 587	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
67	23, 66	eqtr4d 2767	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
68	22, 67	jca 511	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
69		simprr 772	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
70	2	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐽 ∈ (TopOn‘𝑋))
71	4	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐾 ∈ (TopOn‘𝑌))
72	11	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐿 ∈ (TopOn‘∪ 𝐿))
73		xkohmeo.k	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Comp)
74	73	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐾 ∈ 𝑛-Locally Comp)
75		nllytop 23360	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ 𝑛-Locally Comp → 𝐾 ∈ Top)
76	74, 75	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐾 ∈ Top)
77	9	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐿 ∈ Top)
78		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (𝐿 ↑ko 𝐾) = (𝐿 ↑ko 𝐾)
79	78	xkotopon 23487	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)))
80	76, 77, 79	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)))
81		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
82		cnf2 23136	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)) ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔:𝑋⟶(𝐾 Cn 𝐿))
83	70, 80, 81, 82	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔:𝑋⟶(𝐾 Cn 𝐿))
84	83	feqmptd 6929	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑔‘𝑥)))
85	4	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → 𝐾 ∈ (TopOn‘𝑌))
86	11	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → 𝐿 ∈ (TopOn‘∪ 𝐿))
87	83	ffvelcdmda 7056	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → (𝑔‘𝑥) ∈ (𝐾 Cn 𝐿))
88		cnf2 23136	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿) ∧ (𝑔‘𝑥) ∈ (𝐾 Cn 𝐿)) → (𝑔‘𝑥):𝑌⟶∪ 𝐿)
89	85, 86, 87, 88	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → (𝑔‘𝑥):𝑌⟶∪ 𝐿)
90	89	feqmptd 6929	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → (𝑔‘𝑥) = (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
91	90	mpteq2dva 5200	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝑥 ∈ 𝑋 ↦ (𝑔‘𝑥)) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
92	84, 91	eqtrd 2764	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
93	92, 81	eqeltrrd 2829	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
94	70, 71, 72, 74, 93	cnmptk2 23573	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
95	94	adantrr 717	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
96	69, 95	eqeltrd 2828	. . . . 5 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
97	92	adantrr 717	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
98		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))
99		nfmpo1 7469	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))
100	99	nfeq2 2909	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))
101	98, 100	nfan 1899	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
102	25, 101	nfan 1899	. . . . . . 7 ⊢ Ⅎ𝑥(𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
103		nfv 1914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))
104		nfmpo2 7470	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))
105	104	nfeq2 2909	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))
106	103, 105	nfan 1899	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
107	31, 106	nfan 1899	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
108	107, 39	nfan 1899	. . . . . . . . 9 ⊢ Ⅎ𝑦((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋)
109	69	oveqd 7404	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑥𝑓𝑦) = (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))𝑦))
110		fvex 6871	. . . . . . . . . . . 12 ⊢ ((𝑔‘𝑥)‘𝑦) ∈ V
111		eqid 2729	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))
112	111	ovmpt4g 7536	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ ((𝑔‘𝑥)‘𝑦) ∈ V) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))𝑦) = ((𝑔‘𝑥)‘𝑦))
113	110, 112	mp3an3 1452	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))𝑦) = ((𝑔‘𝑥)‘𝑦))
114	109, 113	sylan9eq 2784	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦))
115	114	expr 456	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 → (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦)))
116	108, 115	ralrimi 3235	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦))
117		mpteq12 5195	. . . . . . . 8 ⊢ ((𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
118	61, 116, 117	sylancr 587	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
119	102, 118	mpteq2da 5199	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
120	97, 119	eqtr4d 2767	. . . . 5 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
121	96, 120	jca 511	. . . 4 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))))
122	68, 121	impbida 800	. . 3 ⊢ (𝜑 → ((𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) ↔ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))))
123	122	opabbidv 5173	. 2 ⊢ (𝜑 → {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))} = {⟨𝑔, 𝑓⟩ ∣ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))})
124		xkohmeo.f	. . . . 5 ⊢ 𝐹 = (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
125		df-mpt 5189	. . . . 5 ⊢ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))}
126	124, 125	eqtri 2752	. . . 4 ⊢ 𝐹 = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))}
127	126	cnveqi 5838	. . 3 ⊢ ◡𝐹 = ◡{⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))}
128		cnvopab 6110	. . 3 ⊢ ◡{⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))} = {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))}
129	127, 128	eqtri 2752	. 2 ⊢ ◡𝐹 = {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))}
130		df-mpt 5189	. 2 ⊢ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) = {⟨𝑔, 𝑓⟩ ∣ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))}
131	123, 129, 130	3eqtr4g 2789	1 ⊢ (𝜑 → ◡𝐹 = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  Vcvv 3447  ∪ cuni 4871  {copab 5169   ↦ cmpt 5188   × cxp 5636  ^◡ccnv 5637   Fn wfn 6506  ⟶wf 6507  ‘cfv 6511  (class class class)co 7387   ∈ cmpo 7389  Topctop 22780  TopOnctopon 22797   Cn ccn 23111  Compccmp 23273  𝑛-Locally cnlly 23352   ×_t ctx 23447   ↑_ko cxko 23448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-int 4911  df-iun 4957  df-iin 4958  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-1st 7968  df-2nd 7969  df-1o 8434  df-2o 8435  df-map 8801  df-ixp 8871  df-en 8919  df-dom 8920  df-fin 8922  df-fi 9362  df-rest 17385  df-topgen 17406  df-pt 17407  df-top 22781  df-topon 22798  df-bases 22833  df-ntr 22907  df-nei 22985  df-cn 23114  df-cnp 23115  df-cmp 23274  df-nlly 23354  df-tx 23449  df-xko 23450

This theorem is referenced by:  xkohmeo  23702