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

Theorem xkoptsub 22190
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 21442 . . . . . . . 8 (𝑅 ∈ Top → 𝑋𝑅)
43adantr 481 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑋𝑅)
5 fconstg 6559 . . . . . . . . 9 (𝑆 ∈ Top → (𝑋 × {𝑆}):𝑋⟶{𝑆})
65adantl 482 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}):𝑋⟶{𝑆})
76ffnd 6508 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}) Fn 𝑋)
8 eqid 2818 . . . . . . . 8 {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))}
98ptval 22106 . . . . . . 7 ((𝑋𝑅 ∧ (𝑋 × {𝑆}) Fn 𝑋) → (∏t‘(𝑋 × {𝑆})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))}))
104, 7, 9syl2anc 584 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∏t‘(𝑋 × {𝑆})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))}))
11 simpr 485 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑆 ∈ Top)
1211snssd 4734 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑆} ⊆ Top)
136, 12fssd 6521 . . . . . . . . 9 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}):𝑋⟶Top)
14 eqid 2818 . . . . . . . . . 10 X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) = X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛)
158, 14ptbasfi 22117 . . . . . . . . 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 6956 . . . . . . . . . . . . . . 15 ((𝑆 ∈ Top ∧ 𝑛𝑋) → ((𝑋 × {𝑆})‘𝑛) = 𝑆)
1817adantll 710 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛𝑋) → ((𝑋 × {𝑆})‘𝑛) = 𝑆)
1918unieqd 4840 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛𝑋) → ((𝑋 × {𝑆})‘𝑛) = 𝑆)
2019ixpeq2dva 8464 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) = X𝑛𝑋 𝑆)
21 eqid 2818 . . . . . . . . . . . . . 14 𝑆 = 𝑆
2221topopn 21442 . . . . . . . . . . . . 13 (𝑆 ∈ Top → 𝑆𝑆)
23 ixpconstg 8458 . . . . . . . . . . . . 13 ((𝑋𝑅 𝑆𝑆) → X𝑛𝑋 𝑆 = ( 𝑆m 𝑋))
243, 22, 23syl2an 595 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛𝑋 𝑆 = ( 𝑆m 𝑋))
2520, 24eqtrd 2853 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) = ( 𝑆m 𝑋))
2625sneqd 4569 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛)} = {( 𝑆m 𝑋)})
27 eqid 2818 . . . . . . . . . . . 12 𝑋 = 𝑋
28 fvconst2g 6956 . . . . . . . . . . . . . . 15 ((𝑆 ∈ Top ∧ 𝑘𝑋) → ((𝑋 × {𝑆})‘𝑘) = 𝑆)
2928adantll 710 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → ((𝑋 × {𝑆})‘𝑘) = 𝑆)
3025adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) = ( 𝑆m 𝑋))
3130mpteq1d 5146 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → (𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) = (𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)))
3231cnveqd 5739 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → (𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) = (𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)))
3332imaeq1d 5921 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))
3433ralrimivw 3180 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))
3529, 34jca 512 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))
3635ralrimiva 3179 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∀𝑘𝑋 (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))
37 mpoeq123 7215 . . . . . . . . . . . 12 ((𝑋 = 𝑋 ∧ ∀𝑘𝑋 (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) → (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢)) = (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))
3827, 36, 37sylancr 587 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢)) = (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))
3938rneqd 5801 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢)) = ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))
4026, 39uneq12d 4137 . . . . . . . . 9 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ({X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢))) = ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))
4140fveq2d 6667 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (fi‘({X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢)))) = (fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))))
4216, 41eqtrd 2853 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))} = (fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))))
4342fveq2d 6667 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))}) = (topGen‘(fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))))
4410, 43eqtrd 2853 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∏t‘(𝑋 × {𝑆})) = (topGen‘(fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))))
451, 44syl5eq 2865 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝐽 = (topGen‘(fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))))
4645oveq1d 7160 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽t (𝑅 Cn 𝑆)) = ((topGen‘(fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆)))
47 firest 16694 . . . . 5 (fi‘(({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆))) = ((fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆))
4847fveq2i 6666 . . . 4 (topGen‘(fi‘(({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) = (topGen‘((fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆)))
49 fvex 6676 . . . . 5 (fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) ∈ V
50 ovex 7178 . . . . 5 (𝑅 Cn 𝑆) ∈ V
51 tgrest 21695 . . . . 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 688 . . . 4 (topGen‘((fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆))) = ((topGen‘(fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆))
5348, 52eqtri 2841 . . 3 (topGen‘(fi‘(({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) = ((topGen‘(fi‘({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆))
5446, 53syl6eqr 2871 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽t (𝑅 Cn 𝑆)) = (topGen‘(fi‘(({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))))
55 xkotop 22124 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆ko 𝑅) ∈ Top)
56 snex 5322 . . . . . 6 {( 𝑆m 𝑋)} ∈ V
57 mpoexga 7764 . . . . . . . 8 ((𝑋𝑅𝑆 ∈ Top) → (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V)
583, 57sylan 580 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V)
59 rnexg 7603 . . . . . . 7 ((𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V → ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V)
6058, 59syl 17 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V)
61 unexg 7461 . . . . . 6 (({( 𝑆m 𝑋)} ∈ V ∧ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V) → ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
6256, 60, 61sylancr 587 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
63 restval 16688 . . . . 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 4122 . . . . . . 7 (𝑥 ∈ ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↔ (𝑥 ∈ {( 𝑆m 𝑋)} ∨ 𝑥 ∈ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))
662, 21cnf 21782 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝑅 Cn 𝑆) → 𝑥:𝑋 𝑆)
67 elmapg 8408 . . . . . . . . . . . . . . 15 (( 𝑆𝑆𝑋𝑅) → (𝑥 ∈ ( 𝑆m 𝑋) ↔ 𝑥:𝑋 𝑆))
6822, 3, 67syl2anr 596 . . . . . . . . . . . . . 14 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ ( 𝑆m 𝑋) ↔ 𝑥:𝑋 𝑆))
6966, 68syl5ibr 247 . . . . . . . . . . . . 13 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ (𝑅 Cn 𝑆) → 𝑥 ∈ ( 𝑆m 𝑋)))
7069ssrdv 3970 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) ⊆ ( 𝑆m 𝑋))
7170adantr 481 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆m 𝑋)}) → (𝑅 Cn 𝑆) ⊆ ( 𝑆m 𝑋))
72 elsni 4574 . . . . . . . . . . . 12 (𝑥 ∈ {( 𝑆m 𝑋)} → 𝑥 = ( 𝑆m 𝑋))
7372adantl 482 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆m 𝑋)}) → 𝑥 = ( 𝑆m 𝑋))
7471, 73sseqtrrd 4005 . . . . . . . . . 10 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆m 𝑋)}) → (𝑅 Cn 𝑆) ⊆ 𝑥)
75 sseqin2 4189 . . . . . . . . . 10 ((𝑅 Cn 𝑆) ⊆ 𝑥 ↔ (𝑥 ∩ (𝑅 Cn 𝑆)) = (𝑅 Cn 𝑆))
7674, 75sylib 219 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆m 𝑋)}) → (𝑥 ∩ (𝑅 Cn 𝑆)) = (𝑅 Cn 𝑆))
77 eqid 2818 . . . . . . . . . . . 12 (𝑆ko 𝑅) = (𝑆ko 𝑅)
7877xkouni 22135 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) = (𝑆ko 𝑅))
79 eqid 2818 . . . . . . . . . . . . 13 (𝑆ko 𝑅) = (𝑆ko 𝑅)
8079topopn 21442 . . . . . . . . . . . 12 ((𝑆ko 𝑅) ∈ Top → (𝑆ko 𝑅) ∈ (𝑆ko 𝑅))
8155, 80syl 17 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆ko 𝑅) ∈ (𝑆ko 𝑅))
8278, 81eqeltrd 2910 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) ∈ (𝑆ko 𝑅))
8382adantr 481 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆m 𝑋)}) → (𝑅 Cn 𝑆) ∈ (𝑆ko 𝑅))
8476, 83eqeltrd 2910 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆m 𝑋)}) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅))
85 eqid 2818 . . . . . . . . . . 11 (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) = (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))
8685rnmpo 7273 . . . . . . . . . 10 ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) = {𝑥 ∣ ∃𝑘𝑋𝑢𝑆 𝑥 = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)}
8786abeq2i 2945 . . . . . . . . 9 (𝑥 ∈ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ↔ ∃𝑘𝑋𝑢𝑆 𝑥 = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))
88 cnvresima 6080 . . . . . . . . . . . . . . 15 (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) ↾ (𝑅 Cn 𝑆)) “ 𝑢) = (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆))
8970adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑅 Cn 𝑆) ⊆ ( 𝑆m 𝑋))
9089resmptd 5901 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) ↾ (𝑅 Cn 𝑆)) = (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)))
9190cnveqd 5739 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) ↾ (𝑅 Cn 𝑆)) = (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)))
9291imaeq1d 5921 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) ↾ (𝑅 Cn 𝑆)) “ 𝑢) = ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢))
9388, 92syl5eqr 2867 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) = ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢))
94 fvex 6676 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝑘) ∈ V
9594rgenw 3147 . . . . . . . . . . . . . . . . . . 19 𝑤 ∈ (𝑅 Cn 𝑆)(𝑤𝑘) ∈ V
96 eqid 2818 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) = (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))
9796fnmpt 6481 . . . . . . . . . . . . . . . . . . 19 (∀𝑤 ∈ (𝑅 Cn 𝑆)(𝑤𝑘) ∈ V → (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) Fn (𝑅 Cn 𝑆))
9895, 97mp1i 13 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) Fn (𝑅 Cn 𝑆))
99 elpreima 6820 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) Fn (𝑅 Cn 𝑆) → (𝑓 ∈ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) ∈ 𝑢)))
10098, 99syl 17 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑓 ∈ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) ∈ 𝑢)))
101 fveq1 6662 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑓 → (𝑤𝑘) = (𝑓𝑘))
102 fvex 6676 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓𝑘) ∈ V
103101, 96, 102fvmpt 6761 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ (𝑅 Cn 𝑆) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) = (𝑓𝑘))
104103adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) = (𝑓𝑘))
105104eleq1d 2894 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → (((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) ∈ 𝑢 ↔ (𝑓𝑘) ∈ 𝑢))
106102snss 4710 . . . . . . . . . . . . . . . . . . . 20 ((𝑓𝑘) ∈ 𝑢 ↔ {(𝑓𝑘)} ⊆ 𝑢)
10789sselda 3964 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑓 ∈ ( 𝑆m 𝑋))
108 elmapi 8417 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 ∈ ( 𝑆m 𝑋) → 𝑓:𝑋 𝑆)
109 ffn 6507 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓:𝑋 𝑆𝑓 Fn 𝑋)
110107, 108, 1093syl 18 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑓 Fn 𝑋)
111 simplrl 773 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑘𝑋)
112 fnsnfv 6736 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 Fn 𝑋𝑘𝑋) → {(𝑓𝑘)} = (𝑓 “ {𝑘}))
113110, 111, 112syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → {(𝑓𝑘)} = (𝑓 “ {𝑘}))
114113sseq1d 3995 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ({(𝑓𝑘)} ⊆ 𝑢 ↔ (𝑓 “ {𝑘}) ⊆ 𝑢))
115106, 114syl5bb 284 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ((𝑓𝑘) ∈ 𝑢 ↔ (𝑓 “ {𝑘}) ⊆ 𝑢))
116105, 115bitrd 280 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → (((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) ∈ 𝑢 ↔ (𝑓 “ {𝑘}) ⊆ 𝑢))
117116pm5.32da 579 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → ((𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) ∈ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)))
118100, 117bitrd 280 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑓 ∈ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)))
119118abbi2dv 2947 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢) = {𝑓 ∣ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)})
120 df-rab 3144 . . . . . . . . . . . . . . 15 {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢} = {𝑓 ∣ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)}
121119, 120syl6eqr 2871 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢) = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢})
12293, 121eqtrd 2853 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢})
123 simpll 763 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → 𝑅 ∈ Top)
12411adantr 481 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → 𝑆 ∈ Top)
125 simprl 767 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → 𝑘𝑋)
126125snssd 4734 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → {𝑘} ⊆ 𝑋)
1272toptopon 21453 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘𝑋))
128123, 127sylib 219 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → 𝑅 ∈ (TopOn‘𝑋))
129 restsn2 21707 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑘𝑋) → (𝑅t {𝑘}) = 𝒫 {𝑘})
130128, 125, 129syl2anc 584 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑅t {𝑘}) = 𝒫 {𝑘})
131 snfi 8582 . . . . . . . . . . . . . . . 16 {𝑘} ∈ Fin
132 discmp 21934 . . . . . . . . . . . . . . . 16 ({𝑘} ∈ Fin ↔ 𝒫 {𝑘} ∈ Comp)
133131, 132mpbi 231 . . . . . . . . . . . . . . 15 𝒫 {𝑘} ∈ Comp
134130, 133syl6eqel 2918 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑅t {𝑘}) ∈ Comp)
135 simprr 769 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → 𝑢𝑆)
1362, 123, 124, 126, 134, 135xkoopn 22125 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢} ∈ (𝑆ko 𝑅))
137122, 136eqeltrd 2910 . . . . . . . . . . . 12 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅))
138 ineq1 4178 . . . . . . . . . . . . 13 (𝑥 = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) = (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)))
139138eleq1d 2894 . . . . . . . . . . . 12 (𝑥 = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) → ((𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅) ↔ (((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅)))
140137, 139syl5ibrcom 248 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑥 = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅)))
141140rexlimdvva 3291 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∃𝑘𝑋𝑢𝑆 𝑥 = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅)))
142141imp 407 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ ∃𝑘𝑋𝑢𝑆 𝑥 = ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅))
14387, 142sylan2b 593 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅))
14484, 143jaodan 951 . . . . . . 7 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑥 ∈ {( 𝑆m 𝑋)} ∨ 𝑥 ∈ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅))
14565, 144sylan2b 593 . . . . . 6 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆ko 𝑅))
146145fmpttd 6871 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))):({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))⟶(𝑆ko 𝑅))
147146frnd 6514 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑥 ∈ ({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))) ⊆ (𝑆ko 𝑅))
14864, 147eqsstrd 4002 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (({( 𝑆m 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆m 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) ⊆ (𝑆ko 𝑅))
149 tgfiss 21527 . . 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 4002 1 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽t (𝑅 Cn 𝑆)) ⊆ (𝑆ko 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wo 841  w3a 1079   = wceq 1528  wex 1771  wcel 2105  {cab 2796  wral 3135  wrex 3136  {crab 3139  Vcvv 3492  cdif 3930  cun 3931  cin 3932  wss 3933  𝒫 cpw 4535  {csn 4557   cuni 4830  cmpt 5137   × cxp 5546  ccnv 5547  ran crn 5549  cres 5550  cima 5551   Fn wfn 6343  wf 6344  cfv 6348  (class class class)co 7145  cmpo 7147  m cmap 8395  Xcixp 8449  Fincfn 8497  ficfi 8862  t crest 16682  topGenctg 16699  tcpt 16700  Topctop 21429  TopOnctopon 21446   Cn ccn 21760  Compccmp 21922  ko cxko 22097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-2o 8092  df-oadd 8095  df-er 8278  df-map 8397  df-ixp 8450  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-fi 8863  df-rest 16684  df-topgen 16705  df-pt 16706  df-top 21430  df-topon 21447  df-bases 21482  df-cn 21763  df-cmp 21923  df-xko 22099
This theorem is referenced by:  xkopt  22191  xkopjcn  22192
  Copyright terms: Public domain W3C validator