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

Theorem xkoccn 23614
Description: The "constant function" function which maps 𝑥𝑌 to the constant function 𝑧𝑋𝑥 is a continuous function from 𝑋 into the space of continuous functions from 𝑌 to 𝑋. This can also be understood as the currying of the first projection function. (The currying of the second projection function is 𝑥𝑌 ↦ (𝑧𝑋𝑧), which we already know is continuous because it is a constant function.) (Contributed by Mario Carneiro, 19-Mar-2015.)
Assertion
Ref Expression
xkoccn ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑥𝑌 ↦ (𝑋 × {𝑥})) ∈ (𝑆 Cn (𝑆ko 𝑅)))
Distinct variable groups:   𝑥,𝑅   𝑥,𝑆   𝑥,𝑋   𝑥,𝑌

Proof of Theorem xkoccn
Dummy variables 𝑓 𝑘 𝑣 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnconst2 23278 . . . 4 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌) ∧ 𝑥𝑌) → (𝑋 × {𝑥}) ∈ (𝑅 Cn 𝑆))
213expa 1115 . . 3 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ 𝑥𝑌) → (𝑋 × {𝑥}) ∈ (𝑅 Cn 𝑆))
32fmpttd 7129 . 2 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑥𝑌 ↦ (𝑋 × {𝑥})):𝑌⟶(𝑅 Cn 𝑆))
4 eqid 2726 . . . . . 6 𝑅 = 𝑅
5 eqid 2726 . . . . . 6 {𝑧 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑧) ∈ Comp} = {𝑧 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑧) ∈ Comp}
6 eqid 2726 . . . . . 6 (𝑘 ∈ {𝑧 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑧) ∈ Comp}, 𝑣𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}) = (𝑘 ∈ {𝑧 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑧) ∈ Comp}, 𝑣𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣})
74, 5, 6xkobval 23581 . . . . 5 ran (𝑘 ∈ {𝑧 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑧) ∈ Comp}, 𝑣𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}) = {𝑦 ∣ ∃𝑘 ∈ 𝒫 𝑅𝑣𝑆 ((𝑅t 𝑘) ∈ Comp ∧ 𝑦 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣})}
87eqabri 2870 . . . 4 (𝑦 ∈ ran (𝑘 ∈ {𝑧 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑧) ∈ Comp}, 𝑣𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}) ↔ ∃𝑘 ∈ 𝒫 𝑅𝑣𝑆 ((𝑅t 𝑘) ∈ Comp ∧ 𝑦 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}))
92ad5ant15 757 . . . . . . . . . . . 12 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 = ∅) ∧ 𝑥𝑌) → (𝑋 × {𝑥}) ∈ (𝑅 Cn 𝑆))
10 simplr 767 . . . . . . . . . . . . . 14 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 = ∅) ∧ 𝑥𝑌) → 𝑘 = ∅)
1110imaeq2d 6069 . . . . . . . . . . . . 13 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 = ∅) ∧ 𝑥𝑌) → ((𝑋 × {𝑥}) “ 𝑘) = ((𝑋 × {𝑥}) “ ∅))
12 ima0 6086 . . . . . . . . . . . . . 14 ((𝑋 × {𝑥}) “ ∅) = ∅
13 0ss 4401 . . . . . . . . . . . . . 14 ∅ ⊆ 𝑣
1412, 13eqsstri 4014 . . . . . . . . . . . . 13 ((𝑋 × {𝑥}) “ ∅) ⊆ 𝑣
1511, 14eqsstrdi 4034 . . . . . . . . . . . 12 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 = ∅) ∧ 𝑥𝑌) → ((𝑋 × {𝑥}) “ 𝑘) ⊆ 𝑣)
16 imaeq1 6064 . . . . . . . . . . . . . 14 (𝑓 = (𝑋 × {𝑥}) → (𝑓𝑘) = ((𝑋 × {𝑥}) “ 𝑘))
1716sseq1d 4011 . . . . . . . . . . . . 13 (𝑓 = (𝑋 × {𝑥}) → ((𝑓𝑘) ⊆ 𝑣 ↔ ((𝑋 × {𝑥}) “ 𝑘) ⊆ 𝑣))
1817elrab 3681 . . . . . . . . . . . 12 ((𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣} ↔ ((𝑋 × {𝑥}) ∈ (𝑅 Cn 𝑆) ∧ ((𝑋 × {𝑥}) “ 𝑘) ⊆ 𝑣))
199, 15, 18sylanbrc 581 . . . . . . . . . . 11 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 = ∅) ∧ 𝑥𝑌) → (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣})
2019ralrimiva 3136 . . . . . . . . . 10 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 = ∅) → ∀𝑥𝑌 (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣})
21 rabid2 3453 . . . . . . . . . 10 (𝑌 = {𝑥𝑌 ∣ (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}} ↔ ∀𝑥𝑌 (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣})
2220, 21sylibr 233 . . . . . . . . 9 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 = ∅) → 𝑌 = {𝑥𝑌 ∣ (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}})
23 simpllr 774 . . . . . . . . . . 11 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) → 𝑆 ∈ (TopOn‘𝑌))
24 toponmax 22919 . . . . . . . . . . 11 (𝑆 ∈ (TopOn‘𝑌) → 𝑌𝑆)
2523, 24syl 17 . . . . . . . . . 10 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) → 𝑌𝑆)
2625adantr 479 . . . . . . . . 9 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 = ∅) → 𝑌𝑆)
2722, 26eqeltrrd 2827 . . . . . . . 8 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 = ∅) → {𝑥𝑌 ∣ (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}} ∈ 𝑆)
28 ifnefalse 4545 . . . . . . . . . . . . . . 15 (𝑘 ≠ ∅ → if(𝑘 = ∅, 𝑌, 𝑣) = 𝑣)
2928ad2antlr 725 . . . . . . . . . . . . . 14 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥𝑌) → if(𝑘 = ∅, 𝑌, 𝑣) = 𝑣)
3029eleq2d 2812 . . . . . . . . . . . . 13 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥𝑌) → (𝑥 ∈ if(𝑘 = ∅, 𝑌, 𝑣) ↔ 𝑥𝑣))
31 vex 3466 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
3231snss 4794 . . . . . . . . . . . . . . 15 (𝑥𝑣 ↔ {𝑥} ⊆ 𝑣)
3330, 32bitrdi 286 . . . . . . . . . . . . . 14 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥𝑌) → (𝑥 ∈ if(𝑘 = ∅, 𝑌, 𝑣) ↔ {𝑥} ⊆ 𝑣))
34 df-ima 5695 . . . . . . . . . . . . . . . . 17 ((𝑋 × {𝑥}) “ 𝑘) = ran ((𝑋 × {𝑥}) ↾ 𝑘)
35 simplrl 775 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) → 𝑘 ∈ 𝒫 𝑅)
3635ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥𝑌) → 𝑘 ∈ 𝒫 𝑅)
3736elpwid 4616 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥𝑌) → 𝑘 𝑅)
38 toponuni 22907 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ (TopOn‘𝑋) → 𝑋 = 𝑅)
3938ad5antr 732 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥𝑌) → 𝑋 = 𝑅)
4037, 39sseqtrrd 4021 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥𝑌) → 𝑘𝑋)
41 xpssres 6027 . . . . . . . . . . . . . . . . . . 19 (𝑘𝑋 → ((𝑋 × {𝑥}) ↾ 𝑘) = (𝑘 × {𝑥}))
4240, 41syl 17 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥𝑌) → ((𝑋 × {𝑥}) ↾ 𝑘) = (𝑘 × {𝑥}))
4342rneqd 5944 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥𝑌) → ran ((𝑋 × {𝑥}) ↾ 𝑘) = ran (𝑘 × {𝑥}))
4434, 43eqtrid 2778 . . . . . . . . . . . . . . . 16 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥𝑌) → ((𝑋 × {𝑥}) “ 𝑘) = ran (𝑘 × {𝑥}))
45 rnxp 6181 . . . . . . . . . . . . . . . . 17 (𝑘 ≠ ∅ → ran (𝑘 × {𝑥}) = {𝑥})
4645ad2antlr 725 . . . . . . . . . . . . . . . 16 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥𝑌) → ran (𝑘 × {𝑥}) = {𝑥})
4744, 46eqtrd 2766 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥𝑌) → ((𝑋 × {𝑥}) “ 𝑘) = {𝑥})
4847sseq1d 4011 . . . . . . . . . . . . . 14 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥𝑌) → (((𝑋 × {𝑥}) “ 𝑘) ⊆ 𝑣 ↔ {𝑥} ⊆ 𝑣))
492ad5ant15 757 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥𝑌) → (𝑋 × {𝑥}) ∈ (𝑅 Cn 𝑆))
5049biantrurd 531 . . . . . . . . . . . . . 14 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥𝑌) → (((𝑋 × {𝑥}) “ 𝑘) ⊆ 𝑣 ↔ ((𝑋 × {𝑥}) ∈ (𝑅 Cn 𝑆) ∧ ((𝑋 × {𝑥}) “ 𝑘) ⊆ 𝑣)))
5133, 48, 503bitr2d 306 . . . . . . . . . . . . 13 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥𝑌) → (𝑥 ∈ if(𝑘 = ∅, 𝑌, 𝑣) ↔ ((𝑋 × {𝑥}) ∈ (𝑅 Cn 𝑆) ∧ ((𝑋 × {𝑥}) “ 𝑘) ⊆ 𝑣)))
5230, 51bitr3d 280 . . . . . . . . . . . 12 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥𝑌) → (𝑥𝑣 ↔ ((𝑋 × {𝑥}) ∈ (𝑅 Cn 𝑆) ∧ ((𝑋 × {𝑥}) “ 𝑘) ⊆ 𝑣)))
5352, 18bitr4di 288 . . . . . . . . . . 11 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) ∧ 𝑥𝑌) → (𝑥𝑣 ↔ (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}))
5453rabbi2dva 4219 . . . . . . . . . 10 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) → (𝑌𝑣) = {𝑥𝑌 ∣ (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}})
55 simplrr 776 . . . . . . . . . . . . 13 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) → 𝑣𝑆)
56 toponss 22920 . . . . . . . . . . . . 13 ((𝑆 ∈ (TopOn‘𝑌) ∧ 𝑣𝑆) → 𝑣𝑌)
5723, 55, 56syl2anc 582 . . . . . . . . . . . 12 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) → 𝑣𝑌)
5857adantr 479 . . . . . . . . . . 11 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) → 𝑣𝑌)
59 sseqin2 4216 . . . . . . . . . . 11 (𝑣𝑌 ↔ (𝑌𝑣) = 𝑣)
6058, 59sylib 217 . . . . . . . . . 10 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) → (𝑌𝑣) = 𝑣)
6154, 60eqtr3d 2768 . . . . . . . . 9 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) → {𝑥𝑌 ∣ (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}} = 𝑣)
6255adantr 479 . . . . . . . . 9 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) → 𝑣𝑆)
6361, 62eqeltrd 2826 . . . . . . . 8 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑘 ≠ ∅) → {𝑥𝑌 ∣ (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}} ∈ 𝑆)
6427, 63pm2.61dane 3019 . . . . . . 7 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) → {𝑥𝑌 ∣ (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}} ∈ 𝑆)
65 imaeq2 6065 . . . . . . . . 9 (𝑦 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣} → ((𝑥𝑌 ↦ (𝑋 × {𝑥})) “ 𝑦) = ((𝑥𝑌 ↦ (𝑋 × {𝑥})) “ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}))
66 eqid 2726 . . . . . . . . . 10 (𝑥𝑌 ↦ (𝑋 × {𝑥})) = (𝑥𝑌 ↦ (𝑋 × {𝑥}))
6766mptpreima 6249 . . . . . . . . 9 ((𝑥𝑌 ↦ (𝑋 × {𝑥})) “ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}) = {𝑥𝑌 ∣ (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}}
6865, 67eqtrdi 2782 . . . . . . . 8 (𝑦 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣} → ((𝑥𝑌 ↦ (𝑋 × {𝑥})) “ 𝑦) = {𝑥𝑌 ∣ (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}})
6968eleq1d 2811 . . . . . . 7 (𝑦 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣} → (((𝑥𝑌 ↦ (𝑋 × {𝑥})) “ 𝑦) ∈ 𝑆 ↔ {𝑥𝑌 ∣ (𝑋 × {𝑥}) ∈ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}} ∈ 𝑆))
7064, 69syl5ibrcom 246 . . . . . 6 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) ∧ (𝑅t 𝑘) ∈ Comp) → (𝑦 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣} → ((𝑥𝑌 ↦ (𝑋 × {𝑥})) “ 𝑦) ∈ 𝑆))
7170expimpd 452 . . . . 5 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑆)) → (((𝑅t 𝑘) ∈ Comp ∧ 𝑦 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}) → ((𝑥𝑌 ↦ (𝑋 × {𝑥})) “ 𝑦) ∈ 𝑆))
7271rexlimdvva 3202 . . . 4 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (∃𝑘 ∈ 𝒫 𝑅𝑣𝑆 ((𝑅t 𝑘) ∈ Comp ∧ 𝑦 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}) → ((𝑥𝑌 ↦ (𝑋 × {𝑥})) “ 𝑦) ∈ 𝑆))
738, 72biimtrid 241 . . 3 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑦 ∈ ran (𝑘 ∈ {𝑧 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑧) ∈ Comp}, 𝑣𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}) → ((𝑥𝑌 ↦ (𝑋 × {𝑥})) “ 𝑦) ∈ 𝑆))
7473ralrimiv 3135 . 2 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → ∀𝑦 ∈ ran (𝑘 ∈ {𝑧 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑧) ∈ Comp}, 𝑣𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣})((𝑥𝑌 ↦ (𝑋 × {𝑥})) “ 𝑦) ∈ 𝑆)
75 simpr 483 . . 3 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → 𝑆 ∈ (TopOn‘𝑌))
76 ovex 7457 . . . . . 6 (𝑅 Cn 𝑆) ∈ V
7776pwex 5384 . . . . 5 𝒫 (𝑅 Cn 𝑆) ∈ V
784, 5, 6xkotf 23580 . . . . . 6 (𝑘 ∈ {𝑧 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑧) ∈ Comp}, 𝑣𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}):({𝑧 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑧) ∈ Comp} × 𝑆)⟶𝒫 (𝑅 Cn 𝑆)
79 frn 6735 . . . . . 6 ((𝑘 ∈ {𝑧 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑧) ∈ Comp}, 𝑣𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}):({𝑧 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑧) ∈ Comp} × 𝑆)⟶𝒫 (𝑅 Cn 𝑆) → ran (𝑘 ∈ {𝑧 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑧) ∈ Comp}, 𝑣𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}) ⊆ 𝒫 (𝑅 Cn 𝑆))
8078, 79ax-mp 5 . . . . 5 ran (𝑘 ∈ {𝑧 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑧) ∈ Comp}, 𝑣𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}) ⊆ 𝒫 (𝑅 Cn 𝑆)
8177, 80ssexi 5327 . . . 4 ran (𝑘 ∈ {𝑧 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑧) ∈ Comp}, 𝑣𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}) ∈ V
8281a1i 11 . . 3 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → ran (𝑘 ∈ {𝑧 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑧) ∈ Comp}, 𝑣𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}) ∈ V)
83 topontop 22906 . . . 4 (𝑅 ∈ (TopOn‘𝑋) → 𝑅 ∈ Top)
84 topontop 22906 . . . 4 (𝑆 ∈ (TopOn‘𝑌) → 𝑆 ∈ Top)
854, 5, 6xkoval 23582 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆ko 𝑅) = (topGen‘(fi‘ran (𝑘 ∈ {𝑧 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑧) ∈ Comp}, 𝑣𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}))))
8683, 84, 85syl2an 594 . . 3 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑆ko 𝑅) = (topGen‘(fi‘ran (𝑘 ∈ {𝑧 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑧) ∈ Comp}, 𝑣𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣}))))
87 eqid 2726 . . . . 5 (𝑆ko 𝑅) = (𝑆ko 𝑅)
8887xkotopon 23595 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆ko 𝑅) ∈ (TopOn‘(𝑅 Cn 𝑆)))
8983, 84, 88syl2an 594 . . 3 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑆ko 𝑅) ∈ (TopOn‘(𝑅 Cn 𝑆)))
9075, 82, 86, 89subbascn 23249 . 2 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → ((𝑥𝑌 ↦ (𝑋 × {𝑥})) ∈ (𝑆 Cn (𝑆ko 𝑅)) ↔ ((𝑥𝑌 ↦ (𝑋 × {𝑥})):𝑌⟶(𝑅 Cn 𝑆) ∧ ∀𝑦 ∈ ran (𝑘 ∈ {𝑧 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑧) ∈ Comp}, 𝑣𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓𝑘) ⊆ 𝑣})((𝑥𝑌 ↦ (𝑋 × {𝑥})) “ 𝑦) ∈ 𝑆)))
913, 74, 90mpbir2and 711 1 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑥𝑌 ↦ (𝑋 × {𝑥})) ∈ (𝑆 Cn (𝑆ko 𝑅)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1534  wcel 2099  wne 2930  wral 3051  wrex 3060  {crab 3419  Vcvv 3462  cin 3946  wss 3947  c0 4325  ifcif 4533  𝒫 cpw 4607  {csn 4633   cuni 4913  cmpt 5236   × cxp 5680  ccnv 5681  ran crn 5683  cres 5684  cima 5685  wf 6550  cfv 6554  (class class class)co 7424  cmpo 7426  ficfi 9453  t crest 17435  topGenctg 17452  Topctop 22886  TopOnctopon 22903   Cn ccn 23219  Compccmp 23381  ko cxko 23556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5290  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-int 4955  df-iun 5003  df-iin 5004  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7877  df-1st 8003  df-2nd 8004  df-1o 8496  df-2o 8497  df-map 8857  df-en 8975  df-dom 8976  df-fin 8978  df-fi 9454  df-rest 17437  df-topgen 17458  df-top 22887  df-topon 22904  df-bases 22940  df-cn 23222  df-cnp 23223  df-cmp 23382  df-xko 23558
This theorem is referenced by:  cnmptkc  23674  xkofvcn  23679
  Copyright terms: Public domain W3C validator