MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xkocnv Structured version   Visualization version   GIF version

Theorem xkocnv 21837
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
StepHypRef Expression
1 simprr 748 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
2 xkohmeo.x . . . . . . . . 9 (𝜑𝐽 ∈ (TopOn‘𝑋))
32adantr 466 . . . . . . . 8 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐽 ∈ (TopOn‘𝑋))
4 xkohmeo.y . . . . . . . . 9 (𝜑𝐾 ∈ (TopOn‘𝑌))
54adantr 466 . . . . . . . 8 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐾 ∈ (TopOn‘𝑌))
6 txtopon 21614 . . . . . . . . . . . . . 14 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
72, 4, 6syl2anc 565 . . . . . . . . . . . . 13 (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
87adantr 466 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
9 xkohmeo.l . . . . . . . . . . . . . 14 (𝜑𝐿 ∈ Top)
10 eqid 2770 . . . . . . . . . . . . . . 15 𝐿 = 𝐿
1110toptopon 20941 . . . . . . . . . . . . . 14 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘ 𝐿))
129, 11sylib 208 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ (TopOn‘ 𝐿))
1312adantr 466 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐿 ∈ (TopOn‘ 𝐿))
14 simpr 471 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
15 cnf2 21273 . . . . . . . . . . . 12 (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (TopOn‘ 𝐿) ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓:(𝑋 × 𝑌)⟶ 𝐿)
168, 13, 14, 15syl3anc 1475 . . . . . . . . . . 11 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓:(𝑋 × 𝑌)⟶ 𝐿)
17 ffn 6185 . . . . . . . . . . 11 (𝑓:(𝑋 × 𝑌)⟶ 𝐿𝑓 Fn (𝑋 × 𝑌))
1816, 17syl 17 . . . . . . . . . 10 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 Fn (𝑋 × 𝑌))
19 fnov 6914 . . . . . . . . . 10 (𝑓 Fn (𝑋 × 𝑌) ↔ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
2018, 19sylib 208 . . . . . . . . 9 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
2120, 14eqeltrrd 2850 . . . . . . . 8 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
223, 5, 21cnmpt2k 21711 . . . . . . 7 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))) ∈ (𝐽 Cn (𝐿 ^ko 𝐾)))
2322adantrr 688 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))) ∈ (𝐽 Cn (𝐿 ^ko 𝐾)))
241, 23eqeltrd 2849 . . . . 5 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)))
2520adantrr 688 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
26 eqid 2770 . . . . . . 7 𝑋 = 𝑋
27 nfv 1994 . . . . . . . . 9 𝑥𝜑
28 nfv 1994 . . . . . . . . . 10 𝑥 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)
29 nfmpt1 4879 . . . . . . . . . . 11 𝑥(𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
3029nfeq2 2928 . . . . . . . . . 10 𝑥 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
3128, 30nfan 1979 . . . . . . . . 9 𝑥(𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
3227, 31nfan 1979 . . . . . . . 8 𝑥(𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))))
33 nfv 1994 . . . . . . . . . . . . 13 𝑦𝜑
34 nfv 1994 . . . . . . . . . . . . . 14 𝑦 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)
35 nfcv 2912 . . . . . . . . . . . . . . . 16 𝑦𝑋
36 nfmpt1 4879 . . . . . . . . . . . . . . . 16 𝑦(𝑦𝑌 ↦ (𝑥𝑓𝑦))
3735, 36nfmpt 4878 . . . . . . . . . . . . . . 15 𝑦(𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
3837nfeq2 2928 . . . . . . . . . . . . . 14 𝑦 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
3934, 38nfan 1979 . . . . . . . . . . . . 13 𝑦(𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
4033, 39nfan 1979 . . . . . . . . . . . 12 𝑦(𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))))
41 nfv 1994 . . . . . . . . . . . 12 𝑦 𝑥𝑋
4240, 41nfan 1979 . . . . . . . . . . 11 𝑦((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥𝑋)
43 simplrr 755 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
4443fveq1d 6334 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑔𝑥) = ((𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥))
45 simprl 746 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑥𝑋)
46 toponmax 20950 . . . . . . . . . . . . . . . . . . 19 (𝐾 ∈ (TopOn‘𝑌) → 𝑌𝐾)
474, 46syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑌𝐾)
4847ad2antrr 697 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑌𝐾)
49 mptexg 6627 . . . . . . . . . . . . . . . . 17 (𝑌𝐾 → (𝑦𝑌 ↦ (𝑥𝑓𝑦)) ∈ V)
5048, 49syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑦𝑌 ↦ (𝑥𝑓𝑦)) ∈ V)
51 eqid 2770 . . . . . . . . . . . . . . . . 17 (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))) = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
5251fvmpt2 6433 . . . . . . . . . . . . . . . 16 ((𝑥𝑋 ∧ (𝑦𝑌 ↦ (𝑥𝑓𝑦)) ∈ V) → ((𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥) = (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
5345, 50, 52syl2anc 565 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥) = (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
5444, 53eqtrd 2804 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑔𝑥) = (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
5554fveq1d 6334 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑔𝑥)‘𝑦) = ((𝑦𝑌 ↦ (𝑥𝑓𝑦))‘𝑦))
56 simprr 748 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑦𝑌)
57 ovex 6822 . . . . . . . . . . . . . 14 (𝑥𝑓𝑦) ∈ V
58 eqid 2770 . . . . . . . . . . . . . . 15 (𝑦𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦𝑌 ↦ (𝑥𝑓𝑦))
5958fvmpt2 6433 . . . . . . . . . . . . . 14 ((𝑦𝑌 ∧ (𝑥𝑓𝑦) ∈ V) → ((𝑦𝑌 ↦ (𝑥𝑓𝑦))‘𝑦) = (𝑥𝑓𝑦))
6056, 57, 59sylancl 566 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑦𝑌 ↦ (𝑥𝑓𝑦))‘𝑦) = (𝑥𝑓𝑦))
6155, 60eqtrd 2804 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦))
6261expr 444 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥𝑋) → (𝑦𝑌 → ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦)))
6342, 62ralrimi 3105 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥𝑋) → ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦))
64 eqid 2770 . . . . . . . . . 10 𝑌 = 𝑌
6563, 64jctil 503 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥𝑋) → (𝑌 = 𝑌 ∧ ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦)))
6665ex 397 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥𝑋 → (𝑌 = 𝑌 ∧ ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦))))
6732, 66ralrimi 3105 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → ∀𝑥𝑋 (𝑌 = 𝑌 ∧ ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦)))
68 mpt2eq123 6860 . . . . . . 7 ((𝑋 = 𝑋 ∧ ∀𝑥𝑋 (𝑌 = 𝑌 ∧ ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦))) → (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
6926, 67, 68sylancr 567 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
7025, 69eqtr4d 2807 . . . . 5 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
7124, 70jca 495 . . . 4 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
72 simprr 748 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
732adantr 466 . . . . . . . 8 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝐽 ∈ (TopOn‘𝑋))
744adantr 466 . . . . . . . 8 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝐾 ∈ (TopOn‘𝑌))
7512adantr 466 . . . . . . . 8 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝐿 ∈ (TopOn‘ 𝐿))
76 xkohmeo.k . . . . . . . . 9 (𝜑𝐾 ∈ 𝑛-Locally Comp)
7776adantr 466 . . . . . . . 8 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝐾 ∈ 𝑛-Locally Comp)
78 nllytop 21496 . . . . . . . . . . . . . 14 (𝐾 ∈ 𝑛-Locally Comp → 𝐾 ∈ Top)
7977, 78syl 17 . . . . . . . . . . . . 13 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝐾 ∈ Top)
809adantr 466 . . . . . . . . . . . . 13 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝐿 ∈ Top)
81 eqid 2770 . . . . . . . . . . . . . 14 (𝐿 ^ko 𝐾) = (𝐿 ^ko 𝐾)
8281xkotopon 21623 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐿 ^ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)))
8379, 80, 82syl2anc 565 . . . . . . . . . . . 12 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → (𝐿 ^ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)))
84 simpr 471 . . . . . . . . . . . 12 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)))
85 cnf2 21273 . . . . . . . . . . . 12 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐿 ^ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)) ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝑔:𝑋⟶(𝐾 Cn 𝐿))
8673, 83, 84, 85syl3anc 1475 . . . . . . . . . . 11 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝑔:𝑋⟶(𝐾 Cn 𝐿))
8786feqmptd 6391 . . . . . . . . . 10 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝑔 = (𝑥𝑋 ↦ (𝑔𝑥)))
884ad2antrr 697 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) ∧ 𝑥𝑋) → 𝐾 ∈ (TopOn‘𝑌))
8912ad2antrr 697 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) ∧ 𝑥𝑋) → 𝐿 ∈ (TopOn‘ 𝐿))
9086ffvelrnda 6502 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) ∧ 𝑥𝑋) → (𝑔𝑥) ∈ (𝐾 Cn 𝐿))
91 cnf2 21273 . . . . . . . . . . . . 13 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘ 𝐿) ∧ (𝑔𝑥) ∈ (𝐾 Cn 𝐿)) → (𝑔𝑥):𝑌 𝐿)
9288, 89, 90, 91syl3anc 1475 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) ∧ 𝑥𝑋) → (𝑔𝑥):𝑌 𝐿)
9392feqmptd 6391 . . . . . . . . . . 11 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) ∧ 𝑥𝑋) → (𝑔𝑥) = (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
9493mpteq2dva 4876 . . . . . . . . . 10 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → (𝑥𝑋 ↦ (𝑔𝑥)) = (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
9587, 94eqtrd 2804 . . . . . . . . 9 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
9695, 84eqeltrrd 2850 . . . . . . . 8 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))) ∈ (𝐽 Cn (𝐿 ^ko 𝐾)))
9773, 74, 75, 77, 96cnmptk2 21709 . . . . . . 7 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
9897adantrr 688 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
9972, 98eqeltrd 2849 . . . . 5 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
10095adantrr 688 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
101 nfv 1994 . . . . . . . . 9 𝑥 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))
102 nfmpt21 6868 . . . . . . . . . 10 𝑥(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
103102nfeq2 2928 . . . . . . . . 9 𝑥 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
104101, 103nfan 1979 . . . . . . . 8 𝑥(𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
10527, 104nfan 1979 . . . . . . 7 𝑥(𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
106 nfv 1994 . . . . . . . . . . . 12 𝑦 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))
107 nfmpt22 6869 . . . . . . . . . . . . 13 𝑦(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
108107nfeq2 2928 . . . . . . . . . . . 12 𝑦 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
109106, 108nfan 1979 . . . . . . . . . . 11 𝑦(𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
11033, 109nfan 1979 . . . . . . . . . 10 𝑦(𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
111110, 41nfan 1979 . . . . . . . . 9 𝑦((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ 𝑥𝑋)
11272oveqd 6809 . . . . . . . . . . 11 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → (𝑥𝑓𝑦) = (𝑥(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))𝑦))
113 fvex 6342 . . . . . . . . . . . 12 ((𝑔𝑥)‘𝑦) ∈ V
114 eqid 2770 . . . . . . . . . . . . 13 (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
115114ovmpt4g 6929 . . . . . . . . . . . 12 ((𝑥𝑋𝑦𝑌 ∧ ((𝑔𝑥)‘𝑦) ∈ V) → (𝑥(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))𝑦) = ((𝑔𝑥)‘𝑦))
116113, 115mp3an3 1560 . . . . . . . . . . 11 ((𝑥𝑋𝑦𝑌) → (𝑥(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))𝑦) = ((𝑔𝑥)‘𝑦))
117112, 116sylan9eq 2824 . . . . . . . . . 10 (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑥𝑓𝑦) = ((𝑔𝑥)‘𝑦))
118117expr 444 . . . . . . . . 9 (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ 𝑥𝑋) → (𝑦𝑌 → (𝑥𝑓𝑦) = ((𝑔𝑥)‘𝑦)))
119111, 118ralrimi 3105 . . . . . . . 8 (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ 𝑥𝑋) → ∀𝑦𝑌 (𝑥𝑓𝑦) = ((𝑔𝑥)‘𝑦))
120 mpteq12 4868 . . . . . . . 8 ((𝑌 = 𝑌 ∧ ∀𝑦𝑌 (𝑥𝑓𝑦) = ((𝑔𝑥)‘𝑦)) → (𝑦𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
12164, 119, 120sylancr 567 . . . . . . 7 (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ 𝑥𝑋) → (𝑦𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
122105, 121mpteq2da 4875 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))) = (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
123100, 122eqtr4d 2807 . . . . 5 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
12499, 123jca 495 . . . 4 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))))
12571, 124impbida 794 . . 3 (𝜑 → ((𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))) ↔ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))))
126125opabbidv 4848 . 2 (𝜑 → {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))} = {⟨𝑔, 𝑓⟩ ∣ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))})
127 xkohmeo.f . . . . 5 𝐹 = (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
128 df-mpt 4862 . . . . 5 (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))) = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
129127, 128eqtri 2792 . . . 4 𝐹 = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
130129cnveqi 5435 . . 3 𝐹 = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
131 cnvopab 5674 . . 3 {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))} = {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
132130, 131eqtri 2792 . 2 𝐹 = {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
133 df-mpt 4862 . 2 (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ↦ (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))) = {⟨𝑔, 𝑓⟩ ∣ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))}
134126, 132, 1333eqtr4g 2829 1 (𝜑𝐹 = (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ↦ (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1630  wcel 2144  wral 3060  Vcvv 3349   cuni 4572  {copab 4844  cmpt 4861   × cxp 5247  ccnv 5248   Fn wfn 6026  wf 6027  cfv 6031  (class class class)co 6792  cmpt2 6794  Topctop 20917  TopOnctopon 20934   Cn ccn 21248  Compccmp 21409  𝑛-Locally cnlly 21488   ×t ctx 21583   ^ko cxko 21584
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-rep 4902  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1071  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-ral 3065  df-rex 3066  df-reu 3067  df-rab 3069  df-v 3351  df-sbc 3586  df-csb 3681  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-pss 3737  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-tp 4319  df-op 4321  df-uni 4573  df-int 4610  df-iun 4654  df-iin 4655  df-br 4785  df-opab 4845  df-mpt 4862  df-tr 4885  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-ov 6795  df-oprab 6796  df-mpt2 6797  df-om 7212  df-1st 7314  df-2nd 7315  df-wrecs 7558  df-recs 7620  df-rdg 7658  df-1o 7712  df-2o 7713  df-oadd 7716  df-er 7895  df-map 8010  df-ixp 8062  df-en 8109  df-dom 8110  df-sdom 8111  df-fin 8112  df-fi 8472  df-rest 16290  df-topgen 16311  df-pt 16312  df-top 20918  df-topon 20935  df-bases 20970  df-ntr 21044  df-nei 21122  df-cn 21251  df-cnp 21252  df-cmp 21410  df-nlly 21490  df-tx 21585  df-xko 21586
This theorem is referenced by:  xkohmeo  21838
  Copyright terms: Public domain W3C validator