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

Theorem xkocnv 22106
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 769 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
2 xkohmeo.x . . . . . . . . 9 (𝜑𝐽 ∈ (TopOn‘𝑋))
32adantr 481 . . . . . . . 8 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐽 ∈ (TopOn‘𝑋))
4 xkohmeo.y . . . . . . . . 9 (𝜑𝐾 ∈ (TopOn‘𝑌))
54adantr 481 . . . . . . . 8 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐾 ∈ (TopOn‘𝑌))
6 txtopon 21883 . . . . . . . . . . . . . 14 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
72, 4, 6syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
87adantr 481 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
9 xkohmeo.l . . . . . . . . . . . . . 14 (𝜑𝐿 ∈ Top)
10 toptopon2 21210 . . . . . . . . . . . . . 14 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘ 𝐿))
119, 10sylib 219 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ (TopOn‘ 𝐿))
1211adantr 481 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐿 ∈ (TopOn‘ 𝐿))
13 simpr 485 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
14 cnf2 21541 . . . . . . . . . . . 12 (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (TopOn‘ 𝐿) ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓:(𝑋 × 𝑌)⟶ 𝐿)
158, 12, 13, 14syl3anc 1364 . . . . . . . . . . 11 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓:(𝑋 × 𝑌)⟶ 𝐿)
1615ffnd 6386 . . . . . . . . . 10 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 Fn (𝑋 × 𝑌))
17 fnov 7141 . . . . . . . . . 10 (𝑓 Fn (𝑋 × 𝑌) ↔ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
1816, 17sylib 219 . . . . . . . . 9 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
1918, 13eqeltrrd 2883 . . . . . . . 8 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
203, 5, 19cnmpt2k 21980 . . . . . . 7 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))) ∈ (𝐽 Cn (𝐿 ^ko 𝐾)))
2120adantrr 713 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))) ∈ (𝐽 Cn (𝐿 ^ko 𝐾)))
221, 21eqeltrd 2882 . . . . 5 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)))
2318adantrr 713 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
24 eqid 2794 . . . . . . 7 𝑋 = 𝑋
25 nfv 1893 . . . . . . . . 9 𝑥𝜑
26 nfv 1893 . . . . . . . . . 10 𝑥 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)
27 nfmpt1 5061 . . . . . . . . . . 11 𝑥(𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
2827nfeq2 2963 . . . . . . . . . 10 𝑥 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
2926, 28nfan 1882 . . . . . . . . 9 𝑥(𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
3025, 29nfan 1882 . . . . . . . 8 𝑥(𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))))
31 nfv 1893 . . . . . . . . . . . . 13 𝑦𝜑
32 nfv 1893 . . . . . . . . . . . . . 14 𝑦 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)
33 nfcv 2948 . . . . . . . . . . . . . . . 16 𝑦𝑋
34 nfmpt1 5061 . . . . . . . . . . . . . . . 16 𝑦(𝑦𝑌 ↦ (𝑥𝑓𝑦))
3533, 34nfmpt 5060 . . . . . . . . . . . . . . 15 𝑦(𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
3635nfeq2 2963 . . . . . . . . . . . . . 14 𝑦 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
3732, 36nfan 1882 . . . . . . . . . . . . 13 𝑦(𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
3831, 37nfan 1882 . . . . . . . . . . . 12 𝑦(𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))))
39 nfv 1893 . . . . . . . . . . . 12 𝑦 𝑥𝑋
4038, 39nfan 1882 . . . . . . . . . . 11 𝑦((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥𝑋)
41 simplrr 774 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
4241fveq1d 6543 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑔𝑥) = ((𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥))
43 simprl 767 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑥𝑋)
44 toponmax 21218 . . . . . . . . . . . . . . . . . . 19 (𝐾 ∈ (TopOn‘𝑌) → 𝑌𝐾)
454, 44syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑌𝐾)
4645ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑌𝐾)
4746mptexd 6856 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑦𝑌 ↦ (𝑥𝑓𝑦)) ∈ V)
48 eqid 2794 . . . . . . . . . . . . . . . . 17 (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))) = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
4948fvmpt2 6648 . . . . . . . . . . . . . . . 16 ((𝑥𝑋 ∧ (𝑦𝑌 ↦ (𝑥𝑓𝑦)) ∈ V) → ((𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥) = (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
5043, 47, 49syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥) = (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
5142, 50eqtrd 2830 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑔𝑥) = (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
5251fveq1d 6543 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑔𝑥)‘𝑦) = ((𝑦𝑌 ↦ (𝑥𝑓𝑦))‘𝑦))
53 simprr 769 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑦𝑌)
54 ovex 7051 . . . . . . . . . . . . . 14 (𝑥𝑓𝑦) ∈ V
55 eqid 2794 . . . . . . . . . . . . . . 15 (𝑦𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦𝑌 ↦ (𝑥𝑓𝑦))
5655fvmpt2 6648 . . . . . . . . . . . . . 14 ((𝑦𝑌 ∧ (𝑥𝑓𝑦) ∈ V) → ((𝑦𝑌 ↦ (𝑥𝑓𝑦))‘𝑦) = (𝑥𝑓𝑦))
5753, 54, 56sylancl 586 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑦𝑌 ↦ (𝑥𝑓𝑦))‘𝑦) = (𝑥𝑓𝑦))
5852, 57eqtrd 2830 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦))
5958expr 457 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥𝑋) → (𝑦𝑌 → ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦)))
6040, 59ralrimi 3182 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥𝑋) → ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦))
61 eqid 2794 . . . . . . . . . 10 𝑌 = 𝑌
6260, 61jctil 520 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥𝑋) → (𝑌 = 𝑌 ∧ ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦)))
6362ex 413 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥𝑋 → (𝑌 = 𝑌 ∧ ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦))))
6430, 63ralrimi 3182 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → ∀𝑥𝑋 (𝑌 = 𝑌 ∧ ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦)))
65 mpoeq123 7087 . . . . . . 7 ((𝑋 = 𝑋 ∧ ∀𝑥𝑋 (𝑌 = 𝑌 ∧ ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦))) → (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
6624, 64, 65sylancr 587 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
6723, 66eqtr4d 2833 . . . . 5 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
6822, 67jca 512 . . . 4 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
69 simprr 769 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
702adantr 481 . . . . . . . 8 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝐽 ∈ (TopOn‘𝑋))
714adantr 481 . . . . . . . 8 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝐾 ∈ (TopOn‘𝑌))
7211adantr 481 . . . . . . . 8 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝐿 ∈ (TopOn‘ 𝐿))
73 xkohmeo.k . . . . . . . . 9 (𝜑𝐾 ∈ 𝑛-Locally Comp)
7473adantr 481 . . . . . . . 8 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝐾 ∈ 𝑛-Locally Comp)
75 nllytop 21765 . . . . . . . . . . . . . 14 (𝐾 ∈ 𝑛-Locally Comp → 𝐾 ∈ Top)
7674, 75syl 17 . . . . . . . . . . . . 13 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝐾 ∈ Top)
779adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝐿 ∈ Top)
78 eqid 2794 . . . . . . . . . . . . . 14 (𝐿 ^ko 𝐾) = (𝐿 ^ko 𝐾)
7978xkotopon 21892 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐿 ^ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)))
8076, 77, 79syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → (𝐿 ^ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)))
81 simpr 485 . . . . . . . . . . . 12 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)))
82 cnf2 21541 . . . . . . . . . . . 12 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐿 ^ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)) ∧ 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝑔:𝑋⟶(𝐾 Cn 𝐿))
8370, 80, 81, 82syl3anc 1364 . . . . . . . . . . 11 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝑔:𝑋⟶(𝐾 Cn 𝐿))
8483feqmptd 6604 . . . . . . . . . 10 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝑔 = (𝑥𝑋 ↦ (𝑔𝑥)))
854ad2antrr 722 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) ∧ 𝑥𝑋) → 𝐾 ∈ (TopOn‘𝑌))
8611ad2antrr 722 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) ∧ 𝑥𝑋) → 𝐿 ∈ (TopOn‘ 𝐿))
8783ffvelrnda 6719 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) ∧ 𝑥𝑋) → (𝑔𝑥) ∈ (𝐾 Cn 𝐿))
88 cnf2 21541 . . . . . . . . . . . . 13 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘ 𝐿) ∧ (𝑔𝑥) ∈ (𝐾 Cn 𝐿)) → (𝑔𝑥):𝑌 𝐿)
8985, 86, 87, 88syl3anc 1364 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) ∧ 𝑥𝑋) → (𝑔𝑥):𝑌 𝐿)
9089feqmptd 6604 . . . . . . . . . . 11 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) ∧ 𝑥𝑋) → (𝑔𝑥) = (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
9190mpteq2dva 5058 . . . . . . . . . 10 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → (𝑥𝑋 ↦ (𝑔𝑥)) = (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
9284, 91eqtrd 2830 . . . . . . . . 9 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
9392, 81eqeltrrd 2883 . . . . . . . 8 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))) ∈ (𝐽 Cn (𝐿 ^ko 𝐾)))
9470, 71, 72, 74, 93cnmptk2 21978 . . . . . . 7 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
9594adantrr 713 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
9669, 95eqeltrd 2882 . . . . 5 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
9792adantrr 713 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
98 nfv 1893 . . . . . . . . 9 𝑥 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))
99 nfmpo1 7095 . . . . . . . . . 10 𝑥(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
10099nfeq2 2963 . . . . . . . . 9 𝑥 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
10198, 100nfan 1882 . . . . . . . 8 𝑥(𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
10225, 101nfan 1882 . . . . . . 7 𝑥(𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
103 nfv 1893 . . . . . . . . . . . 12 𝑦 𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾))
104 nfmpo2 7096 . . . . . . . . . . . . 13 𝑦(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
105104nfeq2 2963 . . . . . . . . . . . 12 𝑦 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
106103, 105nfan 1882 . . . . . . . . . . 11 𝑦(𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
10731, 106nfan 1882 . . . . . . . . . 10 𝑦(𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
108107, 39nfan 1882 . . . . . . . . 9 𝑦((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ 𝑥𝑋)
10969oveqd 7036 . . . . . . . . . . 11 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → (𝑥𝑓𝑦) = (𝑥(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))𝑦))
110 fvex 6554 . . . . . . . . . . . 12 ((𝑔𝑥)‘𝑦) ∈ V
111 eqid 2794 . . . . . . . . . . . . 13 (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
112111ovmpt4g 7156 . . . . . . . . . . . 12 ((𝑥𝑋𝑦𝑌 ∧ ((𝑔𝑥)‘𝑦) ∈ V) → (𝑥(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))𝑦) = ((𝑔𝑥)‘𝑦))
113110, 112mp3an3 1442 . . . . . . . . . . 11 ((𝑥𝑋𝑦𝑌) → (𝑥(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))𝑦) = ((𝑔𝑥)‘𝑦))
114109, 113sylan9eq 2850 . . . . . . . . . 10 (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑥𝑓𝑦) = ((𝑔𝑥)‘𝑦))
115114expr 457 . . . . . . . . 9 (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ 𝑥𝑋) → (𝑦𝑌 → (𝑥𝑓𝑦) = ((𝑔𝑥)‘𝑦)))
116108, 115ralrimi 3182 . . . . . . . 8 (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ 𝑥𝑋) → ∀𝑦𝑌 (𝑥𝑓𝑦) = ((𝑔𝑥)‘𝑦))
117 mpteq12 5050 . . . . . . . 8 ((𝑌 = 𝑌 ∧ ∀𝑦𝑌 (𝑥𝑓𝑦) = ((𝑔𝑥)‘𝑦)) → (𝑦𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
11861, 116, 117sylancr 587 . . . . . . 7 (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ 𝑥𝑋) → (𝑦𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
119102, 118mpteq2da 5057 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))) = (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
12097, 119eqtr4d 2833 . . . . 5 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
12196, 120jca 512 . . . 4 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))))
12268, 121impbida 797 . . 3 (𝜑 → ((𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))) ↔ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))))
123122opabbidv 5030 . 2 (𝜑 → {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))} = {⟨𝑔, 𝑓⟩ ∣ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))})
124 xkohmeo.f . . . . 5 𝐹 = (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
125 df-mpt 5044 . . . . 5 (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))) = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
126124, 125eqtri 2818 . . . 4 𝐹 = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
127126cnveqi 5634 . . 3 𝐹 = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
128 cnvopab 5876 . . 3 {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))} = {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
129127, 128eqtri 2818 . 2 𝐹 = {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
130 df-mpt 5044 . 2 (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ↦ (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))) = {⟨𝑔, 𝑓⟩ ∣ (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))}
131123, 129, 1303eqtr4g 2855 1 (𝜑𝐹 = (𝑔 ∈ (𝐽 Cn (𝐿 ^ko 𝐾)) ↦ (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1522  wcel 2080  wral 3104  Vcvv 3436   cuni 4747  {copab 5026  cmpt 5043   × cxp 5444  ccnv 5445   Fn wfn 6223  wf 6224  cfv 6228  (class class class)co 7019  cmpo 7021  Topctop 21185  TopOnctopon 21202   Cn ccn 21516  Compccmp 21678  𝑛-Locally cnlly 21757   ×t ctx 21852   ^ko cxko 21853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-13 2343  ax-ext 2768  ax-rep 5084  ax-sep 5097  ax-nul 5104  ax-pow 5160  ax-pr 5224  ax-un 7322
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-mo 2575  df-eu 2611  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ne 2984  df-ral 3109  df-rex 3110  df-reu 3111  df-rab 3113  df-v 3438  df-sbc 3708  df-csb 3814  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-pss 3878  df-nul 4214  df-if 4384  df-pw 4457  df-sn 4475  df-pr 4477  df-tp 4479  df-op 4481  df-uni 4748  df-int 4785  df-iun 4829  df-iin 4830  df-br 4965  df-opab 5027  df-mpt 5044  df-tr 5067  df-id 5351  df-eprel 5356  df-po 5365  df-so 5366  df-fr 5405  df-we 5407  df-xp 5452  df-rel 5453  df-cnv 5454  df-co 5455  df-dm 5456  df-rn 5457  df-res 5458  df-ima 5459  df-pred 6026  df-ord 6072  df-on 6073  df-lim 6074  df-suc 6075  df-iota 6192  df-fun 6230  df-fn 6231  df-f 6232  df-f1 6233  df-fo 6234  df-f1o 6235  df-fv 6236  df-ov 7022  df-oprab 7023  df-mpo 7024  df-om 7440  df-1st 7548  df-2nd 7549  df-wrecs 7801  df-recs 7863  df-rdg 7901  df-1o 7956  df-2o 7957  df-oadd 7960  df-er 8142  df-map 8261  df-ixp 8314  df-en 8361  df-dom 8362  df-sdom 8363  df-fin 8364  df-fi 8724  df-rest 16525  df-topgen 16546  df-pt 16547  df-top 21186  df-topon 21203  df-bases 21238  df-ntr 21312  df-nei 21390  df-cn 21519  df-cnp 21520  df-cmp 21679  df-nlly 21759  df-tx 21854  df-xko 21855
This theorem is referenced by:  xkohmeo  22107
  Copyright terms: Public domain W3C validator