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

Theorem xkoptsub 21737
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 20990 . . . . . . . 8 (𝑅 ∈ Top → 𝑋𝑅)
43adantr 472 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑋𝑅)
5 fconstg 6274 . . . . . . . . 9 (𝑆 ∈ Top → (𝑋 × {𝑆}):𝑋⟶{𝑆})
65adantl 473 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}):𝑋⟶{𝑆})
76ffnd 6224 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}) Fn 𝑋)
8 eqid 2765 . . . . . . . 8 {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))}
98ptval 21653 . . . . . . 7 ((𝑋𝑅 ∧ (𝑋 × {𝑆}) Fn 𝑋) → (∏t‘(𝑋 × {𝑆})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))}))
104, 7, 9syl2anc 579 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∏t‘(𝑋 × {𝑆})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))}))
11 simpr 477 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑆 ∈ Top)
1211snssd 4494 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑆} ⊆ Top)
136, 12fssd 6237 . . . . . . . . 9 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}):𝑋⟶Top)
14 eqid 2765 . . . . . . . . . 10 X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) = X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛)
158, 14ptbasfi 21664 . . . . . . . . 9 ((𝑋𝑅 ∧ (𝑋 × {𝑆}):𝑋⟶Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))} = (fi‘({X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢)))))
164, 13, 15syl2anc 579 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))} = (fi‘({X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢)))))
17 fvconst2g 6660 . . . . . . . . . . . . . . 15 ((𝑆 ∈ Top ∧ 𝑛𝑋) → ((𝑋 × {𝑆})‘𝑛) = 𝑆)
1817adantll 705 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛𝑋) → ((𝑋 × {𝑆})‘𝑛) = 𝑆)
1918unieqd 4604 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛𝑋) → ((𝑋 × {𝑆})‘𝑛) = 𝑆)
2019ixpeq2dva 8128 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) = X𝑛𝑋 𝑆)
21 eqid 2765 . . . . . . . . . . . . . 14 𝑆 = 𝑆
2221topopn 20990 . . . . . . . . . . . . 13 (𝑆 ∈ Top → 𝑆𝑆)
23 ixpconstg 8122 . . . . . . . . . . . . 13 ((𝑋𝑅 𝑆𝑆) → X𝑛𝑋 𝑆 = ( 𝑆𝑚 𝑋))
243, 22, 23syl2an 589 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛𝑋 𝑆 = ( 𝑆𝑚 𝑋))
2520, 24eqtrd 2799 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) = ( 𝑆𝑚 𝑋))
2625sneqd 4346 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛)} = {( 𝑆𝑚 𝑋)})
27 eqid 2765 . . . . . . . . . . . 12 𝑋 = 𝑋
28 fvconst2g 6660 . . . . . . . . . . . . . . 15 ((𝑆 ∈ Top ∧ 𝑘𝑋) → ((𝑋 × {𝑆})‘𝑘) = 𝑆)
2928adantll 705 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → ((𝑋 × {𝑆})‘𝑘) = 𝑆)
3025adantr 472 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) = ( 𝑆𝑚 𝑋))
3130mpteq1d 4897 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → (𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) = (𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)))
3231cnveqd 5466 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → (𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) = (𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)))
3332imaeq1d 5647 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))
3433ralrimivw 3114 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))
3529, 34jca 507 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘𝑋) → (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))
3635ralrimiva 3113 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∀𝑘𝑋 (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))
37 mpt2eq123 6912 . . . . . . . . . . . 12 ((𝑋 = 𝑋 ∧ ∀𝑘𝑋 (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) → (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢)) = (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))
3827, 36, 37sylancr 581 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢)) = (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))
3938rneqd 5521 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢)) = ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))
4026, 39uneq12d 3930 . . . . . . . . 9 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ({X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢))) = ({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))
4140fveq2d 6379 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (fi‘({X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ ((𝑤X𝑛𝑋 ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤𝑘)) “ 𝑢)))) = (fi‘({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))))
4216, 41eqtrd 2799 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))} = (fi‘({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))))
4342fveq2d 6379 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦𝑋 (𝑔𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋𝑧)(𝑔𝑦) = ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦𝑋 (𝑔𝑦))}) = (topGen‘(fi‘({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))))
4410, 43eqtrd 2799 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∏t‘(𝑋 × {𝑆})) = (topGen‘(fi‘({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))))
451, 44syl5eq 2811 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝐽 = (topGen‘(fi‘({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))))
4645oveq1d 6857 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽t (𝑅 Cn 𝑆)) = ((topGen‘(fi‘({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆)))
47 firest 16361 . . . . 5 (fi‘(({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆))) = ((fi‘({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆))
4847fveq2i 6378 . . . 4 (topGen‘(fi‘(({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) = (topGen‘((fi‘({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆)))
49 fvex 6388 . . . . 5 (fi‘({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) ∈ V
50 ovex 6874 . . . . 5 (𝑅 Cn 𝑆) ∈ V
51 tgrest 21243 . . . . 5 (((fi‘({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) ∈ V ∧ (𝑅 Cn 𝑆) ∈ V) → (topGen‘((fi‘({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆))) = ((topGen‘(fi‘({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆)))
5249, 50, 51mp2an 683 . . . 4 (topGen‘((fi‘({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆))) = ((topGen‘(fi‘({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆))
5348, 52eqtri 2787 . . 3 (topGen‘(fi‘(({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) = ((topGen‘(fi‘({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆))
5446, 53syl6eqr 2817 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽t (𝑅 Cn 𝑆)) = (topGen‘(fi‘(({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))))
55 xkotop 21671 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ^ko 𝑅) ∈ Top)
56 snex 5064 . . . . . 6 {( 𝑆𝑚 𝑋)} ∈ V
57 mpt2exga 7447 . . . . . . . 8 ((𝑋𝑅𝑆 ∈ Top) → (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V)
583, 57sylan 575 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V)
59 rnexg 7296 . . . . . . 7 ((𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V → ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V)
6058, 59syl 17 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V)
61 unexg 7157 . . . . . 6 (({( 𝑆𝑚 𝑋)} ∈ V ∧ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ∈ V) → ({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
6256, 60, 61sylancr 581 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
63 restval 16355 . . . . 5 ((({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ∈ V ∧ (𝑅 Cn 𝑆) ∈ V) → (({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) = ran (𝑥 ∈ ({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))))
6462, 50, 63sylancl 580 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) = ran (𝑥 ∈ ({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))))
65 elun 3915 . . . . . . 7 (𝑥 ∈ ({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↔ (𝑥 ∈ {( 𝑆𝑚 𝑋)} ∨ 𝑥 ∈ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))))
662, 21cnf 21330 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝑅 Cn 𝑆) → 𝑥:𝑋 𝑆)
67 elmapg 8073 . . . . . . . . . . . . . . 15 (( 𝑆𝑆𝑋𝑅) → (𝑥 ∈ ( 𝑆𝑚 𝑋) ↔ 𝑥:𝑋 𝑆))
6822, 3, 67syl2anr 590 . . . . . . . . . . . . . 14 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ ( 𝑆𝑚 𝑋) ↔ 𝑥:𝑋 𝑆))
6966, 68syl5ibr 237 . . . . . . . . . . . . 13 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ (𝑅 Cn 𝑆) → 𝑥 ∈ ( 𝑆𝑚 𝑋)))
7069ssrdv 3767 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) ⊆ ( 𝑆𝑚 𝑋))
7170adantr 472 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆𝑚 𝑋)}) → (𝑅 Cn 𝑆) ⊆ ( 𝑆𝑚 𝑋))
72 elsni 4351 . . . . . . . . . . . 12 (𝑥 ∈ {( 𝑆𝑚 𝑋)} → 𝑥 = ( 𝑆𝑚 𝑋))
7372adantl 473 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆𝑚 𝑋)}) → 𝑥 = ( 𝑆𝑚 𝑋))
7471, 73sseqtr4d 3802 . . . . . . . . . 10 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆𝑚 𝑋)}) → (𝑅 Cn 𝑆) ⊆ 𝑥)
75 sseqin2 3979 . . . . . . . . . 10 ((𝑅 Cn 𝑆) ⊆ 𝑥 ↔ (𝑥 ∩ (𝑅 Cn 𝑆)) = (𝑅 Cn 𝑆))
7674, 75sylib 209 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆𝑚 𝑋)}) → (𝑥 ∩ (𝑅 Cn 𝑆)) = (𝑅 Cn 𝑆))
77 eqid 2765 . . . . . . . . . . . 12 (𝑆 ^ko 𝑅) = (𝑆 ^ko 𝑅)
7877xkouni 21682 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) = (𝑆 ^ko 𝑅))
79 eqid 2765 . . . . . . . . . . . . 13 (𝑆 ^ko 𝑅) = (𝑆 ^ko 𝑅)
8079topopn 20990 . . . . . . . . . . . 12 ((𝑆 ^ko 𝑅) ∈ Top → (𝑆 ^ko 𝑅) ∈ (𝑆 ^ko 𝑅))
8155, 80syl 17 . . . . . . . . . . 11 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ^ko 𝑅) ∈ (𝑆 ^ko 𝑅))
8278, 81eqeltrd 2844 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) ∈ (𝑆 ^ko 𝑅))
8382adantr 472 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆𝑚 𝑋)}) → (𝑅 Cn 𝑆) ∈ (𝑆 ^ko 𝑅))
8476, 83eqeltrd 2844 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {( 𝑆𝑚 𝑋)}) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ^ko 𝑅))
85 eqid 2765 . . . . . . . . . . 11 (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) = (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))
8685rnmpt2 6968 . . . . . . . . . 10 ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) = {𝑥 ∣ ∃𝑘𝑋𝑢𝑆 𝑥 = ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)}
8786abeq2i 2878 . . . . . . . . 9 (𝑥 ∈ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) ↔ ∃𝑘𝑋𝑢𝑆 𝑥 = ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))
88 cnvresima 5809 . . . . . . . . . . . . . . 15 (((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) ↾ (𝑅 Cn 𝑆)) “ 𝑢) = (((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆))
8970adantr 472 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑅 Cn 𝑆) ⊆ ( 𝑆𝑚 𝑋))
9089resmptd 5629 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) ↾ (𝑅 Cn 𝑆)) = (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)))
9190cnveqd 5466 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) ↾ (𝑅 Cn 𝑆)) = (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)))
9291imaeq1d 5647 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) ↾ (𝑅 Cn 𝑆)) “ 𝑢) = ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢))
9388, 92syl5eqr 2813 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) = ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢))
94 fvex 6388 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝑘) ∈ V
9594rgenw 3071 . . . . . . . . . . . . . . . . . . 19 𝑤 ∈ (𝑅 Cn 𝑆)(𝑤𝑘) ∈ V
96 eqid 2765 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) = (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))
9796fnmpt 6198 . . . . . . . . . . . . . . . . . . 19 (∀𝑤 ∈ (𝑅 Cn 𝑆)(𝑤𝑘) ∈ V → (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) Fn (𝑅 Cn 𝑆))
9895, 97mp1i 13 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) Fn (𝑅 Cn 𝑆))
99 elpreima 6527 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) Fn (𝑅 Cn 𝑆) → (𝑓 ∈ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) ∈ 𝑢)))
10098, 99syl 17 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑓 ∈ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) ∈ 𝑢)))
101 fveq1 6374 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑓 → (𝑤𝑘) = (𝑓𝑘))
102 fvex 6388 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓𝑘) ∈ V
103101, 96, 102fvmpt 6471 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ (𝑅 Cn 𝑆) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) = (𝑓𝑘))
104103adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) = (𝑓𝑘))
105104eleq1d 2829 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → (((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) ∈ 𝑢 ↔ (𝑓𝑘) ∈ 𝑢))
106102snss 4470 . . . . . . . . . . . . . . . . . . . 20 ((𝑓𝑘) ∈ 𝑢 ↔ {(𝑓𝑘)} ⊆ 𝑢)
10789sselda 3761 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑓 ∈ ( 𝑆𝑚 𝑋))
108 elmapi 8082 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 ∈ ( 𝑆𝑚 𝑋) → 𝑓:𝑋 𝑆)
109 ffn 6223 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓:𝑋 𝑆𝑓 Fn 𝑋)
110107, 108, 1093syl 18 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑓 Fn 𝑋)
111 simplrl 795 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑘𝑋)
112 fnsnfv 6447 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 Fn 𝑋𝑘𝑋) → {(𝑓𝑘)} = (𝑓 “ {𝑘}))
113110, 111, 112syl2anc 579 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → {(𝑓𝑘)} = (𝑓 “ {𝑘}))
114113sseq1d 3792 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ({(𝑓𝑘)} ⊆ 𝑢 ↔ (𝑓 “ {𝑘}) ⊆ 𝑢))
115106, 114syl5bb 274 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ((𝑓𝑘) ∈ 𝑢 ↔ (𝑓 “ {𝑘}) ⊆ 𝑢))
116105, 115bitrd 270 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → (((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) ∈ 𝑢 ↔ (𝑓 “ {𝑘}) ⊆ 𝑢))
117116pm5.32da 574 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → ((𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘))‘𝑓) ∈ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)))
118100, 117bitrd 270 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑓 ∈ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)))
119118abbi2dv 2885 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢) = {𝑓 ∣ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)})
120 df-rab 3064 . . . . . . . . . . . . . . 15 {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢} = {𝑓 ∣ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)}
121119, 120syl6eqr 2817 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤𝑘)) “ 𝑢) = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢})
12293, 121eqtrd 2799 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢})
123 simpll 783 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → 𝑅 ∈ Top)
12411adantr 472 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → 𝑆 ∈ Top)
125 simprl 787 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → 𝑘𝑋)
126125snssd 4494 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → {𝑘} ⊆ 𝑋)
1272toptopon 21001 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘𝑋))
128123, 127sylib 209 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → 𝑅 ∈ (TopOn‘𝑋))
129 restsn2 21255 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑘𝑋) → (𝑅t {𝑘}) = 𝒫 {𝑘})
130128, 125, 129syl2anc 579 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑅t {𝑘}) = 𝒫 {𝑘})
131 snfi 8245 . . . . . . . . . . . . . . . 16 {𝑘} ∈ Fin
132 discmp 21481 . . . . . . . . . . . . . . . 16 ({𝑘} ∈ Fin ↔ 𝒫 {𝑘} ∈ Comp)
133131, 132mpbi 221 . . . . . . . . . . . . . . 15 𝒫 {𝑘} ∈ Comp
134130, 133syl6eqel 2852 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑅t {𝑘}) ∈ Comp)
135 simprr 789 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → 𝑢𝑆)
1362, 123, 124, 126, 134, 135xkoopn 21672 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢} ∈ (𝑆 ^ko 𝑅))
137122, 136eqeltrd 2844 . . . . . . . . . . . 12 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ^ko 𝑅))
138 ineq1 3969 . . . . . . . . . . . . 13 (𝑥 = ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) = (((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)))
139138eleq1d 2829 . . . . . . . . . . . 12 (𝑥 = ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢) → ((𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ^ko 𝑅) ↔ (((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ^ko 𝑅)))
140137, 139syl5ibrcom 238 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘𝑋𝑢𝑆)) → (𝑥 = ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ^ko 𝑅)))
141140rexlimdvva 3185 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∃𝑘𝑋𝑢𝑆 𝑥 = ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ^ko 𝑅)))
142141imp 395 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ ∃𝑘𝑋𝑢𝑆 𝑥 = ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ^ko 𝑅))
14387, 142sylan2b 587 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ^ko 𝑅))
14484, 143jaodan 980 . . . . . . 7 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑥 ∈ {( 𝑆𝑚 𝑋)} ∨ 𝑥 ∈ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ^ko 𝑅))
14565, 144sylan2b 587 . . . . . 6 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ ({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ^ko 𝑅))
146145fmpttd 6575 . . . . 5 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ ({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))):({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢)))⟶(𝑆 ^ko 𝑅))
147146frnd 6230 . . . 4 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑥 ∈ ({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))) ⊆ (𝑆 ^ko 𝑅))
14864, 147eqsstrd 3799 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) ⊆ (𝑆 ^ko 𝑅))
149 tgfiss 21075 . . 3 (((𝑆 ^ko 𝑅) ∈ Top ∧ (({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) ⊆ (𝑆 ^ko 𝑅)) → (topGen‘(fi‘(({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) ⊆ (𝑆 ^ko 𝑅))
15055, 148, 149syl2anc 579 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (topGen‘(fi‘(({( 𝑆𝑚 𝑋)} ∪ ran (𝑘𝑋, 𝑢𝑆 ↦ ((𝑤 ∈ ( 𝑆𝑚 𝑋) ↦ (𝑤𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) ⊆ (𝑆 ^ko 𝑅))
15154, 150eqsstrd 3799 1 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽t (𝑅 Cn 𝑆)) ⊆ (𝑆 ^ko 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wo 873  w3a 1107   = wceq 1652  wex 1874  wcel 2155  {cab 2751  wral 3055  wrex 3056  {crab 3059  Vcvv 3350  cdif 3729  cun 3730  cin 3731  wss 3732  𝒫 cpw 4315  {csn 4334   cuni 4594  cmpt 4888   × cxp 5275  ccnv 5276  ran crn 5278  cres 5279  cima 5280   Fn wfn 6063  wf 6064  cfv 6068  (class class class)co 6842  cmpt2 6844  𝑚 cmap 8060  Xcixp 8113  Fincfn 8160  ficfi 8523  t crest 16349  topGenctg 16366  tcpt 16367  Topctop 20977  TopOnctopon 20994   Cn ccn 21308  Compccmp 21469   ^ko cxko 21644
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-map 8062  df-ixp 8114  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fi 8524  df-rest 16351  df-topgen 16372  df-pt 16373  df-top 20978  df-topon 20995  df-bases 21030  df-cn 21311  df-cmp 21470  df-xko 21646
This theorem is referenced by:  xkopt  21738  xkopjcn  21739
  Copyright terms: Public domain W3C validator