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

Theorem xkoptsub 23545
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 22795 . . . . . . . 8 (𝑅 ∈ Top → 𝑋𝑅)
43adantr 480 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑋𝑅)
5 fconstg 6778 . . . . . . . . 9 (𝑆 ∈ Top → (𝑋 × {𝑆}):𝑋⟶{𝑆})
65adantl 481 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}):𝑋⟶{𝑆})
76ffnd 6717 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}) Fn 𝑋)
8 eqid 2727 . . . . . . . 8 {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))}
98ptval 23461 . . . . . . 7 ((𝑋𝑅 ∧ (𝑋 × {𝑆}) Fn 𝑋) → (∏t‘(𝑋 × {𝑆})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))}))
104, 7, 9syl2anc 583 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∏t‘(𝑋 × {𝑆})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))}))
11 simpr 484 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑆 ∈ Top)
1211snssd 4808 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑆} ⊆ Top)
136, 12fssd 6734 . . . . . . . . 9 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}):𝑋⟶Top)
14 eqid 2727 . . . . . . . . . 10 X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) = X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛)
158, 14ptbasfi 23472 . . . . . . . . 9 ((𝑋𝑅 ∧ (𝑋 × {𝑆}):𝑋⟶Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))} = (fi‘({X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢)))))
164, 13, 15syl2anc 583 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))} = (fi‘({X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢)))))
17 fvconst2g 7208 . . . . . . . . . . . . . . 15 ((𝑆 ∈ Top ∧ 𝑛𝑋) → ((𝑋 × {𝑆})‘𝑛) = 𝑆)
1817adantll 713 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛𝑋) → ((𝑋 × {𝑆})‘𝑛) = 𝑆)
1918unieqd 4916 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛𝑋) → ((𝑋 × {𝑆})‘𝑛) = 𝑆)
2019ixpeq2dva 8922 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) = X𝑛𝑋 𝑆)
21 eqid 2727 . . . . . . . . . . . . . 14 𝑆 = 𝑆
2221topopn 22795 . . . . . . . . . . . . 13 (𝑆 ∈ Top → 𝑆𝑆)
23 ixpconstg 8916 . . . . . . . . . . . . 13 ((𝑋𝑅 𝑆𝑆) → X𝑛𝑋 𝑆 = ( 𝑆m 𝑋))
243, 22, 23syl2an 595 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛𝑋 𝑆 = ( 𝑆m 𝑋))
2520, 24eqtrd 2767 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) = ( 𝑆m 𝑋))
2625sneqd 4636 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛)} = {( 𝑆m 𝑋)})
27 eqid 2727 . . . . . . . . . . . 12 𝑋 = 𝑋
28 fvconst2g 7208 . . . . . . . . . . . . . . 15 ((𝑆 ∈ Top ∧ 𝑘𝑋) → ((𝑋 × {𝑆})‘𝑘) = 𝑆)
2928adantll 713 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → ((𝑋 × {𝑆})‘𝑘) = 𝑆)
3025adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) = ( 𝑆m 𝑋))
3130mpteq1d 5237 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → (𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) = (𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)))
3231cnveqd 5872 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → (𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) = (𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)))
3332imaeq1d 6056 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))
3433ralrimivw 3145 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))
3529, 34jca 511 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))
3635ralrimiva 3141 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∀𝑘𝑋 (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))
37 mpoeq123 7486 . . . . . . . . . . . 12 ((𝑋 = 𝑋 ∧ ∀𝑘𝑋 (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) → (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢)) = (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))
3827, 36, 37sylancr 586 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢)) = (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))
3938rneqd 5934 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢)) = ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))
4026, 39uneq12d 4160 . . . . . . . . 9 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ({X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢))) = ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))
4140fveq2d 6895 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (fi‘({X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢)))) = (fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))))
4216, 41eqtrd 2767 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))} = (fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))))
4342fveq2d 6895 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))}) = (topGen‘(fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))))
4410, 43eqtrd 2767 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∏t‘(𝑋 × {𝑆})) = (topGen‘(fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))))
451, 44eqtrid 2779 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝐽 = (topGen‘(fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))))
4645oveq1d 7429 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽t (𝑅 Cn 𝑆)) = ((topGen‘(fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆)))
47 firest 17405 . . . . 5 (fi‘(({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆))) = ((fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆))
4847fveq2i 6894 . . . 4 (topGen‘(fi‘(({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) = (topGen‘((fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆)))
49 fvex 6904 . . . . 5 (fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) ∈ V
50 ovex 7447 . . . . 5 (𝑅 Cn 𝑆) ∈ V
51 tgrest 23050 . . . . 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 691 . . . 4 (topGen‘((fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆))) = ((topGen‘(fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆))
5348, 52eqtri 2755 . . 3 (topGen‘(fi‘(({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) = ((topGen‘(fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆))
5446, 53eqtr4di 2785 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽t (𝑅 Cn 𝑆)) = (topGen‘(fi‘(({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))))
55 xkotop 23479 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆ko 𝑅) ∈ Top)
56 snex 5427 . . . . . 6 {( 𝑆m 𝑋)} ∈ V
57 mpoexga 8076 . . . . . . . 8 ((𝑋𝑅𝑆 ∈ Top) → (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V)
583, 57sylan 579 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V)
59 rnexg 7904 . . . . . . 7 ((𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V → ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V)
6058, 59syl 17 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V)
61 unexg 7745 . . . . . 6 (({( 𝑆m 𝑋)} ∈ V ∧ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V) → ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
6256, 60, 61sylancr 586 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
63 restval 17399 . . . . 5 ((({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ∈ V ∧ (𝑅 Cn 𝑆) ∈ V) → (({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) = ran (𝑥 ∈ ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))))
6462, 50, 63sylancl 585 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) = ran (𝑥 ∈ ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))))
65 elun 4144 . . . . . . 7 (𝑥 ∈ ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↔ (𝑥 ∈ {( 𝑆m 𝑋)} ∨ 𝑥 ∈ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))
662, 21cnf 23137 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝑅 Cn 𝑆) → 𝑥:𝑋 𝑆)
67 elmapg 8849 . . . . . . . . . . . . . . 15 (( 𝑆𝑆𝑋𝑅) → (𝑥 ∈ ( 𝑆m 𝑋) ↔ 𝑥:𝑋 𝑆))
6822, 3, 67syl2anr 596 . . . . . . . . . . . . . 14 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ ( 𝑆m 𝑋) ↔ 𝑥:𝑋 𝑆))
6966, 68imbitrrid 245 . . . . . . . . . . . . 13 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ (𝑅 Cn 𝑆) → 𝑥 ∈ ( 𝑆m 𝑋)))
7069ssrdv 3984 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) ⊆ ( 𝑆m 𝑋))
7170adantr 480 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆m 𝑋)}) → (𝑅 Cn 𝑆) ⊆ ( 𝑆m 𝑋))
72 elsni 4641 . . . . . . . . . . . 12 (𝑥 ∈ {( 𝑆m 𝑋)} → 𝑥 = ( 𝑆m 𝑋))
7372adantl 481 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆m 𝑋)}) → 𝑥 = ( 𝑆m 𝑋))
7471, 73sseqtrrd 4019 . . . . . . . . . 10 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆m 𝑋)}) → (𝑅 Cn 𝑆) ⊆ 𝑥)
75 sseqin2 4211 . . . . . . . . . 10 ((𝑅 Cn 𝑆) ⊆ 𝑥 ↔ (𝑥 ∩ (𝑅 Cn 𝑆)) = (𝑅 Cn 𝑆))
7674, 75sylib 217 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆m 𝑋)}) → (𝑥 ∩ (𝑅 Cn 𝑆)) = (𝑅 Cn 𝑆))
77 eqid 2727 . . . . . . . . . . . 12 (𝑆ko 𝑅) = (𝑆ko 𝑅)
7877xkouni 23490 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) = (𝑆ko 𝑅))
79 eqid 2727 . . . . . . . . . . . . 13 (𝑆ko 𝑅) = (𝑆ko 𝑅)
8079topopn 22795 . . . . . . . . . . . 12 ((𝑆ko 𝑅) ∈ Top → (𝑆ko 𝑅) ∈ (𝑆ko 𝑅))
8155, 80syl 17 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆ko 𝑅) ∈ (𝑆ko 𝑅))
8278, 81eqeltrd 2828 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) ∈ (𝑆ko 𝑅))
8382adantr 480 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆m 𝑋)}) → (𝑅 Cn 𝑆) ∈ (𝑆ko 𝑅))
8476, 83eqeltrd 2828 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆m 𝑋)}) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅))
85 eqid 2727 . . . . . . . . . . 11 (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) = (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))
8685rnmpo 7548 . . . . . . . . . 10 ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) = {𝑥 ∣ ∃𝑘𝑋𝑢𝑆 𝑥 = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)}
8786eqabri 2872 . . . . . . . . 9 (𝑥 ∈ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ↔ ∃𝑘𝑋𝑢𝑆 𝑥 = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))
88 cnvresima 6228 . . . . . . . . . . . . . . 15 (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) ↾ (𝑅 Cn 𝑆)) “ 𝑢) = (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆))
8970adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑅 Cn 𝑆) ⊆ ( 𝑆m 𝑋))
9089resmptd 6038 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) ↾ (𝑅 Cn 𝑆)) = (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)))
9190cnveqd 5872 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) ↾ (𝑅 Cn 𝑆)) = (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)))
9291imaeq1d 6056 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) ↾ (𝑅 Cn 𝑆)) “ 𝑢) = ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢))
9388, 92eqtr3id 2781 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) = ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢))
94 fvex 6904 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝑘) ∈ V
9594rgenw 3060 . . . . . . . . . . . . . . . . . . 19 𝑤 ∈ (𝑅 Cn 𝑆)(𝑤𝑘) ∈ V
96 eqid 2727 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) = (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))
9796fnmpt 6689 . . . . . . . . . . . . . . . . . . 19 (∀𝑤 ∈ (𝑅 Cn 𝑆)(𝑤𝑘) ∈ V → (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) Fn (𝑅 Cn 𝑆))
9895, 97mp1i 13 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) Fn (𝑅 Cn 𝑆))
99 elpreima 7061 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) Fn (𝑅 Cn 𝑆) → (𝑓 ∈ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) ∈ 𝑢)))
10098, 99syl 17 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑓 ∈ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) ∈ 𝑢)))
101 fveq1 6890 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑓 → (𝑤𝑘) = (𝑓𝑘))
102 fvex 6904 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓𝑘) ∈ V
103101, 96, 102fvmpt 6999 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ (𝑅 Cn 𝑆) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) = (𝑓𝑘))
104103adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) = (𝑓𝑘))
105104eleq1d 2813 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → (((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) ∈ 𝑢 ↔ (𝑓𝑘) ∈ 𝑢))
106102snss 4785 . . . . . . . . . . . . . . . . . . . 20 ((𝑓𝑘) ∈ 𝑢 ↔ {(𝑓𝑘)} ⊆ 𝑢)
10789sselda 3978 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑓 ∈ ( 𝑆m 𝑋))
108 elmapi 8859 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 ∈ ( 𝑆m 𝑋) → 𝑓:𝑋 𝑆)
109 ffn 6716 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓:𝑋 𝑆𝑓 Fn 𝑋)
110107, 108, 1093syl 18 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑓 Fn 𝑋)
111 simplrl 776 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑘𝑋)
112 fnsnfv 6971 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 Fn 𝑋𝑘𝑋) → {(𝑓𝑘)} = (𝑓 “ {𝑘}))
113110, 111, 112syl2anc 583 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → {(𝑓𝑘)} = (𝑓 “ {𝑘}))
114113sseq1d 4009 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ({(𝑓𝑘)} ⊆ 𝑢 ↔ (𝑓 “ {𝑘}) ⊆ 𝑢))
115106, 114bitrid 283 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ((𝑓𝑘) ∈ 𝑢 ↔ (𝑓 “ {𝑘}) ⊆ 𝑢))
116105, 115bitrd 279 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → (((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) ∈ 𝑢 ↔ (𝑓 “ {𝑘}) ⊆ 𝑢))
117116pm5.32da 578 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → ((𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) ∈ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)))
118100, 117bitrd 279 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑓 ∈ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)))
119118eqabdv 2862 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢) = {𝑓 ∣ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)})
120 df-rab 3428 . . . . . . . . . . . . . . 15 {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢} = {𝑓 ∣ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)}
121119, 120eqtr4di 2785 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢) = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢})
12293, 121eqtrd 2767 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢})
123 simpll 766 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → 𝑅 ∈ Top)
12411adantr 480 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → 𝑆 ∈ Top)
125 simprl 770 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → 𝑘𝑋)
126125snssd 4808 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → {𝑘} ⊆ 𝑋)
1272toptopon 22806 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘𝑋))
128123, 127sylib 217 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → 𝑅 ∈ (TopOn‘𝑋))
129 restsn2 23062 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑘𝑋) → (𝑅t {𝑘}) = 𝒫 {𝑘})
130128, 125, 129syl2anc 583 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑅t {𝑘}) = 𝒫 {𝑘})
131 snfi 9060 . . . . . . . . . . . . . . . 16 {𝑘} ∈ Fin
132 discmp 23289 . . . . . . . . . . . . . . . 16 ({𝑘} ∈ Fin ↔ 𝒫 {𝑘} ∈ Comp)
133131, 132mpbi 229 . . . . . . . . . . . . . . 15 𝒫 {𝑘} ∈ Comp
134130, 133eqeltrdi 2836 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑅t {𝑘}) ∈ Comp)
135 simprr 772 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → 𝑢𝑆)
1362, 123, 124, 126, 134, 135xkoopn 23480 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢} ∈ (𝑆ko 𝑅))
137122, 136eqeltrd 2828 . . . . . . . . . . . 12 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅))
138 ineq1 4201 . . . . . . . . . . . . 13 (𝑥 = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) = (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)))
139138eleq1d 2813 . . . . . . . . . . . 12 (𝑥 = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) → ((𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅) ↔ (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅)))
140137, 139syl5ibrcom 246 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑥 = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅)))
141140rexlimdvva 3206 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∃𝑘𝑋𝑢𝑆 𝑥 = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅)))
142141imp 406 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ ∃𝑘𝑋𝑢𝑆 𝑥 = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅))
14387, 142sylan2b 593 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅))
14484, 143jaodan 956 . . . . . . 7 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑥 ∈ {( 𝑆m 𝑋)} ∨ 𝑥 ∈ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅))
14565, 144sylan2b 593 . . . . . 6 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅))
146145fmpttd 7119 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))):({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))⟶(𝑆ko 𝑅))
147146frnd 6724 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑥 ∈ ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))) ⊆ (𝑆ko 𝑅))
14864, 147eqsstrd 4016 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) ⊆ (𝑆ko 𝑅))
149 tgfiss 22881 . . 3 (((𝑆ko 𝑅) ∈ Top ∧ (({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) ⊆ (𝑆ko 𝑅)) → (topGen‘(fi‘(({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) ⊆ (𝑆ko 𝑅))
15055, 148, 149syl2anc 583 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (topGen‘(fi‘(({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) ⊆ (𝑆ko 𝑅))
15154, 150eqsstrd 4016 1 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽t (𝑅 Cn 𝑆)) ⊆ (𝑆ko 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  wo 846  w3a 1085   = wceq 1534  wex 1774  wcel 2099  {cab 2704  wral 3056  wrex 3065  {crab 3427  Vcvv 3469  cdif 3941  cun 3942  cin 3943  wss 3944  𝒫 cpw 4598  {csn 4624   cuni 4903  cmpt 5225   × cxp 5670  ccnv 5671  ran crn 5673  cres 5674  cima 5675   Fn wfn 6537  wf 6538  cfv 6542  (class class class)co 7414  cmpo 7416  m cmap 8836  Xcixp 8907  Fincfn 8955  ficfi 9425  t crest 17393  topGenctg 17410  tcpt 17411  Topctop 22782  TopOnctopon 22799   Cn ccn 23115  Compccmp 23277  ko cxko 23452
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 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-1st 7987  df-2nd 7988  df-1o 8480  df-er 8718  df-map 8838  df-ixp 8908  df-en 8956  df-dom 8957  df-fin 8959  df-fi 9426  df-rest 17395  df-topgen 17416  df-pt 17417  df-top 22783  df-topon 22800  df-bases 22836  df-cn 23118  df-cmp 23278  df-xko 23454
This theorem is referenced by:  xkopt  23546  xkopjcn  23547
  Copyright terms: Public domain W3C validator