Theorem xkocnv 23775

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 773	. . . . . 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 23552	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
7	2, 4, 6	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
8	7	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
9		xkohmeo.l	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ Top)
10		toptopon2 22879	. . . . . . . . . . . . . 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 23210	. . . . . . . . . . . 12 ⊢ (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿) ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓:(𝑋 × 𝑌)⟶∪ 𝐿)
15	8, 12, 13, 14	syl3anc 1374	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓:(𝑋 × 𝑌)⟶∪ 𝐿)
16	15	ffnd 6673	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 Fn (𝑋 × 𝑌))
17		fnov 7501	. . . . . . . . . 10 ⊢ (𝑓 Fn (𝑋 × 𝑌) ↔ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
18	16, 17	sylib 218	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
19	18, 13	eqeltrrd 2838	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
20	3, 5, 19	cnmpt2k 23649	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
21	20	adantrr 718	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
22	1, 21	eqeltrd 2837	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
23	18	adantrr 718	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
24		eqid 2737	. . . . . . 7 ⊢ 𝑋 = 𝑋
25		nfv 1916	. . . . . . . . 9 ⊢ Ⅎ𝑥𝜑
26		nfv 1916	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)
27		nfmpt1 5199	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
28	27	nfeq2 2917	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
29	26, 28	nfan 1901	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
30	25, 29	nfan 1901	. . . . . . . 8 ⊢ Ⅎ𝑥(𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))))
31		nfv 1916	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦𝜑
32		nfv 1916	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)
33		nfcv 2899	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦𝑋
34		nfmpt1 5199	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦(𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))
35	33, 34	nfmpt 5198	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦(𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
36	35	nfeq2 2917	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
37	32, 36	nfan 1901	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
38	31, 37	nfan 1901	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))))
39		nfv 1916	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑥 ∈ 𝑋
40	38, 39	nfan 1901	. . . . . . . . . . 11 ⊢ Ⅎ𝑦((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋)
41		simplrr 778	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
42	41	fveq1d 6846	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑔‘𝑥) = ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥))
43		simprl 771	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑥 ∈ 𝑋)
44		toponmax 22887	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 ∈ 𝐾)
45	4, 44	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑌 ∈ 𝐾)
46	45	ad2antrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑌 ∈ 𝐾)
47	46	mptexd 7182	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) ∈ V)
48		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
49	48	fvmpt2 6963	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) ∈ V) → ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
50	43, 47, 49	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
51	42, 50	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑔‘𝑥) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
52	51	fveq1d 6846	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑔‘𝑥)‘𝑦) = ((𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))‘𝑦))
53		simprr 773	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ∈ 𝑌)
54		ovex 7403	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑓𝑦) ∈ V
55		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))
56	55	fvmpt2 6963	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝑌 ∧ (𝑥𝑓𝑦) ∈ V) → ((𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))‘𝑦) = (𝑥𝑓𝑦))
57	53, 54, 56	sylancl 587	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))‘𝑦) = (𝑥𝑓𝑦))
58	52, 57	eqtrd 2772	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))
59	58	expr 456	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 → ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦)))
60	40, 59	ralrimi 3236	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))
61		eqid 2737	. . . . . . . . . 10 ⊢ 𝑌 = 𝑌
62	60, 61	jctil 519	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥 ∈ 𝑋) → (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦)))
63	62	ex 412	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥 ∈ 𝑋 → (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))))
64	30, 63	ralrimi 3236	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → ∀𝑥 ∈ 𝑋 (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦)))
65		mpoeq123 7442	. . . . . . 7 ⊢ ((𝑋 = 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 ((𝑔‘𝑥)‘𝑦) = (𝑥𝑓𝑦))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
66	24, 64, 65	sylancr 588	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))
67	23, 66	eqtr4d 2775	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
68	22, 67	jca 511	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
69		simprr 773	. . . . . 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 23434	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ 𝑛-Locally Comp → 𝐾 ∈ Top)
76	74, 75	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐾 ∈ Top)
77	9	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝐿 ∈ Top)
78		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (𝐿 ↑ko 𝐾) = (𝐿 ↑ko 𝐾)
79	78	xkotopon 23561	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)))
80	76, 77, 79	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)))
81		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
82		cnf2 23210	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)) ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔:𝑋⟶(𝐾 Cn 𝐿))
83	70, 80, 81, 82	syl3anc 1374	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔:𝑋⟶(𝐾 Cn 𝐿))
84	83	feqmptd 6912	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑔‘𝑥)))
85	4	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → 𝐾 ∈ (TopOn‘𝑌))
86	11	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → 𝐿 ∈ (TopOn‘∪ 𝐿))
87	83	ffvelcdmda 7040	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → (𝑔‘𝑥) ∈ (𝐾 Cn 𝐿))
88		cnf2 23210	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿) ∧ (𝑔‘𝑥) ∈ (𝐾 Cn 𝐿)) → (𝑔‘𝑥):𝑌⟶∪ 𝐿)
89	85, 86, 87, 88	syl3anc 1374	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → (𝑔‘𝑥):𝑌⟶∪ 𝐿)
90	89	feqmptd 6912	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ∧ 𝑥 ∈ 𝑋) → (𝑔‘𝑥) = (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
91	90	mpteq2dva 5193	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝑥 ∈ 𝑋 ↦ (𝑔‘𝑥)) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
92	84, 91	eqtrd 2772	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
93	92, 81	eqeltrrd 2838	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)))
94	70, 71, 72, 74, 93	cnmptk2 23647	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
95	94	adantrr 718	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
96	69, 95	eqeltrd 2837	. . . . 5 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
97	92	adantrr 718	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
98		nfv 1916	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))
99		nfmpo1 7450	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))
100	99	nfeq2 2917	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))
101	98, 100	nfan 1901	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
102	25, 101	nfan 1901	. . . . . . 7 ⊢ Ⅎ𝑥(𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
103		nfv 1916	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))
104		nfmpo2 7451	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))
105	104	nfeq2 2917	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))
106	103, 105	nfan 1901	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
107	31, 106	nfan 1901	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
108	107, 39	nfan 1901	. . . . . . . . 9 ⊢ Ⅎ𝑦((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋)
109	69	oveqd 7387	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑥𝑓𝑦) = (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))𝑦))
110		fvex 6857	. . . . . . . . . . . 12 ⊢ ((𝑔‘𝑥)‘𝑦) ∈ V
111		eqid 2737	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))
112	111	ovmpt4g 7517	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ ((𝑔‘𝑥)‘𝑦) ∈ V) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))𝑦) = ((𝑔‘𝑥)‘𝑦))
113	110, 112	mp3an3 1453	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))𝑦) = ((𝑔‘𝑥)‘𝑦))
114	109, 113	sylan9eq 2792	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦))
115	114	expr 456	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 → (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦)))
116	108, 115	ralrimi 3236	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦))
117		mpteq12 5188	. . . . . . . 8 ⊢ ((𝑌 = 𝑌 ∧ ∀𝑦 ∈ 𝑌 (𝑥𝑓𝑦) = ((𝑔‘𝑥)‘𝑦)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
118	61, 116, 117	sylancr 588	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))
119	102, 118	mpteq2da 5192	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))
120	97, 119	eqtr4d 2775	. . . . 5 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
121	96, 120	jca 511	. . . 4 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) → (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))))
122	68, 121	impbida 801	. . 3 ⊢ (𝜑 → ((𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) ↔ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))))
123	122	opabbidv 5166	. 2 ⊢ (𝜑 → {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))} = {⟨𝑔, 𝑓⟩ ∣ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))})
124		xkohmeo.f	. . . . 5 ⊢ 𝐹 = (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))
125		df-mpt 5182	. . . . 5 ⊢ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))}
126	124, 125	eqtri 2760	. . . 4 ⊢ 𝐹 = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))}
127	126	cnveqi 5833	. . 3 ⊢ ◡𝐹 = ◡{⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))}
128		cnvopab 6104	. . 3 ⊢ ◡{⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))} = {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))}
129	127, 128	eqtri 2760	. 2 ⊢ ◡𝐹 = {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦))))}
130		df-mpt 5182	. 2 ⊢ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))) = {⟨𝑔, 𝑓⟩ ∣ (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ∧ 𝑓 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))}
131	123, 129, 130	3eqtr4g 2797	1 ⊢ (𝜑 → ◡𝐹 = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦))))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  Vcvv 3442  ∪ cuni 4865  {copab 5162   ↦ cmpt 5181   × cxp 5632  ^◡ccnv 5633   Fn wfn 6497  ⟶wf 6498  ‘cfv 6502  (class class class)co 7370   ∈ cmpo 7372  Topctop 22854  TopOnctopon 22871   Cn ccn 23185  Compccmp 23347  𝑛-Locally cnlly 23426   ×_t ctx 23521   ↑_ko cxko 23522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4905  df-iun 4950  df-iin 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5529  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5587  df-we 5589  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-ord 6330  df-on 6331  df-lim 6332  df-suc 6333  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-ov 7373  df-oprab 7374  df-mpo 7375  df-om 7821  df-1st 7945  df-2nd 7946  df-1o 8409  df-2o 8410  df-map 8779  df-ixp 8850  df-en 8898  df-dom 8899  df-fin 8901  df-fi 9328  df-rest 17356  df-topgen 17377  df-pt 17378  df-top 22855  df-topon 22872  df-bases 22907  df-ntr 22981  df-nei 23059  df-cn 23188  df-cnp 23189  df-cmp 23348  df-nlly 23428  df-tx 23523  df-xko 23524

This theorem is referenced by:  xkohmeo  23776