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

Theorem xkocnv 23838
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 480 . . . . . . . 8 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐽 ∈ (TopOn‘𝑋))
4 xkohmeo.y . . . . . . . . 9 (𝜑𝐾 ∈ (TopOn‘𝑌))
54adantr 480 . . . . . . . 8 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐾 ∈ (TopOn‘𝑌))
6 txtopon 23615 . . . . . . . . . . . . . 14 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
72, 4, 6syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
87adantr 480 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)))
9 xkohmeo.l . . . . . . . . . . . . . 14 (𝜑𝐿 ∈ Top)
10 toptopon2 22940 . . . . . . . . . . . . . 14 (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘ 𝐿))
119, 10sylib 218 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ (TopOn‘ 𝐿))
1211adantr 480 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝐿 ∈ (TopOn‘ 𝐿))
13 simpr 484 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
14 cnf2 23273 . . . . . . . . . . . 12 (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (TopOn‘ 𝐿) ∧ 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓:(𝑋 × 𝑌)⟶ 𝐿)
158, 12, 13, 14syl3anc 1370 . . . . . . . . . . 11 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓:(𝑋 × 𝑌)⟶ 𝐿)
1615ffnd 6738 . . . . . . . . . 10 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 Fn (𝑋 × 𝑌))
17 fnov 7564 . . . . . . . . . 10 (𝑓 Fn (𝑋 × 𝑌) ↔ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
1816, 17sylib 218 . . . . . . . . 9 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
1918, 13eqeltrrd 2840 . . . . . . . 8 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
203, 5, 19cnmpt2k 23712 . . . . . . 7 ((𝜑𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))) ∈ (𝐽 Cn (𝐿ko 𝐾)))
2120adantrr 717 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))) ∈ (𝐽 Cn (𝐿ko 𝐾)))
221, 21eqeltrd 2839 . . . . 5 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)))
2318adantrr 717 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
24 eqid 2735 . . . . . . 7 𝑋 = 𝑋
25 nfv 1912 . . . . . . . . 9 𝑥𝜑
26 nfv 1912 . . . . . . . . . 10 𝑥 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)
27 nfmpt1 5256 . . . . . . . . . . 11 𝑥(𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
2827nfeq2 2921 . . . . . . . . . 10 𝑥 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
2926, 28nfan 1897 . . . . . . . . 9 𝑥(𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
3025, 29nfan 1897 . . . . . . . 8 𝑥(𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))))
31 nfv 1912 . . . . . . . . . . . . 13 𝑦𝜑
32 nfv 1912 . . . . . . . . . . . . . 14 𝑦 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿)
33 nfcv 2903 . . . . . . . . . . . . . . . 16 𝑦𝑋
34 nfmpt1 5256 . . . . . . . . . . . . . . . 16 𝑦(𝑦𝑌 ↦ (𝑥𝑓𝑦))
3533, 34nfmpt 5255 . . . . . . . . . . . . . . 15 𝑦(𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
3635nfeq2 2921 . . . . . . . . . . . . . 14 𝑦 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
3732, 36nfan 1897 . . . . . . . . . . . . 13 𝑦(𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
3831, 37nfan 1897 . . . . . . . . . . . 12 𝑦(𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))))
39 nfv 1912 . . . . . . . . . . . 12 𝑦 𝑥𝑋
4038, 39nfan 1897 . . . . . . . . . . 11 𝑦((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥𝑋)
41 simplrr 778 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
4241fveq1d 6909 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑔𝑥) = ((𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥))
43 simprl 771 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑥𝑋)
44 toponmax 22948 . . . . . . . . . . . . . . . . . . 19 (𝐾 ∈ (TopOn‘𝑌) → 𝑌𝐾)
454, 44syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑌𝐾)
4645ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑌𝐾)
4746mptexd 7244 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑦𝑌 ↦ (𝑥𝑓𝑦)) ∈ V)
48 eqid 2735 . . . . . . . . . . . . . . . . 17 (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))) = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
4948fvmpt2 7027 . . . . . . . . . . . . . . . 16 ((𝑥𝑋 ∧ (𝑦𝑌 ↦ (𝑥𝑓𝑦)) ∈ V) → ((𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥) = (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
5043, 47, 49syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))‘𝑥) = (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
5142, 50eqtrd 2775 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑔𝑥) = (𝑦𝑌 ↦ (𝑥𝑓𝑦)))
5251fveq1d 6909 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑔𝑥)‘𝑦) = ((𝑦𝑌 ↦ (𝑥𝑓𝑦))‘𝑦))
53 simprr 773 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → 𝑦𝑌)
54 ovex 7464 . . . . . . . . . . . . . 14 (𝑥𝑓𝑦) ∈ V
55 eqid 2735 . . . . . . . . . . . . . . 15 (𝑦𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦𝑌 ↦ (𝑥𝑓𝑦))
5655fvmpt2 7027 . . . . . . . . . . . . . 14 ((𝑦𝑌 ∧ (𝑥𝑓𝑦) ∈ V) → ((𝑦𝑌 ↦ (𝑥𝑓𝑦))‘𝑦) = (𝑥𝑓𝑦))
5753, 54, 56sylancl 586 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑦𝑌 ↦ (𝑥𝑓𝑦))‘𝑦) = (𝑥𝑓𝑦))
5852, 57eqtrd 2775 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ (𝑥𝑋𝑦𝑌)) → ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦))
5958expr 456 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥𝑋) → (𝑦𝑌 → ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦)))
6040, 59ralrimi 3255 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥𝑋) → ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦))
61 eqid 2735 . . . . . . . . . 10 𝑌 = 𝑌
6260, 61jctil 519 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) ∧ 𝑥𝑋) → (𝑌 = 𝑌 ∧ ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦)))
6362ex 412 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥𝑋 → (𝑌 = 𝑌 ∧ ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦))))
6430, 63ralrimi 3255 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → ∀𝑥𝑋 (𝑌 = 𝑌 ∧ ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦)))
65 mpoeq123 7505 . . . . . . 7 ((𝑋 = 𝑋 ∧ ∀𝑥𝑋 (𝑌 = 𝑌 ∧ ∀𝑦𝑌 ((𝑔𝑥)‘𝑦) = (𝑥𝑓𝑦))) → (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
6624, 64, 65sylancr 587 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) = (𝑥𝑋, 𝑦𝑌 ↦ (𝑥𝑓𝑦)))
6723, 66eqtr4d 2778 . . . . 5 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
6822, 67jca 511 . . . 4 ((𝜑 ∧ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))) → (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
69 simprr 773 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
702adantr 480 . . . . . . . 8 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝐽 ∈ (TopOn‘𝑋))
714adantr 480 . . . . . . . 8 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝐾 ∈ (TopOn‘𝑌))
7211adantr 480 . . . . . . . 8 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝐿 ∈ (TopOn‘ 𝐿))
73 xkohmeo.k . . . . . . . . 9 (𝜑𝐾 ∈ 𝑛-Locally Comp)
7473adantr 480 . . . . . . . 8 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝐾 ∈ 𝑛-Locally Comp)
75 nllytop 23497 . . . . . . . . . . . . . 14 (𝐾 ∈ 𝑛-Locally Comp → 𝐾 ∈ Top)
7674, 75syl 17 . . . . . . . . . . . . 13 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝐾 ∈ Top)
779adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝐿 ∈ Top)
78 eqid 2735 . . . . . . . . . . . . . 14 (𝐿ko 𝐾) = (𝐿ko 𝐾)
7978xkotopon 23624 . . . . . . . . . . . . 13 ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐿ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)))
8076, 77, 79syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → (𝐿ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)))
81 simpr 484 . . . . . . . . . . . 12 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)))
82 cnf2 23273 . . . . . . . . . . . 12 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐿ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)) ∧ 𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝑔:𝑋⟶(𝐾 Cn 𝐿))
8370, 80, 81, 82syl3anc 1370 . . . . . . . . . . 11 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝑔:𝑋⟶(𝐾 Cn 𝐿))
8483feqmptd 6977 . . . . . . . . . 10 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝑔 = (𝑥𝑋 ↦ (𝑔𝑥)))
854ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) ∧ 𝑥𝑋) → 𝐾 ∈ (TopOn‘𝑌))
8611ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) ∧ 𝑥𝑋) → 𝐿 ∈ (TopOn‘ 𝐿))
8783ffvelcdmda 7104 . . . . . . . . . . . . 13 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) ∧ 𝑥𝑋) → (𝑔𝑥) ∈ (𝐾 Cn 𝐿))
88 cnf2 23273 . . . . . . . . . . . . 13 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘ 𝐿) ∧ (𝑔𝑥) ∈ (𝐾 Cn 𝐿)) → (𝑔𝑥):𝑌 𝐿)
8985, 86, 87, 88syl3anc 1370 . . . . . . . . . . . 12 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) ∧ 𝑥𝑋) → (𝑔𝑥):𝑌 𝐿)
9089feqmptd 6977 . . . . . . . . . . 11 (((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) ∧ 𝑥𝑋) → (𝑔𝑥) = (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
9190mpteq2dva 5248 . . . . . . . . . 10 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → (𝑥𝑋 ↦ (𝑔𝑥)) = (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
9284, 91eqtrd 2775 . . . . . . . . 9 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
9392, 81eqeltrrd 2840 . . . . . . . 8 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))) ∈ (𝐽 Cn (𝐿ko 𝐾)))
9470, 71, 72, 74, 93cnmptk2 23710 . . . . . . 7 ((𝜑𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))) → (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
9594adantrr 717 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
9669, 95eqeltrd 2839 . . . . 5 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → 𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿))
9792adantrr 717 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
98 nfv 1912 . . . . . . . . 9 𝑥 𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))
99 nfmpo1 7513 . . . . . . . . . 10 𝑥(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
10099nfeq2 2921 . . . . . . . . 9 𝑥 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
10198, 100nfan 1897 . . . . . . . 8 𝑥(𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
10225, 101nfan 1897 . . . . . . 7 𝑥(𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
103 nfv 1912 . . . . . . . . . . . 12 𝑦 𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾))
104 nfmpo2 7514 . . . . . . . . . . . . 13 𝑦(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
105104nfeq2 2921 . . . . . . . . . . . 12 𝑦 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
106103, 105nfan 1897 . . . . . . . . . . 11 𝑦(𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
10731, 106nfan 1897 . . . . . . . . . 10 𝑦(𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
108107, 39nfan 1897 . . . . . . . . 9 𝑦((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ 𝑥𝑋)
10969oveqd 7448 . . . . . . . . . . 11 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → (𝑥𝑓𝑦) = (𝑥(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))𝑦))
110 fvex 6920 . . . . . . . . . . . 12 ((𝑔𝑥)‘𝑦) ∈ V
111 eqid 2735 . . . . . . . . . . . . 13 (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)) = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))
112111ovmpt4g 7580 . . . . . . . . . . . 12 ((𝑥𝑋𝑦𝑌 ∧ ((𝑔𝑥)‘𝑦) ∈ V) → (𝑥(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))𝑦) = ((𝑔𝑥)‘𝑦))
113110, 112mp3an3 1449 . . . . . . . . . . 11 ((𝑥𝑋𝑦𝑌) → (𝑥(𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))𝑦) = ((𝑔𝑥)‘𝑦))
114109, 113sylan9eq 2795 . . . . . . . . . 10 (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ (𝑥𝑋𝑦𝑌)) → (𝑥𝑓𝑦) = ((𝑔𝑥)‘𝑦))
115114expr 456 . . . . . . . . 9 (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ 𝑥𝑋) → (𝑦𝑌 → (𝑥𝑓𝑦) = ((𝑔𝑥)‘𝑦)))
116108, 115ralrimi 3255 . . . . . . . 8 (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ 𝑥𝑋) → ∀𝑦𝑌 (𝑥𝑓𝑦) = ((𝑔𝑥)‘𝑦))
117 mpteq12 5240 . . . . . . . 8 ((𝑌 = 𝑌 ∧ ∀𝑦𝑌 (𝑥𝑓𝑦) = ((𝑔𝑥)‘𝑦)) → (𝑦𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
11861, 116, 117sylancr 587 . . . . . . 7 (((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) ∧ 𝑥𝑋) → (𝑦𝑌 ↦ (𝑥𝑓𝑦)) = (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))
119102, 118mpteq2da 5246 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))) = (𝑥𝑋 ↦ (𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
12097, 119eqtr4d 2778 . . . . 5 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
12196, 120jca 511 . . . 4 ((𝜑 ∧ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))) → (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))))
12268, 121impbida 801 . . 3 (𝜑 → ((𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))) ↔ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))))
123122opabbidv 5214 . 2 (𝜑 → {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))} = {⟨𝑔, 𝑓⟩ ∣ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))})
124 xkohmeo.f . . . . 5 𝐹 = (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))
125 df-mpt 5232 . . . . 5 (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦)))) = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
126124, 125eqtri 2763 . . . 4 𝐹 = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
127126cnveqi 5888 . . 3 𝐹 = {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
128 cnvopab 6160 . . 3 {⟨𝑓, 𝑔⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))} = {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
129127, 128eqtri 2763 . 2 𝐹 = {⟨𝑔, 𝑓⟩ ∣ (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ 𝑔 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ (𝑥𝑓𝑦))))}
130 df-mpt 5232 . 2 (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ↦ (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))) = {⟨𝑔, 𝑓⟩ ∣ (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ∧ 𝑓 = (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦)))}
131123, 129, 1303eqtr4g 2800 1 (𝜑𝐹 = (𝑔 ∈ (𝐽 Cn (𝐿ko 𝐾)) ↦ (𝑥𝑋, 𝑦𝑌 ↦ ((𝑔𝑥)‘𝑦))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1537  wcel 2106  wral 3059  Vcvv 3478   cuni 4912  {copab 5210  cmpt 5231   × cxp 5687  ccnv 5688   Fn wfn 6558  wf 6559  cfv 6563  (class class class)co 7431  cmpo 7433  Topctop 22915  TopOnctopon 22932   Cn ccn 23248  Compccmp 23410  𝑛-Locally cnlly 23489   ×t ctx 23584  ko cxko 23585
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-1o 8505  df-2o 8506  df-map 8867  df-ixp 8937  df-en 8985  df-dom 8986  df-fin 8988  df-fi 9449  df-rest 17469  df-topgen 17490  df-pt 17491  df-top 22916  df-topon 22933  df-bases 22969  df-ntr 23044  df-nei 23122  df-cn 23251  df-cnp 23252  df-cmp 23411  df-nlly 23491  df-tx 23586  df-xko 23587
This theorem is referenced by:  xkohmeo  23839
  Copyright terms: Public domain W3C validator