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

Theorem xkoinjcn 21484
Description: Continuity of "injection", i.e. currying, as a function on continuous function spaces. (Contributed by Mario Carneiro, 23-Mar-2015.)
Hypothesis
Ref Expression
xkoinjcn.3 𝐹 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩))
Assertion
Ref Expression
xkoinjcn ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → 𝐹 ∈ (𝑅 Cn ((𝑆 ×t 𝑅) ^ko 𝑆)))
Distinct variable groups:   𝑥,𝑦,𝑅   𝑥,𝑆,𝑦   𝑥,𝑌,𝑦   𝑥,𝑋,𝑦
Allowed substitution hints:   𝐹(𝑥,𝑦)

Proof of Theorem xkoinjcn
Dummy variables 𝑓 𝑘 𝑟 𝑣 𝑤 𝑧 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simplr 792 . . . 4 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑥𝑋) → 𝑆 ∈ (TopOn‘𝑌))
21cnmptid 21458 . . . 4 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑥𝑋) → (𝑦𝑌𝑦) ∈ (𝑆 Cn 𝑆))
3 simpll 790 . . . . 5 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑥𝑋) → 𝑅 ∈ (TopOn‘𝑋))
4 simpr 477 . . . . 5 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑥𝑋) → 𝑥𝑋)
51, 3, 4cnmptc 21459 . . . 4 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑥𝑋) → (𝑦𝑌𝑥) ∈ (𝑆 Cn 𝑅))
61, 2, 5cnmpt1t 21462 . . 3 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑥𝑋) → (𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) ∈ (𝑆 Cn (𝑆 ×t 𝑅)))
7 xkoinjcn.3 . . 3 𝐹 = (𝑥𝑋 ↦ (𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩))
86, 7fmptd 6383 . 2 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → 𝐹:𝑋⟶(𝑆 Cn (𝑆 ×t 𝑅)))
9 eqid 2621 . . . . . 6 𝑆 = 𝑆
10 eqid 2621 . . . . . 6 {𝑤 ∈ 𝒫 𝑆 ∣ (𝑆t 𝑤) ∈ Comp} = {𝑤 ∈ 𝒫 𝑆 ∣ (𝑆t 𝑤) ∈ Comp}
11 eqid 2621 . . . . . 6 (𝑘 ∈ {𝑤 ∈ 𝒫 𝑆 ∣ (𝑆t 𝑤) ∈ Comp}, 𝑣 ∈ (𝑆 ×t 𝑅) ↦ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣}) = (𝑘 ∈ {𝑤 ∈ 𝒫 𝑆 ∣ (𝑆t 𝑤) ∈ Comp}, 𝑣 ∈ (𝑆 ×t 𝑅) ↦ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣})
129, 10, 11xkobval 21383 . . . . 5 ran (𝑘 ∈ {𝑤 ∈ 𝒫 𝑆 ∣ (𝑆t 𝑤) ∈ Comp}, 𝑣 ∈ (𝑆 ×t 𝑅) ↦ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣}) = {𝑧 ∣ ∃𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅)((𝑆t 𝑘) ∈ Comp ∧ 𝑧 = {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣})}
1312abeq2i 2734 . . . 4 (𝑧 ∈ ran (𝑘 ∈ {𝑤 ∈ 𝒫 𝑆 ∣ (𝑆t 𝑤) ∈ Comp}, 𝑣 ∈ (𝑆 ×t 𝑅) ↦ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣}) ↔ ∃𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅)((𝑆t 𝑘) ∈ Comp ∧ 𝑧 = {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣}))
14 simpll 790 . . . . . . . . . . . 12 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) → (𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)))
1514, 6sylan 488 . . . . . . . . . . 11 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ 𝑥𝑋) → (𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) ∈ (𝑆 Cn (𝑆 ×t 𝑅)))
16 imaeq1 5459 . . . . . . . . . . . . 13 (𝑓 = (𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) → (𝑓𝑘) = ((𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) “ 𝑘))
1716sseq1d 3630 . . . . . . . . . . . 12 (𝑓 = (𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) → ((𝑓𝑘) ⊆ 𝑣 ↔ ((𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) “ 𝑘) ⊆ 𝑣))
1817elrab3 3362 . . . . . . . . . . 11 ((𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) ∈ (𝑆 Cn (𝑆 ×t 𝑅)) → ((𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) ∈ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣} ↔ ((𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) “ 𝑘) ⊆ 𝑣))
1915, 18syl 17 . . . . . . . . . 10 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ 𝑥𝑋) → ((𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) ∈ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣} ↔ ((𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) “ 𝑘) ⊆ 𝑣))
20 funmpt 5924 . . . . . . . . . . 11 Fun (𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩)
21 simplrl 800 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) → 𝑘 ∈ 𝒫 𝑆)
2221elpwid 4168 . . . . . . . . . . . . . 14 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) → 𝑘 𝑆)
2314simprd 479 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) → 𝑆 ∈ (TopOn‘𝑌))
24 toponuni 20713 . . . . . . . . . . . . . . 15 (𝑆 ∈ (TopOn‘𝑌) → 𝑌 = 𝑆)
2523, 24syl 17 . . . . . . . . . . . . . 14 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) → 𝑌 = 𝑆)
2622, 25sseqtr4d 3640 . . . . . . . . . . . . 13 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) → 𝑘𝑌)
2726adantr 481 . . . . . . . . . . . 12 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ 𝑥𝑋) → 𝑘𝑌)
28 dmmptg 5630 . . . . . . . . . . . . 13 (∀𝑦𝑌𝑦, 𝑥⟩ ∈ V → dom (𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) = 𝑌)
29 opex 4930 . . . . . . . . . . . . . 14 𝑦, 𝑥⟩ ∈ V
3029a1i 11 . . . . . . . . . . . . 13 (𝑦𝑌 → ⟨𝑦, 𝑥⟩ ∈ V)
3128, 30mprg 2925 . . . . . . . . . . . 12 dom (𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) = 𝑌
3227, 31syl6sseqr 3650 . . . . . . . . . . 11 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ 𝑥𝑋) → 𝑘 ⊆ dom (𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩))
33 funimass4 6245 . . . . . . . . . . 11 ((Fun (𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) ∧ 𝑘 ⊆ dom (𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩)) → (((𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) “ 𝑘) ⊆ 𝑣 ↔ ∀𝑧𝑘 ((𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩)‘𝑧) ∈ 𝑣))
3420, 32, 33sylancr 695 . . . . . . . . . 10 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ 𝑥𝑋) → (((𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) “ 𝑘) ⊆ 𝑣 ↔ ∀𝑧𝑘 ((𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩)‘𝑧) ∈ 𝑣))
3527sselda 3601 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ 𝑥𝑋) ∧ 𝑧𝑘) → 𝑧𝑌)
36 opeq1 4400 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑧 → ⟨𝑦, 𝑥⟩ = ⟨𝑧, 𝑥⟩)
37 eqid 2621 . . . . . . . . . . . . . . . 16 (𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) = (𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩)
38 opex 4930 . . . . . . . . . . . . . . . 16 𝑧, 𝑥⟩ ∈ V
3936, 37, 38fvmpt 6280 . . . . . . . . . . . . . . 15 (𝑧𝑌 → ((𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩)‘𝑧) = ⟨𝑧, 𝑥⟩)
4035, 39syl 17 . . . . . . . . . . . . . 14 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ 𝑥𝑋) ∧ 𝑧𝑘) → ((𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩)‘𝑧) = ⟨𝑧, 𝑥⟩)
4140eleq1d 2685 . . . . . . . . . . . . 13 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ 𝑥𝑋) ∧ 𝑧𝑘) → (((𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩)‘𝑧) ∈ 𝑣 ↔ ⟨𝑧, 𝑥⟩ ∈ 𝑣))
42 vex 3201 . . . . . . . . . . . . . 14 𝑥 ∈ V
43 opeq2 4401 . . . . . . . . . . . . . . 15 (𝑤 = 𝑥 → ⟨𝑧, 𝑤⟩ = ⟨𝑧, 𝑥⟩)
4443eleq1d 2685 . . . . . . . . . . . . . 14 (𝑤 = 𝑥 → (⟨𝑧, 𝑤⟩ ∈ 𝑣 ↔ ⟨𝑧, 𝑥⟩ ∈ 𝑣))
4542, 44ralsn 4220 . . . . . . . . . . . . 13 (∀𝑤 ∈ {𝑥}⟨𝑧, 𝑤⟩ ∈ 𝑣 ↔ ⟨𝑧, 𝑥⟩ ∈ 𝑣)
4641, 45syl6bbr 278 . . . . . . . . . . . 12 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ 𝑥𝑋) ∧ 𝑧𝑘) → (((𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩)‘𝑧) ∈ 𝑣 ↔ ∀𝑤 ∈ {𝑥}⟨𝑧, 𝑤⟩ ∈ 𝑣))
4746ralbidva 2984 . . . . . . . . . . 11 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ 𝑥𝑋) → (∀𝑧𝑘 ((𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩)‘𝑧) ∈ 𝑣 ↔ ∀𝑧𝑘𝑤 ∈ {𝑥}⟨𝑧, 𝑤⟩ ∈ 𝑣))
48 dfss3 3590 . . . . . . . . . . . 12 ((𝑘 × {𝑥}) ⊆ 𝑣 ↔ ∀𝑡 ∈ (𝑘 × {𝑥})𝑡𝑣)
49 eleq1 2688 . . . . . . . . . . . . 13 (𝑡 = ⟨𝑧, 𝑤⟩ → (𝑡𝑣 ↔ ⟨𝑧, 𝑤⟩ ∈ 𝑣))
5049ralxp 5261 . . . . . . . . . . . 12 (∀𝑡 ∈ (𝑘 × {𝑥})𝑡𝑣 ↔ ∀𝑧𝑘𝑤 ∈ {𝑥}⟨𝑧, 𝑤⟩ ∈ 𝑣)
5148, 50bitri 264 . . . . . . . . . . 11 ((𝑘 × {𝑥}) ⊆ 𝑣 ↔ ∀𝑧𝑘𝑤 ∈ {𝑥}⟨𝑧, 𝑤⟩ ∈ 𝑣)
5247, 51syl6bbr 278 . . . . . . . . . 10 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ 𝑥𝑋) → (∀𝑧𝑘 ((𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩)‘𝑧) ∈ 𝑣 ↔ (𝑘 × {𝑥}) ⊆ 𝑣))
5319, 34, 523bitrd 294 . . . . . . . . 9 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ 𝑥𝑋) → ((𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) ∈ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣} ↔ (𝑘 × {𝑥}) ⊆ 𝑣))
5453rabbidva 3186 . . . . . . . 8 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) → {𝑥𝑋 ∣ (𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) ∈ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣}} = {𝑥𝑋 ∣ (𝑘 × {𝑥}) ⊆ 𝑣})
55 sneq 4185 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → {𝑥} = {𝑤})
5655xpeq2d 5137 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝑘 × {𝑥}) = (𝑘 × {𝑤}))
5756sseq1d 3630 . . . . . . . . . . . 12 (𝑥 = 𝑤 → ((𝑘 × {𝑥}) ⊆ 𝑣 ↔ (𝑘 × {𝑤}) ⊆ 𝑣))
5857elrab 3361 . . . . . . . . . . 11 (𝑤 ∈ {𝑥𝑋 ∣ (𝑘 × {𝑥}) ⊆ 𝑣} ↔ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣))
59 eqid 2621 . . . . . . . . . . . . 13 (𝑆t 𝑘) = (𝑆t 𝑘)
60 eqid 2621 . . . . . . . . . . . . 13 𝑅 = 𝑅
61 simplr 792 . . . . . . . . . . . . 13 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → (𝑆t 𝑘) ∈ Comp)
62 simpll 790 . . . . . . . . . . . . . . 15 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) → 𝑅 ∈ (TopOn‘𝑋))
6362ad2antrr 762 . . . . . . . . . . . . . 14 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → 𝑅 ∈ (TopOn‘𝑋))
64 topontop 20712 . . . . . . . . . . . . . 14 (𝑅 ∈ (TopOn‘𝑋) → 𝑅 ∈ Top)
6563, 64syl 17 . . . . . . . . . . . . 13 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → 𝑅 ∈ Top)
66 topontop 20712 . . . . . . . . . . . . . . . . . 18 (𝑆 ∈ (TopOn‘𝑌) → 𝑆 ∈ Top)
6766adantl 482 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → 𝑆 ∈ Top)
6864adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → 𝑅 ∈ Top)
69 txtop 21366 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ Top ∧ 𝑅 ∈ Top) → (𝑆 ×t 𝑅) ∈ Top)
7067, 68, 69syl2anc 693 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑆 ×t 𝑅) ∈ Top)
7170ad3antrrr 766 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → (𝑆 ×t 𝑅) ∈ Top)
72 vex 3201 . . . . . . . . . . . . . . . 16 𝑘 ∈ V
73 toponmax 20724 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ (TopOn‘𝑋) → 𝑋𝑅)
7463, 73syl 17 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → 𝑋𝑅)
75 xpexg 6957 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ V ∧ 𝑋𝑅) → (𝑘 × 𝑋) ∈ V)
7672, 74, 75sylancr 695 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → (𝑘 × 𝑋) ∈ V)
77 simprr 796 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) → 𝑣 ∈ (𝑆 ×t 𝑅))
7877ad2antrr 762 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → 𝑣 ∈ (𝑆 ×t 𝑅))
79 elrestr 16083 . . . . . . . . . . . . . . 15 (((𝑆 ×t 𝑅) ∈ Top ∧ (𝑘 × 𝑋) ∈ V ∧ 𝑣 ∈ (𝑆 ×t 𝑅)) → (𝑣 ∩ (𝑘 × 𝑋)) ∈ ((𝑆 ×t 𝑅) ↾t (𝑘 × 𝑋)))
8071, 76, 78, 79syl3anc 1325 . . . . . . . . . . . . . 14 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → (𝑣 ∩ (𝑘 × 𝑋)) ∈ ((𝑆 ×t 𝑅) ↾t (𝑘 × 𝑋)))
8167ad3antrrr 766 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → 𝑆 ∈ Top)
8272a1i 11 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → 𝑘 ∈ V)
83 txrest 21428 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ Top ∧ 𝑅 ∈ Top) ∧ (𝑘 ∈ V ∧ 𝑋𝑅)) → ((𝑆 ×t 𝑅) ↾t (𝑘 × 𝑋)) = ((𝑆t 𝑘) ×t (𝑅t 𝑋)))
8481, 65, 82, 74, 83syl22anc 1326 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → ((𝑆 ×t 𝑅) ↾t (𝑘 × 𝑋)) = ((𝑆t 𝑘) ×t (𝑅t 𝑋)))
85 toponuni 20713 . . . . . . . . . . . . . . . . . . 19 (𝑅 ∈ (TopOn‘𝑋) → 𝑋 = 𝑅)
8663, 85syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → 𝑋 = 𝑅)
8786oveq2d 6663 . . . . . . . . . . . . . . . . 17 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → (𝑅t 𝑋) = (𝑅t 𝑅))
8860restid 16088 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ (TopOn‘𝑋) → (𝑅t 𝑅) = 𝑅)
8963, 88syl 17 . . . . . . . . . . . . . . . . 17 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → (𝑅t 𝑅) = 𝑅)
9087, 89eqtrd 2655 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → (𝑅t 𝑋) = 𝑅)
9190oveq2d 6663 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → ((𝑆t 𝑘) ×t (𝑅t 𝑋)) = ((𝑆t 𝑘) ×t 𝑅))
9284, 91eqtrd 2655 . . . . . . . . . . . . . 14 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → ((𝑆 ×t 𝑅) ↾t (𝑘 × 𝑋)) = ((𝑆t 𝑘) ×t 𝑅))
9380, 92eleqtrd 2702 . . . . . . . . . . . . 13 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → (𝑣 ∩ (𝑘 × 𝑋)) ∈ ((𝑆t 𝑘) ×t 𝑅))
9423adantr 481 . . . . . . . . . . . . . . . . 17 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → 𝑆 ∈ (TopOn‘𝑌))
9526adantr 481 . . . . . . . . . . . . . . . . 17 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → 𝑘𝑌)
96 resttopon 20959 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ (TopOn‘𝑌) ∧ 𝑘𝑌) → (𝑆t 𝑘) ∈ (TopOn‘𝑘))
9794, 95, 96syl2anc 693 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → (𝑆t 𝑘) ∈ (TopOn‘𝑘))
98 toponuni 20713 . . . . . . . . . . . . . . . 16 ((𝑆t 𝑘) ∈ (TopOn‘𝑘) → 𝑘 = (𝑆t 𝑘))
9997, 98syl 17 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → 𝑘 = (𝑆t 𝑘))
10099xpeq1d 5136 . . . . . . . . . . . . . 14 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → (𝑘 × {𝑤}) = ( (𝑆t 𝑘) × {𝑤}))
101 simprr 796 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → (𝑘 × {𝑤}) ⊆ 𝑣)
102 simprl 794 . . . . . . . . . . . . . . . . 17 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → 𝑤𝑋)
103102snssd 4338 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → {𝑤} ⊆ 𝑋)
104 xpss2 5227 . . . . . . . . . . . . . . . 16 ({𝑤} ⊆ 𝑋 → (𝑘 × {𝑤}) ⊆ (𝑘 × 𝑋))
105103, 104syl 17 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → (𝑘 × {𝑤}) ⊆ (𝑘 × 𝑋))
106101, 105ssind 3835 . . . . . . . . . . . . . 14 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → (𝑘 × {𝑤}) ⊆ (𝑣 ∩ (𝑘 × 𝑋)))
107100, 106eqsstr3d 3638 . . . . . . . . . . . . 13 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → ( (𝑆t 𝑘) × {𝑤}) ⊆ (𝑣 ∩ (𝑘 × 𝑋)))
108102, 86eleqtrd 2702 . . . . . . . . . . . . 13 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → 𝑤 𝑅)
10959, 60, 61, 65, 93, 107, 108txtube 21437 . . . . . . . . . . . 12 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → ∃𝑟𝑅 (𝑤𝑟 ∧ ( (𝑆t 𝑘) × 𝑟) ⊆ (𝑣 ∩ (𝑘 × 𝑋))))
110 toponss 20725 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑟𝑅) → 𝑟𝑋)
11163, 110sylan 488 . . . . . . . . . . . . . . . 16 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) ∧ 𝑟𝑅) → 𝑟𝑋)
112 ssrab 3678 . . . . . . . . . . . . . . . . 17 (𝑟 ⊆ {𝑥𝑋 ∣ (𝑘 × {𝑥}) ⊆ 𝑣} ↔ (𝑟𝑋 ∧ ∀𝑥𝑟 (𝑘 × {𝑥}) ⊆ 𝑣))
113112baib 944 . . . . . . . . . . . . . . . 16 (𝑟𝑋 → (𝑟 ⊆ {𝑥𝑋 ∣ (𝑘 × {𝑥}) ⊆ 𝑣} ↔ ∀𝑥𝑟 (𝑘 × {𝑥}) ⊆ 𝑣))
114111, 113syl 17 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) ∧ 𝑟𝑅) → (𝑟 ⊆ {𝑥𝑋 ∣ (𝑘 × {𝑥}) ⊆ 𝑣} ↔ ∀𝑥𝑟 (𝑘 × {𝑥}) ⊆ 𝑣))
115 xpss2 5227 . . . . . . . . . . . . . . . . . 18 (𝑟𝑋 → (𝑘 × 𝑟) ⊆ (𝑘 × 𝑋))
116111, 115syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) ∧ 𝑟𝑅) → (𝑘 × 𝑟) ⊆ (𝑘 × 𝑋))
117116biantrud 528 . . . . . . . . . . . . . . . 16 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) ∧ 𝑟𝑅) → ((𝑘 × 𝑟) ⊆ 𝑣 ↔ ((𝑘 × 𝑟) ⊆ 𝑣 ∧ (𝑘 × 𝑟) ⊆ (𝑘 × 𝑋))))
118 iunid 4573 . . . . . . . . . . . . . . . . . . . 20 𝑥𝑟 {𝑥} = 𝑟
119118xpeq2i 5134 . . . . . . . . . . . . . . . . . . 19 (𝑘 × 𝑥𝑟 {𝑥}) = (𝑘 × 𝑟)
120 xpiundi 5171 . . . . . . . . . . . . . . . . . . 19 (𝑘 × 𝑥𝑟 {𝑥}) = 𝑥𝑟 (𝑘 × {𝑥})
121119, 120eqtr3i 2645 . . . . . . . . . . . . . . . . . 18 (𝑘 × 𝑟) = 𝑥𝑟 (𝑘 × {𝑥})
122121sseq1i 3627 . . . . . . . . . . . . . . . . 17 ((𝑘 × 𝑟) ⊆ 𝑣 𝑥𝑟 (𝑘 × {𝑥}) ⊆ 𝑣)
123 iunss 4559 . . . . . . . . . . . . . . . . 17 ( 𝑥𝑟 (𝑘 × {𝑥}) ⊆ 𝑣 ↔ ∀𝑥𝑟 (𝑘 × {𝑥}) ⊆ 𝑣)
124122, 123bitri 264 . . . . . . . . . . . . . . . 16 ((𝑘 × 𝑟) ⊆ 𝑣 ↔ ∀𝑥𝑟 (𝑘 × {𝑥}) ⊆ 𝑣)
125 ssin 3833 . . . . . . . . . . . . . . . 16 (((𝑘 × 𝑟) ⊆ 𝑣 ∧ (𝑘 × 𝑟) ⊆ (𝑘 × 𝑋)) ↔ (𝑘 × 𝑟) ⊆ (𝑣 ∩ (𝑘 × 𝑋)))
126117, 124, 1253bitr3g 302 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) ∧ 𝑟𝑅) → (∀𝑥𝑟 (𝑘 × {𝑥}) ⊆ 𝑣 ↔ (𝑘 × 𝑟) ⊆ (𝑣 ∩ (𝑘 × 𝑋))))
12799adantr 481 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) ∧ 𝑟𝑅) → 𝑘 = (𝑆t 𝑘))
128127xpeq1d 5136 . . . . . . . . . . . . . . . 16 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) ∧ 𝑟𝑅) → (𝑘 × 𝑟) = ( (𝑆t 𝑘) × 𝑟))
129128sseq1d 3630 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) ∧ 𝑟𝑅) → ((𝑘 × 𝑟) ⊆ (𝑣 ∩ (𝑘 × 𝑋)) ↔ ( (𝑆t 𝑘) × 𝑟) ⊆ (𝑣 ∩ (𝑘 × 𝑋))))
130114, 126, 1293bitrd 294 . . . . . . . . . . . . . 14 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) ∧ 𝑟𝑅) → (𝑟 ⊆ {𝑥𝑋 ∣ (𝑘 × {𝑥}) ⊆ 𝑣} ↔ ( (𝑆t 𝑘) × 𝑟) ⊆ (𝑣 ∩ (𝑘 × 𝑋))))
131130anbi2d 740 . . . . . . . . . . . . 13 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) ∧ 𝑟𝑅) → ((𝑤𝑟𝑟 ⊆ {𝑥𝑋 ∣ (𝑘 × {𝑥}) ⊆ 𝑣}) ↔ (𝑤𝑟 ∧ ( (𝑆t 𝑘) × 𝑟) ⊆ (𝑣 ∩ (𝑘 × 𝑋)))))
132131rexbidva 3047 . . . . . . . . . . . 12 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → (∃𝑟𝑅 (𝑤𝑟𝑟 ⊆ {𝑥𝑋 ∣ (𝑘 × {𝑥}) ⊆ 𝑣}) ↔ ∃𝑟𝑅 (𝑤𝑟 ∧ ( (𝑆t 𝑘) × 𝑟) ⊆ (𝑣 ∩ (𝑘 × 𝑋)))))
133109, 132mpbird 247 . . . . . . . . . . 11 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ (𝑤𝑋 ∧ (𝑘 × {𝑤}) ⊆ 𝑣)) → ∃𝑟𝑅 (𝑤𝑟𝑟 ⊆ {𝑥𝑋 ∣ (𝑘 × {𝑥}) ⊆ 𝑣}))
13458, 133sylan2b 492 . . . . . . . . . 10 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) ∧ 𝑤 ∈ {𝑥𝑋 ∣ (𝑘 × {𝑥}) ⊆ 𝑣}) → ∃𝑟𝑅 (𝑤𝑟𝑟 ⊆ {𝑥𝑋 ∣ (𝑘 × {𝑥}) ⊆ 𝑣}))
135134ralrimiva 2965 . . . . . . . . 9 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) → ∀𝑤 ∈ {𝑥𝑋 ∣ (𝑘 × {𝑥}) ⊆ 𝑣}∃𝑟𝑅 (𝑤𝑟𝑟 ⊆ {𝑥𝑋 ∣ (𝑘 × {𝑥}) ⊆ 𝑣}))
136 eltop2 20773 . . . . . . . . . 10 (𝑅 ∈ Top → ({𝑥𝑋 ∣ (𝑘 × {𝑥}) ⊆ 𝑣} ∈ 𝑅 ↔ ∀𝑤 ∈ {𝑥𝑋 ∣ (𝑘 × {𝑥}) ⊆ 𝑣}∃𝑟𝑅 (𝑤𝑟𝑟 ⊆ {𝑥𝑋 ∣ (𝑘 × {𝑥}) ⊆ 𝑣})))
13714, 68, 1363syl 18 . . . . . . . . 9 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) → ({𝑥𝑋 ∣ (𝑘 × {𝑥}) ⊆ 𝑣} ∈ 𝑅 ↔ ∀𝑤 ∈ {𝑥𝑋 ∣ (𝑘 × {𝑥}) ⊆ 𝑣}∃𝑟𝑅 (𝑤𝑟𝑟 ⊆ {𝑥𝑋 ∣ (𝑘 × {𝑥}) ⊆ 𝑣})))
138135, 137mpbird 247 . . . . . . . 8 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) → {𝑥𝑋 ∣ (𝑘 × {𝑥}) ⊆ 𝑣} ∈ 𝑅)
13954, 138eqeltrd 2700 . . . . . . 7 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) → {𝑥𝑋 ∣ (𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) ∈ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣}} ∈ 𝑅)
140 imaeq2 5460 . . . . . . . . 9 (𝑧 = {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣} → (𝐹𝑧) = (𝐹 “ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣}))
1417mptpreima 5626 . . . . . . . . 9 (𝐹 “ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣}) = {𝑥𝑋 ∣ (𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) ∈ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣}}
142140, 141syl6eq 2671 . . . . . . . 8 (𝑧 = {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣} → (𝐹𝑧) = {𝑥𝑋 ∣ (𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) ∈ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣}})
143142eleq1d 2685 . . . . . . 7 (𝑧 = {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣} → ((𝐹𝑧) ∈ 𝑅 ↔ {𝑥𝑋 ∣ (𝑦𝑌 ↦ ⟨𝑦, 𝑥⟩) ∈ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣}} ∈ 𝑅))
144139, 143syl5ibrcom 237 . . . . . 6 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) ∧ (𝑆t 𝑘) ∈ Comp) → (𝑧 = {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣} → (𝐹𝑧) ∈ 𝑅))
145144expimpd 629 . . . . 5 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅))) → (((𝑆t 𝑘) ∈ Comp ∧ 𝑧 = {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣}) → (𝐹𝑧) ∈ 𝑅))
146145rexlimdvva 3036 . . . 4 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (∃𝑘 ∈ 𝒫 𝑆𝑣 ∈ (𝑆 ×t 𝑅)((𝑆t 𝑘) ∈ Comp ∧ 𝑧 = {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣}) → (𝐹𝑧) ∈ 𝑅))
14713, 146syl5bi 232 . . 3 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑧 ∈ ran (𝑘 ∈ {𝑤 ∈ 𝒫 𝑆 ∣ (𝑆t 𝑤) ∈ Comp}, 𝑣 ∈ (𝑆 ×t 𝑅) ↦ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣}) → (𝐹𝑧) ∈ 𝑅))
148147ralrimiv 2964 . 2 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → ∀𝑧 ∈ ran (𝑘 ∈ {𝑤 ∈ 𝒫 𝑆 ∣ (𝑆t 𝑤) ∈ Comp}, 𝑣 ∈ (𝑆 ×t 𝑅) ↦ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣})(𝐹𝑧) ∈ 𝑅)
149 simpl 473 . . 3 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → 𝑅 ∈ (TopOn‘𝑋))
150 ovex 6675 . . . . . 6 (𝑆 Cn (𝑆 ×t 𝑅)) ∈ V
151150pwex 4846 . . . . 5 𝒫 (𝑆 Cn (𝑆 ×t 𝑅)) ∈ V
1529, 10, 11xkotf 21382 . . . . . 6 (𝑘 ∈ {𝑤 ∈ 𝒫 𝑆 ∣ (𝑆t 𝑤) ∈ Comp}, 𝑣 ∈ (𝑆 ×t 𝑅) ↦ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣}):({𝑤 ∈ 𝒫 𝑆 ∣ (𝑆t 𝑤) ∈ Comp} × (𝑆 ×t 𝑅))⟶𝒫 (𝑆 Cn (𝑆 ×t 𝑅))
153 frn 6051 . . . . . 6 ((𝑘 ∈ {𝑤 ∈ 𝒫 𝑆 ∣ (𝑆t 𝑤) ∈ Comp}, 𝑣 ∈ (𝑆 ×t 𝑅) ↦ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣}):({𝑤 ∈ 𝒫 𝑆 ∣ (𝑆t 𝑤) ∈ Comp} × (𝑆 ×t 𝑅))⟶𝒫 (𝑆 Cn (𝑆 ×t 𝑅)) → ran (𝑘 ∈ {𝑤 ∈ 𝒫 𝑆 ∣ (𝑆t 𝑤) ∈ Comp}, 𝑣 ∈ (𝑆 ×t 𝑅) ↦ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣}) ⊆ 𝒫 (𝑆 Cn (𝑆 ×t 𝑅)))
154152, 153ax-mp 5 . . . . 5 ran (𝑘 ∈ {𝑤 ∈ 𝒫 𝑆 ∣ (𝑆t 𝑤) ∈ Comp}, 𝑣 ∈ (𝑆 ×t 𝑅) ↦ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣}) ⊆ 𝒫 (𝑆 Cn (𝑆 ×t 𝑅))
155151, 154ssexi 4801 . . . 4 ran (𝑘 ∈ {𝑤 ∈ 𝒫 𝑆 ∣ (𝑆t 𝑤) ∈ Comp}, 𝑣 ∈ (𝑆 ×t 𝑅) ↦ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣}) ∈ V
156155a1i 11 . . 3 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → ran (𝑘 ∈ {𝑤 ∈ 𝒫 𝑆 ∣ (𝑆t 𝑤) ∈ Comp}, 𝑣 ∈ (𝑆 ×t 𝑅) ↦ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣}) ∈ V)
1579, 10, 11xkoval 21384 . . . 4 ((𝑆 ∈ Top ∧ (𝑆 ×t 𝑅) ∈ Top) → ((𝑆 ×t 𝑅) ^ko 𝑆) = (topGen‘(fi‘ran (𝑘 ∈ {𝑤 ∈ 𝒫 𝑆 ∣ (𝑆t 𝑤) ∈ Comp}, 𝑣 ∈ (𝑆 ×t 𝑅) ↦ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣}))))
15867, 70, 157syl2anc 693 . . 3 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → ((𝑆 ×t 𝑅) ^ko 𝑆) = (topGen‘(fi‘ran (𝑘 ∈ {𝑤 ∈ 𝒫 𝑆 ∣ (𝑆t 𝑤) ∈ Comp}, 𝑣 ∈ (𝑆 ×t 𝑅) ↦ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣}))))
159 eqid 2621 . . . . 5 ((𝑆 ×t 𝑅) ^ko 𝑆) = ((𝑆 ×t 𝑅) ^ko 𝑆)
160159xkotopon 21397 . . . 4 ((𝑆 ∈ Top ∧ (𝑆 ×t 𝑅) ∈ Top) → ((𝑆 ×t 𝑅) ^ko 𝑆) ∈ (TopOn‘(𝑆 Cn (𝑆 ×t 𝑅))))
16167, 70, 160syl2anc 693 . . 3 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → ((𝑆 ×t 𝑅) ^ko 𝑆) ∈ (TopOn‘(𝑆 Cn (𝑆 ×t 𝑅))))
162149, 156, 158, 161subbascn 21052 . 2 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝑅 Cn ((𝑆 ×t 𝑅) ^ko 𝑆)) ↔ (𝐹:𝑋⟶(𝑆 Cn (𝑆 ×t 𝑅)) ∧ ∀𝑧 ∈ ran (𝑘 ∈ {𝑤 ∈ 𝒫 𝑆 ∣ (𝑆t 𝑤) ∈ Comp}, 𝑣 ∈ (𝑆 ×t 𝑅) ↦ {𝑓 ∈ (𝑆 Cn (𝑆 ×t 𝑅)) ∣ (𝑓𝑘) ⊆ 𝑣})(𝐹𝑧) ∈ 𝑅)))
1638, 148, 162mpbir2and 957 1 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → 𝐹 ∈ (𝑅 Cn ((𝑆 ×t 𝑅) ^ko 𝑆)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1482  wcel 1989  wral 2911  wrex 2912  {crab 2915  Vcvv 3198  cin 3571  wss 3572  𝒫 cpw 4156  {csn 4175  cop 4181   cuni 4434   ciun 4518  cmpt 4727   × cxp 5110  ccnv 5111  dom cdm 5112  ran crn 5113  cima 5115  Fun wfun 5880  wf 5882  cfv 5886  (class class class)co 6647  cmpt2 6649  ficfi 8313  t crest 16075  topGenctg 16092  Topctop 20692  TopOnctopon 20709   Cn ccn 21022  Compccmp 21183   ×t ctx 21357   ^ko cxko 21358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-rep 4769  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-ral 2916  df-rex 2917  df-reu 2918  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-int 4474  df-iun 4520  df-iin 4521  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-om 7063  df-1st 7165  df-2nd 7166  df-wrecs 7404  df-recs 7465  df-rdg 7503  df-1o 7557  df-oadd 7561  df-er 7739  df-map 7856  df-en 7953  df-dom 7954  df-fin 7956  df-fi 8314  df-rest 16077  df-topgen 16098  df-top 20693  df-topon 20710  df-bases 20744  df-cn 21025  df-cnp 21026  df-cmp 21184  df-tx 21359  df-xko 21360
This theorem is referenced by:  cnmpt2k  21485
  Copyright terms: Public domain W3C validator