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

Theorem xkocnv 23165
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 771 . . . . . 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 22942 . . . . . . . . . . . . . 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 22267 . . . . . . . . . . . . . 14 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘ 𝐿))
119, 10sylib 217 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ (TopOn‘ 𝐿))
1211adantr 481 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐿 ∈ (TopOn‘ 𝐿))
13 simpr 485 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
14 cnf2 22600 . . . . . . . . . . . 12 (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (TopOn‘ 𝐿) ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓:(𝑋 × 𝑌)⟶ 𝐿)
158, 12, 13, 14syl3anc 1371 . . . . . . . . . . 11 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓:(𝑋 × 𝑌)⟶ 𝐿)
1615ffnd 6669 . . . . . . . . . 10 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 Fn (𝑋 × 𝑌))
17 fnov 7487 . . . . . . . . . 10 (𝑓 Fn (𝑋 × 𝑌) ↔ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
1816, 17sylib 217 . . . . . . . . 9 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
1918, 13eqeltrrd 2839 . . . . . . . 8 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
203, 5, 19cnmpt2k 23039 . . . . . . 7 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))) ∈ (𝐽 Cn (𝐿ko 𝐾)))
2120adantrr 715 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))) ∈ (𝐽 Cn (𝐿ko 𝐾)))
221, 21eqeltrd 2838 . . . . 5 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)))
2318adantrr 715 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
24 eqid 2736 . . . . . . 7 𝑋 = 𝑋
25 nfv 1917 . . . . . . . . 9 𝑥𝜑
26 nfv 1917 . . . . . . . . . 10 𝑥 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)
27 nfmpt1 5213 . . . . . . . . . . 11 𝑥(𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
2827nfeq2 2924 . . . . . . . . . 10 𝑥 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
2926, 28nfan 1902 . . . . . . . . 9 𝑥(𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
3025, 29nfan 1902 . . . . . . . 8 𝑥(𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))))
31 nfv 1917 . . . . . . . . . . . . 13 𝑦𝜑
32 nfv 1917 . . . . . . . . . . . . . 14 𝑦 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)
33 nfcv 2907 . . . . . . . . . . . . . . . 16 𝑦𝑋
34 nfmpt1 5213 . . . . . . . . . . . . . . . 16 𝑦(𝑦𝑌 ↦ (𝑥𝑓𝑦))
3533, 34nfmpt 5212 . . . . . . . . . . . . . . 15 𝑦(𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
3635nfeq2 2924 . . . . . . . . . . . . . 14 𝑦 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
3732, 36nfan 1902 . . . . . . . . . . . . 13 𝑦(𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
3831, 37nfan 1902 . . . . . . . . . . . 12 𝑦(𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))))
39 nfv 1917 . . . . . . . . . . . 12 𝑦 𝑥𝑋
4038, 39nfan 1902 . . . . . . . . . . 11 𝑦((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥𝑋)
41 simplrr 776 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
4241fveq1d 6844 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑔𝑥) = ((𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥))
43 simprl 769 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑥𝑋)
44 toponmax 22275 . . . . . . . . . . . . . . . . . . 19 (𝐾 ∈ (TopOn‘𝑌) → 𝑌𝐾)
454, 44syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑌𝐾)
4645ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑌𝐾)
4746mptexd 7174 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑦𝑌 ↦ (𝑥𝑓𝑦)) ∈ V)
48 eqid 2736 . . . . . . . . . . . . . . . . 17 (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))) = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
4948fvmpt2 6959 . . . . . . . . . . . . . . . 16 ((𝑥𝑋 ∧ (𝑦𝑌 ↦ (𝑥𝑓𝑦)) ∈ V) → ((𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥) = (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
5043, 47, 49syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥) = (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
5142, 50eqtrd 2776 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑔𝑥) = (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
5251fveq1d 6844 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑔𝑥)‘𝑦) = ((𝑦𝑌 ↦ (𝑥𝑓𝑦))‘𝑦))
53 simprr 771 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑦𝑌)
54 ovex 7390 . . . . . . . . . . . . . 14 (𝑥𝑓𝑦) ∈ V
55 eqid 2736 . . . . . . . . . . . . . . 15 (𝑦𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦𝑌 ↦ (𝑥𝑓𝑦))
5655fvmpt2 6959 . . . . . . . . . . . . . 14 ((𝑦𝑌 ∧ (𝑥𝑓𝑦) ∈ V) → ((𝑦𝑌 ↦ (𝑥𝑓𝑦))‘𝑦) = (𝑥𝑓𝑦))
5753, 54, 56sylancl 586 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑦𝑌 ↦ (𝑥𝑓𝑦))‘𝑦) = (𝑥𝑓𝑦))
5852, 57eqtrd 2776 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦))
5958expr 457 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥𝑋) → (𝑦𝑌 → ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦)))
6040, 59ralrimi 3240 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥𝑋) → ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦))
61 eqid 2736 . . . . . . . . . 10 𝑌 = 𝑌
6260, 61jctil 520 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥𝑋) → (𝑌 = 𝑌 ∧ ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦)))
6362ex 413 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥𝑋 → (𝑌 = 𝑌 ∧ ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦))))
6430, 63ralrimi 3240 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → ∀𝑥𝑋 (𝑌 = 𝑌 ∧ ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦)))
65 mpoeq123 7429 . . . . . . 7 ((𝑋 = 𝑋 ∧ ∀𝑥𝑋 (𝑌 = 𝑌 ∧ ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦))) → (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
6624, 64, 65sylancr 587 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
6723, 66eqtr4d 2779 . . . . 5 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
6822, 67jca 512 . . . 4 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
69 simprr 771 . . . . . 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 22824 . . . . . . . . . . . . . 14 (𝐾 ∈ 𝑛-Locally Comp → 𝐾 ∈ Top)
7674, 75syl 17 . . . . . . . . . . . . 13 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝐾 ∈ Top)
779adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝐿 ∈ Top)
78 eqid 2736 . . . . . . . . . . . . . 14 (𝐿ko 𝐾) = (𝐿ko 𝐾)
7978xkotopon 22951 . . . . . . . . . . . . 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 22600 . . . . . . . . . . . 12 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐿ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)) ∧ 𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝑔:𝑋⟶(𝐾 Cn 𝐿))
8370, 80, 81, 82syl3anc 1371 . . . . . . . . . . 11 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝑔:𝑋⟶(𝐾 Cn 𝐿))
8483feqmptd 6910 . . . . . . . . . 10 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝑔 = (𝑥𝑋 ↦ (𝑔𝑥)))
854ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) ∧ 𝑥𝑋) → 𝐾 ∈ (TopOn‘𝑌))
8611ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) ∧ 𝑥𝑋) → 𝐿 ∈ (TopOn‘ 𝐿))
8783ffvelcdmda 7035 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) ∧ 𝑥𝑋) → (𝑔𝑥) ∈ (𝐾 Cn 𝐿))
88 cnf2 22600 . . . . . . . . . . . . 13 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘ 𝐿) ∧ (𝑔𝑥) ∈ (𝐾 Cn 𝐿)) → (𝑔𝑥):𝑌 𝐿)
8985, 86, 87, 88syl3anc 1371 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) ∧ 𝑥𝑋) → (𝑔𝑥):𝑌 𝐿)
9089feqmptd 6910 . . . . . . . . . . 11 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) ∧ 𝑥𝑋) → (𝑔𝑥) = (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
9190mpteq2dva 5205 . . . . . . . . . 10 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → (𝑥𝑋 ↦ (𝑔𝑥)) = (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
9284, 91eqtrd 2776 . . . . . . . . 9 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
9392, 81eqeltrrd 2839 . . . . . . . 8 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))) ∈ (𝐽 Cn (𝐿ko 𝐾)))
9470, 71, 72, 74, 93cnmptk2 23037 . . . . . . 7 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
9594adantrr 715 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
9669, 95eqeltrd 2838 . . . . 5 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
9792adantrr 715 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
98 nfv 1917 . . . . . . . . 9 𝑥 𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))
99 nfmpo1 7437 . . . . . . . . . 10 𝑥(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
10099nfeq2 2924 . . . . . . . . 9 𝑥 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
10198, 100nfan 1902 . . . . . . . 8 𝑥(𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
10225, 101nfan 1902 . . . . . . 7 𝑥(𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
103 nfv 1917 . . . . . . . . . . . 12 𝑦 𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))
104 nfmpo2 7438 . . . . . . . . . . . . 13 𝑦(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
105104nfeq2 2924 . . . . . . . . . . . 12 𝑦 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
106103, 105nfan 1902 . . . . . . . . . . 11 𝑦(𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
10731, 106nfan 1902 . . . . . . . . . 10 𝑦(𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
108107, 39nfan 1902 . . . . . . . . 9 𝑦((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ 𝑥𝑋)
10969oveqd 7374 . . . . . . . . . . 11 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → (𝑥𝑓𝑦) = (𝑥(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))𝑦))
110 fvex 6855 . . . . . . . . . . . 12 ((𝑔𝑥)‘𝑦) ∈ V
111 eqid 2736 . . . . . . . . . . . . 13 (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
112111ovmpt4g 7502 . . . . . . . . . . . 12 ((𝑥𝑋𝑦𝑌 ∧ ((𝑔𝑥)‘𝑦) ∈ V) → (𝑥(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))𝑦) = ((𝑔𝑥)‘𝑦))
113110, 112mp3an3 1450 . . . . . . . . . . 11 ((𝑥𝑋𝑦𝑌) → (𝑥(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))𝑦) = ((𝑔𝑥)‘𝑦))
114109, 113sylan9eq 2796 . . . . . . . . . 10 (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑥𝑓𝑦) = ((𝑔𝑥)‘𝑦))
115114expr 457 . . . . . . . . 9 (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ 𝑥𝑋) → (𝑦𝑌 → (𝑥𝑓𝑦) = ((𝑔𝑥)‘𝑦)))
116108, 115ralrimi 3240 . . . . . . . 8 (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ 𝑥𝑋) → ∀𝑦𝑌 (𝑥𝑓𝑦) = ((𝑔𝑥)‘𝑦))
117 mpteq12 5197 . . . . . . . 8 ((𝑌 = 𝑌 ∧ ∀𝑦𝑌 (𝑥𝑓𝑦) = ((𝑔𝑥)‘𝑦)) → (𝑦𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
11861, 116, 117sylancr 587 . . . . . . 7 (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ 𝑥𝑋) → (𝑦𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
119102, 118mpteq2da 5203 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))) = (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
12097, 119eqtr4d 2779 . . . . 5 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
12196, 120jca 512 . . . 4 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))))
12268, 121impbida 799 . . 3 (𝜑 → ((𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))) ↔ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))))
123122opabbidv 5171 . 2 (𝜑 → {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))} = {⟨𝑔, 𝑓⟩ ∣ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))})
124 xkohmeo.f . . . . 5 𝐹 = (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
125 df-mpt 5189 . . . . 5 (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))) = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
126124, 125eqtri 2764 . . . 4 𝐹 = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
127126cnveqi 5830 . . 3 𝐹 = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
128 cnvopab 6091 . . 3 {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))} = {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
129127, 128eqtri 2764 . 2 𝐹 = {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
130 df-mpt 5189 . 2 (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ↦ (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))) = {⟨𝑔, 𝑓⟩ ∣ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))}
131123, 129, 1303eqtr4g 2801 1 (𝜑𝐹 = (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ↦ (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  wral 3064  Vcvv 3445   cuni 4865  {copab 5167  cmpt 5188   × cxp 5631  ccnv 5632   Fn wfn 6491  wf 6492  cfv 6496  (class class class)co 7357  cmpo 7359  Topctop 22242  TopOnctopon 22259   Cn ccn 22575  Compccmp 22737  𝑛-Locally cnlly 22816   ×t ctx 22911  ko cxko 22912
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-1o 8412  df-er 8648  df-map 8767  df-ixp 8836  df-en 8884  df-dom 8885  df-fin 8887  df-fi 9347  df-rest 17304  df-topgen 17325  df-pt 17326  df-top 22243  df-topon 22260  df-bases 22296  df-ntr 22371  df-nei 22449  df-cn 22578  df-cnp 22579  df-cmp 22738  df-nlly 22818  df-tx 22913  df-xko 22914
This theorem is referenced by:  xkohmeo  23166
  Copyright terms: Public domain W3C validator