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

Theorem xkoptsub 23662
Description: The compact-open topology is finer than the product topology restricted to continuous functions. (Contributed by Mario Carneiro, 19-Mar-2015.)
Hypotheses
Ref Expression
xkoptsub.x 𝑋 = 𝑅
xkoptsub.j 𝐽 = (∏t‘(𝑋 × {𝑆}))
Assertion
Ref Expression
xkoptsub ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽t (𝑅 Cn 𝑆)) ⊆ (𝑆ko 𝑅))

Proof of Theorem xkoptsub
Dummy variables 𝑓 𝑔 𝑘 𝑛 𝑢 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xkoptsub.j . . . . 5 𝐽 = (∏t‘(𝑋 × {𝑆}))
2 xkoptsub.x . . . . . . . . 9 𝑋 = 𝑅
32topopn 22912 . . . . . . . 8 (𝑅 ∈ Top → 𝑋𝑅)
43adantr 480 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑋𝑅)
5 fconstg 6795 . . . . . . . . 9 (𝑆 ∈ Top → (𝑋 × {𝑆}):𝑋⟶{𝑆})
65adantl 481 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}):𝑋⟶{𝑆})
76ffnd 6737 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}) Fn 𝑋)
8 eqid 2737 . . . . . . . 8 {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))}
98ptval 23578 . . . . . . 7 ((𝑋𝑅 ∧ (𝑋 × {𝑆}) Fn 𝑋) → (∏t‘(𝑋 × {𝑆})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))}))
104, 7, 9syl2anc 584 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∏t‘(𝑋 × {𝑆})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))}))
11 simpr 484 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑆 ∈ Top)
1211snssd 4809 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑆} ⊆ Top)
136, 12fssd 6753 . . . . . . . . 9 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}):𝑋⟶Top)
14 eqid 2737 . . . . . . . . . 10 X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) = X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛)
158, 14ptbasfi 23589 . . . . . . . . 9 ((𝑋𝑅 ∧ (𝑋 × {𝑆}):𝑋⟶Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))} = (fi‘({X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢)))))
164, 13, 15syl2anc 584 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))} = (fi‘({X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢)))))
17 fvconst2g 7222 . . . . . . . . . . . . . . 15 ((𝑆 ∈ Top ∧ 𝑛𝑋) → ((𝑋 × {𝑆})‘𝑛) = 𝑆)
1817adantll 714 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛𝑋) → ((𝑋 × {𝑆})‘𝑛) = 𝑆)
1918unieqd 4920 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛𝑋) → ((𝑋 × {𝑆})‘𝑛) = 𝑆)
2019ixpeq2dva 8952 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) = X𝑛𝑋 𝑆)
21 eqid 2737 . . . . . . . . . . . . . 14 𝑆 = 𝑆
2221topopn 22912 . . . . . . . . . . . . 13 (𝑆 ∈ Top → 𝑆𝑆)
23 ixpconstg 8946 . . . . . . . . . . . . 13 ((𝑋𝑅 𝑆𝑆) → X𝑛𝑋 𝑆 = ( 𝑆m 𝑋))
243, 22, 23syl2an 596 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛𝑋 𝑆 = ( 𝑆m 𝑋))
2520, 24eqtrd 2777 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) = ( 𝑆m 𝑋))
2625sneqd 4638 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛)} = {( 𝑆m 𝑋)})
27 eqid 2737 . . . . . . . . . . . 12 𝑋 = 𝑋
28 fvconst2g 7222 . . . . . . . . . . . . . . 15 ((𝑆 ∈ Top ∧ 𝑘𝑋) → ((𝑋 × {𝑆})‘𝑘) = 𝑆)
2928adantll 714 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → ((𝑋 × {𝑆})‘𝑘) = 𝑆)
3025adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) = ( 𝑆m 𝑋))
3130mpteq1d 5237 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → (𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) = (𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)))
3231cnveqd 5886 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → (𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) = (𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)))
3332imaeq1d 6077 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))
3433ralrimivw 3150 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))
3529, 34jca 511 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))
3635ralrimiva 3146 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∀𝑘𝑋 (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))
37 mpoeq123 7505 . . . . . . . . . . . 12 ((𝑋 = 𝑋 ∧ ∀𝑘𝑋 (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) → (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢)) = (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))
3827, 36, 37sylancr 587 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢)) = (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))
3938rneqd 5949 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢)) = ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))
4026, 39uneq12d 4169 . . . . . . . . 9 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ({X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢))) = ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))
4140fveq2d 6910 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (fi‘({X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢)))) = (fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))))
4216, 41eqtrd 2777 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))} = (fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))))
4342fveq2d 6910 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))}) = (topGen‘(fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))))
4410, 43eqtrd 2777 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∏t‘(𝑋 × {𝑆})) = (topGen‘(fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))))
451, 44eqtrid 2789 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝐽 = (topGen‘(fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))))
4645oveq1d 7446 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽t (𝑅 Cn 𝑆)) = ((topGen‘(fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆)))
47 firest 17477 . . . . 5 (fi‘(({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆))) = ((fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆))
4847fveq2i 6909 . . . 4 (topGen‘(fi‘(({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) = (topGen‘((fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆)))
49 fvex 6919 . . . . 5 (fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) ∈ V
50 ovex 7464 . . . . 5 (𝑅 Cn 𝑆) ∈ V
51 tgrest 23167 . . . . 5 (((fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) ∈ V ∧ (𝑅 Cn 𝑆) ∈ V) → (topGen‘((fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆))) = ((topGen‘(fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆)))
5249, 50, 51mp2an 692 . . . 4 (topGen‘((fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆))) = ((topGen‘(fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆))
5348, 52eqtri 2765 . . 3 (topGen‘(fi‘(({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) = ((topGen‘(fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆))
5446, 53eqtr4di 2795 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽t (𝑅 Cn 𝑆)) = (topGen‘(fi‘(({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))))
55 xkotop 23596 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆ko 𝑅) ∈ Top)
56 snex 5436 . . . . . 6 {( 𝑆m 𝑋)} ∈ V
57 mpoexga 8102 . . . . . . . 8 ((𝑋𝑅𝑆 ∈ Top) → (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V)
583, 57sylan 580 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V)
59 rnexg 7924 . . . . . . 7 ((𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V → ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V)
6058, 59syl 17 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V)
61 unexg 7763 . . . . . 6 (({( 𝑆m 𝑋)} ∈ V ∧ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V) → ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
6256, 60, 61sylancr 587 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
63 restval 17471 . . . . 5 ((({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ∈ V ∧ (𝑅 Cn 𝑆) ∈ V) → (({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) = ran (𝑥 ∈ ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))))
6462, 50, 63sylancl 586 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) = ran (𝑥 ∈ ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))))
65 elun 4153 . . . . . . 7 (𝑥 ∈ ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↔ (𝑥 ∈ {( 𝑆m 𝑋)} ∨ 𝑥 ∈ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))
662, 21cnf 23254 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝑅 Cn 𝑆) → 𝑥:𝑋 𝑆)
67 elmapg 8879 . . . . . . . . . . . . . . 15 (( 𝑆𝑆𝑋𝑅) → (𝑥 ∈ ( 𝑆m 𝑋) ↔ 𝑥:𝑋 𝑆))
6822, 3, 67syl2anr 597 . . . . . . . . . . . . . 14 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ ( 𝑆m 𝑋) ↔ 𝑥:𝑋 𝑆))
6966, 68imbitrrid 246 . . . . . . . . . . . . 13 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ (𝑅 Cn 𝑆) → 𝑥 ∈ ( 𝑆m 𝑋)))
7069ssrdv 3989 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) ⊆ ( 𝑆m 𝑋))
7170adantr 480 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆m 𝑋)}) → (𝑅 Cn 𝑆) ⊆ ( 𝑆m 𝑋))
72 elsni 4643 . . . . . . . . . . . 12 (𝑥 ∈ {( 𝑆m 𝑋)} → 𝑥 = ( 𝑆m 𝑋))
7372adantl 481 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆m 𝑋)}) → 𝑥 = ( 𝑆m 𝑋))
7471, 73sseqtrrd 4021 . . . . . . . . . 10 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆m 𝑋)}) → (𝑅 Cn 𝑆) ⊆ 𝑥)
75 sseqin2 4223 . . . . . . . . . 10 ((𝑅 Cn 𝑆) ⊆ 𝑥 ↔ (𝑥 ∩ (𝑅 Cn 𝑆)) = (𝑅 Cn 𝑆))
7674, 75sylib 218 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆m 𝑋)}) → (𝑥 ∩ (𝑅 Cn 𝑆)) = (𝑅 Cn 𝑆))
77 eqid 2737 . . . . . . . . . . . 12 (𝑆ko 𝑅) = (𝑆ko 𝑅)
7877xkouni 23607 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) = (𝑆ko 𝑅))
79 eqid 2737 . . . . . . . . . . . . 13 (𝑆ko 𝑅) = (𝑆ko 𝑅)
8079topopn 22912 . . . . . . . . . . . 12 ((𝑆ko 𝑅) ∈ Top → (𝑆ko 𝑅) ∈ (𝑆ko 𝑅))
8155, 80syl 17 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆ko 𝑅) ∈ (𝑆ko 𝑅))
8278, 81eqeltrd 2841 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) ∈ (𝑆ko 𝑅))
8382adantr 480 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆m 𝑋)}) → (𝑅 Cn 𝑆) ∈ (𝑆ko 𝑅))
8476, 83eqeltrd 2841 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆m 𝑋)}) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅))
85 eqid 2737 . . . . . . . . . . 11 (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) = (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))
8685rnmpo 7566 . . . . . . . . . 10 ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) = {𝑥 ∣ ∃𝑘𝑋𝑢𝑆 𝑥 = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)}
8786eqabri 2885 . . . . . . . . 9 (𝑥 ∈ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ↔ ∃𝑘𝑋𝑢𝑆 𝑥 = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))
88 cnvresima 6250 . . . . . . . . . . . . . . 15 (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) ↾ (𝑅 Cn 𝑆)) “ 𝑢) = (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆))
8970adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑅 Cn 𝑆) ⊆ ( 𝑆m 𝑋))
9089resmptd 6058 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) ↾ (𝑅 Cn 𝑆)) = (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)))
9190cnveqd 5886 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) ↾ (𝑅 Cn 𝑆)) = (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)))
9291imaeq1d 6077 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) ↾ (𝑅 Cn 𝑆)) “ 𝑢) = ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢))
9388, 92eqtr3id 2791 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) = ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢))
94 fvex 6919 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝑘) ∈ V
9594rgenw 3065 . . . . . . . . . . . . . . . . . . 19 𝑤 ∈ (𝑅 Cn 𝑆)(𝑤𝑘) ∈ V
96 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) = (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))
9796fnmpt 6708 . . . . . . . . . . . . . . . . . . 19 (∀𝑤 ∈ (𝑅 Cn 𝑆)(𝑤𝑘) ∈ V → (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) Fn (𝑅 Cn 𝑆))
9895, 97mp1i 13 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) Fn (𝑅 Cn 𝑆))
99 elpreima 7078 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) Fn (𝑅 Cn 𝑆) → (𝑓 ∈ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) ∈ 𝑢)))
10098, 99syl 17 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑓 ∈ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) ∈ 𝑢)))
101 fveq1 6905 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑓 → (𝑤𝑘) = (𝑓𝑘))
102 fvex 6919 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓𝑘) ∈ V
103101, 96, 102fvmpt 7016 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ (𝑅 Cn 𝑆) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) = (𝑓𝑘))
104103adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) = (𝑓𝑘))
105104eleq1d 2826 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → (((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) ∈ 𝑢 ↔ (𝑓𝑘) ∈ 𝑢))
106102snss 4785 . . . . . . . . . . . . . . . . . . . 20 ((𝑓𝑘) ∈ 𝑢 ↔ {(𝑓𝑘)} ⊆ 𝑢)
10789sselda 3983 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑓 ∈ ( 𝑆m 𝑋))
108 elmapi 8889 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 ∈ ( 𝑆m 𝑋) → 𝑓:𝑋 𝑆)
109 ffn 6736 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓:𝑋 𝑆𝑓 Fn 𝑋)
110107, 108, 1093syl 18 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑓 Fn 𝑋)
111 simplrl 777 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑘𝑋)
112 fnsnfv 6988 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 Fn 𝑋𝑘𝑋) → {(𝑓𝑘)} = (𝑓 “ {𝑘}))
113110, 111, 112syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → {(𝑓𝑘)} = (𝑓 “ {𝑘}))
114113sseq1d 4015 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ({(𝑓𝑘)} ⊆ 𝑢 ↔ (𝑓 “ {𝑘}) ⊆ 𝑢))
115106, 114bitrid 283 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ((𝑓𝑘) ∈ 𝑢 ↔ (𝑓 “ {𝑘}) ⊆ 𝑢))
116105, 115bitrd 279 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → (((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) ∈ 𝑢 ↔ (𝑓 “ {𝑘}) ⊆ 𝑢))
117116pm5.32da 579 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → ((𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) ∈ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)))
118100, 117bitrd 279 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑓 ∈ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)))
119118eqabdv 2875 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢) = {𝑓 ∣ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)})
120 df-rab 3437 . . . . . . . . . . . . . . 15 {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢} = {𝑓 ∣ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)}
121119, 120eqtr4di 2795 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢) = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢})
12293, 121eqtrd 2777 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢})
123 simpll 767 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → 𝑅 ∈ Top)
12411adantr 480 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → 𝑆 ∈ Top)
125 simprl 771 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → 𝑘𝑋)
126125snssd 4809 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → {𝑘} ⊆ 𝑋)
1272toptopon 22923 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘𝑋))
128123, 127sylib 218 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → 𝑅 ∈ (TopOn‘𝑋))
129 restsn2 23179 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑘𝑋) → (𝑅t {𝑘}) = 𝒫 {𝑘})
130128, 125, 129syl2anc 584 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑅t {𝑘}) = 𝒫 {𝑘})
131 snfi 9083 . . . . . . . . . . . . . . . 16 {𝑘} ∈ Fin
132 discmp 23406 . . . . . . . . . . . . . . . 16 ({𝑘} ∈ Fin ↔ 𝒫 {𝑘} ∈ Comp)
133131, 132mpbi 230 . . . . . . . . . . . . . . 15 𝒫 {𝑘} ∈ Comp
134130, 133eqeltrdi 2849 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑅t {𝑘}) ∈ Comp)
135 simprr 773 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → 𝑢𝑆)
1362, 123, 124, 126, 134, 135xkoopn 23597 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢} ∈ (𝑆ko 𝑅))
137122, 136eqeltrd 2841 . . . . . . . . . . . 12 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅))
138 ineq1 4213 . . . . . . . . . . . . 13 (𝑥 = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) = (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)))
139138eleq1d 2826 . . . . . . . . . . . 12 (𝑥 = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) → ((𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅) ↔ (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅)))
140137, 139syl5ibrcom 247 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑥 = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅)))
141140rexlimdvva 3213 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∃𝑘𝑋𝑢𝑆 𝑥 = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅)))
142141imp 406 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ ∃𝑘𝑋𝑢𝑆 𝑥 = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅))
14387, 142sylan2b 594 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅))
14484, 143jaodan 960 . . . . . . 7 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑥 ∈ {( 𝑆m 𝑋)} ∨ 𝑥 ∈ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅))
14565, 144sylan2b 594 . . . . . 6 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅))
146145fmpttd 7135 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))):({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))⟶(𝑆ko 𝑅))
147146frnd 6744 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑥 ∈ ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))) ⊆ (𝑆ko 𝑅))
14864, 147eqsstrd 4018 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) ⊆ (𝑆ko 𝑅))
149 tgfiss 22998 . . 3 (((𝑆ko 𝑅) ∈ Top ∧ (({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) ⊆ (𝑆ko 𝑅)) → (topGen‘(fi‘(({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) ⊆ (𝑆ko 𝑅))
15055, 148, 149syl2anc 584 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (topGen‘(fi‘(({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) ⊆ (𝑆ko 𝑅))
15154, 150eqsstrd 4018 1 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽t (𝑅 Cn 𝑆)) ⊆ (𝑆ko 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 848  w3a 1087   = wceq 1540  wex 1779  wcel 2108  {cab 2714  wral 3061  wrex 3070  {crab 3436  Vcvv 3480  cdif 3948  cun 3949  cin 3950  wss 3951  𝒫 cpw 4600  {csn 4626   cuni 4907  cmpt 5225   × cxp 5683  ccnv 5684  ran crn 5686  cres 5687  cima 5688   Fn wfn 6556  wf 6557  cfv 6561  (class class class)co 7431  cmpo 7433  m cmap 8866  Xcixp 8937  Fincfn 8985  ficfi 9450  t crest 17465  topGenctg 17482  tcpt 17483  Topctop 22899  TopOnctopon 22916   Cn ccn 23232  Compccmp 23394  ko cxko 23569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-1o 8506  df-2o 8507  df-map 8868  df-ixp 8938  df-en 8986  df-dom 8987  df-fin 8989  df-fi 9451  df-rest 17467  df-topgen 17488  df-pt 17489  df-top 22900  df-topon 22917  df-bases 22953  df-cn 23235  df-cmp 23395  df-xko 23571
This theorem is referenced by:  xkopt  23663  xkopjcn  23664
  Copyright terms: Public domain W3C validator