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

Theorem xkocnv 22558
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 773 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
2 xkohmeo.x . . . . . . . . 9 (𝜑𝐽 ∈ (TopOn‘𝑋))
32adantr 484 . . . . . . . 8 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐽 ∈ (TopOn‘𝑋))
4 xkohmeo.y . . . . . . . . 9 (𝜑𝐾 ∈ (TopOn‘𝑌))
54adantr 484 . . . . . . . 8 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐾 ∈ (TopOn‘𝑌))
6 txtopon 22335 . . . . . . . . . . . . . 14 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
72, 4, 6syl2anc 587 . . . . . . . . . . . . 13 (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
87adantr 484 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
9 xkohmeo.l . . . . . . . . . . . . . 14 (𝜑𝐿 ∈ Top)
10 toptopon2 21662 . . . . . . . . . . . . . 14 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘ 𝐿))
119, 10sylib 221 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ (TopOn‘ 𝐿))
1211adantr 484 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐿 ∈ (TopOn‘ 𝐿))
13 simpr 488 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
14 cnf2 21993 . . . . . . . . . . . 12 (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (TopOn‘ 𝐿) ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓:(𝑋 × 𝑌)⟶ 𝐿)
158, 12, 13, 14syl3anc 1372 . . . . . . . . . . 11 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓:(𝑋 × 𝑌)⟶ 𝐿)
1615ffnd 6499 . . . . . . . . . 10 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 Fn (𝑋 × 𝑌))
17 fnov 7291 . . . . . . . . . 10 (𝑓 Fn (𝑋 × 𝑌) ↔ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
1816, 17sylib 221 . . . . . . . . 9 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
1918, 13eqeltrrd 2834 . . . . . . . 8 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
203, 5, 19cnmpt2k 22432 . . . . . . 7 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))) ∈ (𝐽 Cn (𝐿ko 𝐾)))
2120adantrr 717 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))) ∈ (𝐽 Cn (𝐿ko 𝐾)))
221, 21eqeltrd 2833 . . . . 5 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)))
2318adantrr 717 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
24 eqid 2738 . . . . . . 7 𝑋 = 𝑋
25 nfv 1920 . . . . . . . . 9 𝑥𝜑
26 nfv 1920 . . . . . . . . . 10 𝑥 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)
27 nfmpt1 5125 . . . . . . . . . . 11 𝑥(𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
2827nfeq2 2916 . . . . . . . . . 10 𝑥 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
2926, 28nfan 1905 . . . . . . . . 9 𝑥(𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
3025, 29nfan 1905 . . . . . . . 8 𝑥(𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))))
31 nfv 1920 . . . . . . . . . . . . 13 𝑦𝜑
32 nfv 1920 . . . . . . . . . . . . . 14 𝑦 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)
33 nfcv 2899 . . . . . . . . . . . . . . . 16 𝑦𝑋
34 nfmpt1 5125 . . . . . . . . . . . . . . . 16 𝑦(𝑦𝑌 ↦ (𝑥𝑓𝑦))
3533, 34nfmpt 5124 . . . . . . . . . . . . . . 15 𝑦(𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
3635nfeq2 2916 . . . . . . . . . . . . . 14 𝑦 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
3732, 36nfan 1905 . . . . . . . . . . . . 13 𝑦(𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
3831, 37nfan 1905 . . . . . . . . . . . 12 𝑦(𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))))
39 nfv 1920 . . . . . . . . . . . 12 𝑦 𝑥𝑋
4038, 39nfan 1905 . . . . . . . . . . 11 𝑦((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥𝑋)
41 simplrr 778 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
4241fveq1d 6670 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑔𝑥) = ((𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥))
43 simprl 771 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑥𝑋)
44 toponmax 21670 . . . . . . . . . . . . . . . . . . 19 (𝐾 ∈ (TopOn‘𝑌) → 𝑌𝐾)
454, 44syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑌𝐾)
4645ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑌𝐾)
4746mptexd 6991 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑦𝑌 ↦ (𝑥𝑓𝑦)) ∈ V)
48 eqid 2738 . . . . . . . . . . . . . . . . 17 (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))) = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
4948fvmpt2 6780 . . . . . . . . . . . . . . . 16 ((𝑥𝑋 ∧ (𝑦𝑌 ↦ (𝑥𝑓𝑦)) ∈ V) → ((𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥) = (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
5043, 47, 49syl2anc 587 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥) = (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
5142, 50eqtrd 2773 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑔𝑥) = (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
5251fveq1d 6670 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑔𝑥)‘𝑦) = ((𝑦𝑌 ↦ (𝑥𝑓𝑦))‘𝑦))
53 simprr 773 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑦𝑌)
54 ovex 7197 . . . . . . . . . . . . . 14 (𝑥𝑓𝑦) ∈ V
55 eqid 2738 . . . . . . . . . . . . . . 15 (𝑦𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦𝑌 ↦ (𝑥𝑓𝑦))
5655fvmpt2 6780 . . . . . . . . . . . . . 14 ((𝑦𝑌 ∧ (𝑥𝑓𝑦) ∈ V) → ((𝑦𝑌 ↦ (𝑥𝑓𝑦))‘𝑦) = (𝑥𝑓𝑦))
5753, 54, 56sylancl 589 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑦𝑌 ↦ (𝑥𝑓𝑦))‘𝑦) = (𝑥𝑓𝑦))
5852, 57eqtrd 2773 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦))
5958expr 460 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥𝑋) → (𝑦𝑌 → ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦)))
6040, 59ralrimi 3127 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥𝑋) → ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦))
61 eqid 2738 . . . . . . . . . 10 𝑌 = 𝑌
6260, 61jctil 523 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥𝑋) → (𝑌 = 𝑌 ∧ ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦)))
6362ex 416 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥𝑋 → (𝑌 = 𝑌 ∧ ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦))))
6430, 63ralrimi 3127 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → ∀𝑥𝑋 (𝑌 = 𝑌 ∧ ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦)))
65 mpoeq123 7234 . . . . . . 7 ((𝑋 = 𝑋 ∧ ∀𝑥𝑋 (𝑌 = 𝑌 ∧ ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦))) → (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
6624, 64, 65sylancr 590 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
6723, 66eqtr4d 2776 . . . . 5 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
6822, 67jca 515 . . . 4 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
69 simprr 773 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
702adantr 484 . . . . . . . 8 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝐽 ∈ (TopOn‘𝑋))
714adantr 484 . . . . . . . 8 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝐾 ∈ (TopOn‘𝑌))
7211adantr 484 . . . . . . . 8 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝐿 ∈ (TopOn‘ 𝐿))
73 xkohmeo.k . . . . . . . . 9 (𝜑𝐾 ∈ 𝑛-Locally Comp)
7473adantr 484 . . . . . . . 8 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝐾 ∈ 𝑛-Locally Comp)
75 nllytop 22217 . . . . . . . . . . . . . 14 (𝐾 ∈ 𝑛-Locally Comp → 𝐾 ∈ Top)
7674, 75syl 17 . . . . . . . . . . . . 13 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝐾 ∈ Top)
779adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝐿 ∈ Top)
78 eqid 2738 . . . . . . . . . . . . . 14 (𝐿ko 𝐾) = (𝐿ko 𝐾)
7978xkotopon 22344 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐿ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)))
8076, 77, 79syl2anc 587 . . . . . . . . . . . 12 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → (𝐿ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)))
81 simpr 488 . . . . . . . . . . . 12 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)))
82 cnf2 21993 . . . . . . . . . . . 12 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐿ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)) ∧ 𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝑔:𝑋⟶(𝐾 Cn 𝐿))
8370, 80, 81, 82syl3anc 1372 . . . . . . . . . . 11 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝑔:𝑋⟶(𝐾 Cn 𝐿))
8483feqmptd 6731 . . . . . . . . . 10 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝑔 = (𝑥𝑋 ↦ (𝑔𝑥)))
854ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) ∧ 𝑥𝑋) → 𝐾 ∈ (TopOn‘𝑌))
8611ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) ∧ 𝑥𝑋) → 𝐿 ∈ (TopOn‘ 𝐿))
8783ffvelrnda 6855 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) ∧ 𝑥𝑋) → (𝑔𝑥) ∈ (𝐾 Cn 𝐿))
88 cnf2 21993 . . . . . . . . . . . . 13 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘ 𝐿) ∧ (𝑔𝑥) ∈ (𝐾 Cn 𝐿)) → (𝑔𝑥):𝑌 𝐿)
8985, 86, 87, 88syl3anc 1372 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) ∧ 𝑥𝑋) → (𝑔𝑥):𝑌 𝐿)
9089feqmptd 6731 . . . . . . . . . . 11 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) ∧ 𝑥𝑋) → (𝑔𝑥) = (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
9190mpteq2dva 5122 . . . . . . . . . 10 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → (𝑥𝑋 ↦ (𝑔𝑥)) = (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
9284, 91eqtrd 2773 . . . . . . . . 9 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
9392, 81eqeltrrd 2834 . . . . . . . 8 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))) ∈ (𝐽 Cn (𝐿ko 𝐾)))
9470, 71, 72, 74, 93cnmptk2 22430 . . . . . . 7 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
9594adantrr 717 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
9669, 95eqeltrd 2833 . . . . 5 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
9792adantrr 717 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
98 nfv 1920 . . . . . . . . 9 𝑥 𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))
99 nfmpo1 7242 . . . . . . . . . 10 𝑥(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
10099nfeq2 2916 . . . . . . . . 9 𝑥 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
10198, 100nfan 1905 . . . . . . . 8 𝑥(𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
10225, 101nfan 1905 . . . . . . 7 𝑥(𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
103 nfv 1920 . . . . . . . . . . . 12 𝑦 𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))
104 nfmpo2 7243 . . . . . . . . . . . . 13 𝑦(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
105104nfeq2 2916 . . . . . . . . . . . 12 𝑦 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
106103, 105nfan 1905 . . . . . . . . . . 11 𝑦(𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
10731, 106nfan 1905 . . . . . . . . . 10 𝑦(𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
108107, 39nfan 1905 . . . . . . . . 9 𝑦((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ 𝑥𝑋)
10969oveqd 7181 . . . . . . . . . . 11 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → (𝑥𝑓𝑦) = (𝑥(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))𝑦))
110 fvex 6681 . . . . . . . . . . . 12 ((𝑔𝑥)‘𝑦) ∈ V
111 eqid 2738 . . . . . . . . . . . . 13 (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
112111ovmpt4g 7306 . . . . . . . . . . . 12 ((𝑥𝑋𝑦𝑌 ∧ ((𝑔𝑥)‘𝑦) ∈ V) → (𝑥(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))𝑦) = ((𝑔𝑥)‘𝑦))
113110, 112mp3an3 1451 . . . . . . . . . . 11 ((𝑥𝑋𝑦𝑌) → (𝑥(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))𝑦) = ((𝑔𝑥)‘𝑦))
114109, 113sylan9eq 2793 . . . . . . . . . 10 (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑥𝑓𝑦) = ((𝑔𝑥)‘𝑦))
115114expr 460 . . . . . . . . 9 (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ 𝑥𝑋) → (𝑦𝑌 → (𝑥𝑓𝑦) = ((𝑔𝑥)‘𝑦)))
116108, 115ralrimi 3127 . . . . . . . 8 (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ 𝑥𝑋) → ∀𝑦𝑌 (𝑥𝑓𝑦) = ((𝑔𝑥)‘𝑦))
117 mpteq12 5114 . . . . . . . 8 ((𝑌 = 𝑌 ∧ ∀𝑦𝑌 (𝑥𝑓𝑦) = ((𝑔𝑥)‘𝑦)) → (𝑦𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
11861, 116, 117sylancr 590 . . . . . . 7 (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ 𝑥𝑋) → (𝑦𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
119102, 118mpteq2da 5121 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))) = (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
12097, 119eqtr4d 2776 . . . . 5 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
12196, 120jca 515 . . . 4 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))))
12268, 121impbida 801 . . 3 (𝜑 → ((𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))) ↔ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))))
123122opabbidv 5093 . 2 (𝜑 → {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))} = {⟨𝑔, 𝑓⟩ ∣ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))})
124 xkohmeo.f . . . . 5 𝐹 = (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
125 df-mpt 5108 . . . . 5 (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))) = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
126124, 125eqtri 2761 . . . 4 𝐹 = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
127126cnveqi 5711 . . 3 𝐹 = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
128 cnvopab 5965 . . 3 {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))} = {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
129127, 128eqtri 2761 . 2 𝐹 = {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
130 df-mpt 5108 . 2 (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ↦ (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))) = {⟨𝑔, 𝑓⟩ ∣ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))}
131123, 129, 1303eqtr4g 2798 1 (𝜑𝐹 = (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ↦ (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1542  wcel 2113  wral 3053  Vcvv 3397   cuni 4793  {copab 5089  cmpt 5107   × cxp 5517  ccnv 5518   Fn wfn 6328  wf 6329  cfv 6333  (class class class)co 7164  cmpo 7166  Topctop 21637  TopOnctopon 21654   Cn ccn 21968  Compccmp 22130  𝑛-Locally cnlly 22209   ×t ctx 22304  ko cxko 22305
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5151  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-pss 3860  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-tp 4518  df-op 4520  df-uni 4794  df-int 4834  df-iun 4880  df-iin 4881  df-br 5028  df-opab 5090  df-mpt 5108  df-tr 5134  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-ov 7167  df-oprab 7168  df-mpo 7169  df-om 7594  df-1st 7707  df-2nd 7708  df-1o 8124  df-er 8313  df-map 8432  df-ixp 8501  df-en 8549  df-dom 8550  df-fin 8552  df-fi 8941  df-rest 16792  df-topgen 16813  df-pt 16814  df-top 21638  df-topon 21655  df-bases 21690  df-ntr 21764  df-nei 21842  df-cn 21971  df-cnp 21972  df-cmp 22131  df-nlly 22211  df-tx 22306  df-xko 22307
This theorem is referenced by:  xkohmeo  22559
  Copyright terms: Public domain W3C validator