# Metamath Proof Explorer

## Theorem xkoinjcn

Description: Continuity of "injection", i.e. currying, as a function on continuous function spaces. (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Hypothesis xkoinjcn.3 ${⊢}{F}=\left({x}\in {X}⟼\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\right)$
Assertion xkoinjcn ${⊢}\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\to {F}\in \left({R}\mathrm{Cn}\left(\left({S}{×}_{t}{R}\right){^}_{\mathrm{ko}}{S}\right)\right)$

### Proof

Step Hyp Ref Expression
1 xkoinjcn.3 ${⊢}{F}=\left({x}\in {X}⟼\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\right)$
2 simplr ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {x}\in {X}\right)\to {S}\in \mathrm{TopOn}\left({Y}\right)$
3 2 cnmptid ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {x}\in {X}\right)\to \left({y}\in {Y}⟼{y}\right)\in \left({S}\mathrm{Cn}{S}\right)$
4 simpll ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {x}\in {X}\right)\to {R}\in \mathrm{TopOn}\left({X}\right)$
5 simpr ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {x}\in {X}\right)\to {x}\in {X}$
6 2 4 5 cnmptc ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {x}\in {X}\right)\to \left({y}\in {Y}⟼{x}\right)\in \left({S}\mathrm{Cn}{R}\right)$
7 2 3 6 cnmpt1t ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge {x}\in {X}\right)\to \left({y}\in {Y}⟼⟨{y},{x}⟩\right)\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)$
8 7 1 fmptd ${⊢}\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\to {F}:{X}⟶{S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)$
9 eqid ${⊢}\bigcup {S}=\bigcup {S}$
10 eqid ${⊢}\left\{{w}\in 𝒫\bigcup {S}|{S}{↾}_{𝑡}{w}\in \mathrm{Comp}\right\}=\left\{{w}\in 𝒫\bigcup {S}|{S}{↾}_{𝑡}{w}\in \mathrm{Comp}\right\}$
11 eqid ${⊢}\left({k}\in \left\{{w}\in 𝒫\bigcup {S}|{S}{↾}_{𝑡}{w}\in \mathrm{Comp}\right\},{v}\in \left({S}{×}_{t}{R}\right)⟼\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right)=\left({k}\in \left\{{w}\in 𝒫\bigcup {S}|{S}{↾}_{𝑡}{w}\in \mathrm{Comp}\right\},{v}\in \left({S}{×}_{t}{R}\right)⟼\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right)$
12 9 10 11 xkobval ${⊢}\mathrm{ran}\left({k}\in \left\{{w}\in 𝒫\bigcup {S}|{S}{↾}_{𝑡}{w}\in \mathrm{Comp}\right\},{v}\in \left({S}{×}_{t}{R}\right)⟼\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right)=\left\{{z}|\exists {k}\in 𝒫\bigcup {S}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left({S}{×}_{t}{R}\right)\phantom{\rule{.4em}{0ex}}\left({S}{↾}_{𝑡}{k}\in \mathrm{Comp}\wedge {z}=\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right)\right\}$
13 12 abeq2i ${⊢}{z}\in \mathrm{ran}\left({k}\in \left\{{w}\in 𝒫\bigcup {S}|{S}{↾}_{𝑡}{w}\in \mathrm{Comp}\right\},{v}\in \left({S}{×}_{t}{R}\right)⟼\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right)↔\exists {k}\in 𝒫\bigcup {S}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left({S}{×}_{t}{R}\right)\phantom{\rule{.4em}{0ex}}\left({S}{↾}_{𝑡}{k}\in \mathrm{Comp}\wedge {z}=\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right)$
14 simpll ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\to \left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)$
15 14 7 sylan ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge {x}\in {X}\right)\to \left({y}\in {Y}⟼⟨{y},{x}⟩\right)\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)$
16 imaeq1 ${⊢}{f}=\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\to {f}\left[{k}\right]=\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\left[{k}\right]$
17 16 sseq1d ${⊢}{f}=\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\to \left({f}\left[{k}\right]\subseteq {v}↔\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\left[{k}\right]\subseteq {v}\right)$
18 17 elrab3 ${⊢}\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)\to \left(\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\in \left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}↔\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\left[{k}\right]\subseteq {v}\right)$
19 15 18 syl ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge {x}\in {X}\right)\to \left(\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\in \left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}↔\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\left[{k}\right]\subseteq {v}\right)$
20 funmpt ${⊢}\mathrm{Fun}\left({y}\in {Y}⟼⟨{y},{x}⟩\right)$
21 simplrl ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\to {k}\in 𝒫\bigcup {S}$
22 21 elpwid ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\to {k}\subseteq \bigcup {S}$
23 14 simprd ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\to {S}\in \mathrm{TopOn}\left({Y}\right)$
24 toponuni ${⊢}{S}\in \mathrm{TopOn}\left({Y}\right)\to {Y}=\bigcup {S}$
25 23 24 syl ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\to {Y}=\bigcup {S}$
26 22 25 sseqtrrd ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\to {k}\subseteq {Y}$
27 26 adantr ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge {x}\in {X}\right)\to {k}\subseteq {Y}$
28 dmmptg ${⊢}\forall {y}\in {Y}\phantom{\rule{.4em}{0ex}}⟨{y},{x}⟩\in \mathrm{V}\to \mathrm{dom}\left({y}\in {Y}⟼⟨{y},{x}⟩\right)={Y}$
29 opex ${⊢}⟨{y},{x}⟩\in \mathrm{V}$
30 29 a1i ${⊢}{y}\in {Y}\to ⟨{y},{x}⟩\in \mathrm{V}$
31 28 30 mprg ${⊢}\mathrm{dom}\left({y}\in {Y}⟼⟨{y},{x}⟩\right)={Y}$
32 27 31 sseqtrrdi ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge {x}\in {X}\right)\to {k}\subseteq \mathrm{dom}\left({y}\in {Y}⟼⟨{y},{x}⟩\right)$
33 funimass4 ${⊢}\left(\mathrm{Fun}\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\wedge {k}\subseteq \mathrm{dom}\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\right)\to \left(\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\left[{k}\right]\subseteq {v}↔\forall {z}\in {k}\phantom{\rule{.4em}{0ex}}\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\left({z}\right)\in {v}\right)$
34 20 32 33 sylancr ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge {x}\in {X}\right)\to \left(\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\left[{k}\right]\subseteq {v}↔\forall {z}\in {k}\phantom{\rule{.4em}{0ex}}\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\left({z}\right)\in {v}\right)$
35 27 sselda ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge {x}\in {X}\right)\wedge {z}\in {k}\right)\to {z}\in {Y}$
36 opeq1 ${⊢}{y}={z}\to ⟨{y},{x}⟩=⟨{z},{x}⟩$
37 eqid ${⊢}\left({y}\in {Y}⟼⟨{y},{x}⟩\right)=\left({y}\in {Y}⟼⟨{y},{x}⟩\right)$
38 opex ${⊢}⟨{z},{x}⟩\in \mathrm{V}$
39 36 37 38 fvmpt ${⊢}{z}\in {Y}\to \left({y}\in {Y}⟼⟨{y},{x}⟩\right)\left({z}\right)=⟨{z},{x}⟩$
40 35 39 syl ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge {x}\in {X}\right)\wedge {z}\in {k}\right)\to \left({y}\in {Y}⟼⟨{y},{x}⟩\right)\left({z}\right)=⟨{z},{x}⟩$
41 40 eleq1d ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge {x}\in {X}\right)\wedge {z}\in {k}\right)\to \left(\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\left({z}\right)\in {v}↔⟨{z},{x}⟩\in {v}\right)$
42 vex ${⊢}{x}\in \mathrm{V}$
43 opeq2 ${⊢}{w}={x}\to ⟨{z},{w}⟩=⟨{z},{x}⟩$
44 43 eleq1d ${⊢}{w}={x}\to \left(⟨{z},{w}⟩\in {v}↔⟨{z},{x}⟩\in {v}\right)$
45 42 44 ralsn ${⊢}\forall {w}\in \left\{{x}\right\}\phantom{\rule{.4em}{0ex}}⟨{z},{w}⟩\in {v}↔⟨{z},{x}⟩\in {v}$
46 41 45 syl6bbr ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge {x}\in {X}\right)\wedge {z}\in {k}\right)\to \left(\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\left({z}\right)\in {v}↔\forall {w}\in \left\{{x}\right\}\phantom{\rule{.4em}{0ex}}⟨{z},{w}⟩\in {v}\right)$
47 46 ralbidva ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge {x}\in {X}\right)\to \left(\forall {z}\in {k}\phantom{\rule{.4em}{0ex}}\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\left({z}\right)\in {v}↔\forall {z}\in {k}\phantom{\rule{.4em}{0ex}}\forall {w}\in \left\{{x}\right\}\phantom{\rule{.4em}{0ex}}⟨{z},{w}⟩\in {v}\right)$
48 dfss3 ${⊢}{k}×\left\{{x}\right\}\subseteq {v}↔\forall {t}\in \left({k}×\left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{t}\in {v}$
49 eleq1 ${⊢}{t}=⟨{z},{w}⟩\to \left({t}\in {v}↔⟨{z},{w}⟩\in {v}\right)$
50 49 ralxp ${⊢}\forall {t}\in \left({k}×\left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{t}\in {v}↔\forall {z}\in {k}\phantom{\rule{.4em}{0ex}}\forall {w}\in \left\{{x}\right\}\phantom{\rule{.4em}{0ex}}⟨{z},{w}⟩\in {v}$
51 48 50 bitri ${⊢}{k}×\left\{{x}\right\}\subseteq {v}↔\forall {z}\in {k}\phantom{\rule{.4em}{0ex}}\forall {w}\in \left\{{x}\right\}\phantom{\rule{.4em}{0ex}}⟨{z},{w}⟩\in {v}$
52 47 51 syl6bbr ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge {x}\in {X}\right)\to \left(\forall {z}\in {k}\phantom{\rule{.4em}{0ex}}\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\left({z}\right)\in {v}↔{k}×\left\{{x}\right\}\subseteq {v}\right)$
53 19 34 52 3bitrd ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge {x}\in {X}\right)\to \left(\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\in \left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}↔{k}×\left\{{x}\right\}\subseteq {v}\right)$
54 53 rabbidva ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\to \left\{{x}\in {X}|\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\in \left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right\}=\left\{{x}\in {X}|{k}×\left\{{x}\right\}\subseteq {v}\right\}$
55 sneq ${⊢}{x}={w}\to \left\{{x}\right\}=\left\{{w}\right\}$
56 55 xpeq2d ${⊢}{x}={w}\to {k}×\left\{{x}\right\}={k}×\left\{{w}\right\}$
57 56 sseq1d ${⊢}{x}={w}\to \left({k}×\left\{{x}\right\}\subseteq {v}↔{k}×\left\{{w}\right\}\subseteq {v}\right)$
58 57 elrab ${⊢}{w}\in \left\{{x}\in {X}|{k}×\left\{{x}\right\}\subseteq {v}\right\}↔\left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)$
59 eqid ${⊢}\bigcup \left({S}{↾}_{𝑡}{k}\right)=\bigcup \left({S}{↾}_{𝑡}{k}\right)$
60 eqid ${⊢}\bigcup {R}=\bigcup {R}$
61 simplr ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {S}{↾}_{𝑡}{k}\in \mathrm{Comp}$
62 simpll ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\to {R}\in \mathrm{TopOn}\left({X}\right)$
63 62 ad2antrr ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {R}\in \mathrm{TopOn}\left({X}\right)$
64 topontop ${⊢}{R}\in \mathrm{TopOn}\left({X}\right)\to {R}\in \mathrm{Top}$
65 63 64 syl ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {R}\in \mathrm{Top}$
66 topontop ${⊢}{S}\in \mathrm{TopOn}\left({Y}\right)\to {S}\in \mathrm{Top}$
67 66 adantl ${⊢}\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\to {S}\in \mathrm{Top}$
68 64 adantr ${⊢}\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\to {R}\in \mathrm{Top}$
69 txtop ${⊢}\left({S}\in \mathrm{Top}\wedge {R}\in \mathrm{Top}\right)\to {S}{×}_{t}{R}\in \mathrm{Top}$
70 67 68 69 syl2anc ${⊢}\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\to {S}{×}_{t}{R}\in \mathrm{Top}$
71 70 ad3antrrr ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {S}{×}_{t}{R}\in \mathrm{Top}$
72 vex ${⊢}{k}\in \mathrm{V}$
73 toponmax ${⊢}{R}\in \mathrm{TopOn}\left({X}\right)\to {X}\in {R}$
74 63 73 syl ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {X}\in {R}$
75 xpexg ${⊢}\left({k}\in \mathrm{V}\wedge {X}\in {R}\right)\to {k}×{X}\in \mathrm{V}$
76 72 74 75 sylancr ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {k}×{X}\in \mathrm{V}$
77 simprr ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\to {v}\in \left({S}{×}_{t}{R}\right)$
78 77 ad2antrr ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {v}\in \left({S}{×}_{t}{R}\right)$
79 elrestr ${⊢}\left({S}{×}_{t}{R}\in \mathrm{Top}\wedge {k}×{X}\in \mathrm{V}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\to {v}\cap \left({k}×{X}\right)\in \left(\left({S}{×}_{t}{R}\right){↾}_{𝑡}\left({k}×{X}\right)\right)$
80 71 76 78 79 syl3anc ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {v}\cap \left({k}×{X}\right)\in \left(\left({S}{×}_{t}{R}\right){↾}_{𝑡}\left({k}×{X}\right)\right)$
81 67 ad3antrrr ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {S}\in \mathrm{Top}$
82 72 a1i ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {k}\in \mathrm{V}$
83 txrest ${⊢}\left(\left({S}\in \mathrm{Top}\wedge {R}\in \mathrm{Top}\right)\wedge \left({k}\in \mathrm{V}\wedge {X}\in {R}\right)\right)\to \left({S}{×}_{t}{R}\right){↾}_{𝑡}\left({k}×{X}\right)=\left({S}{↾}_{𝑡}{k}\right){×}_{t}\left({R}{↾}_{𝑡}{X}\right)$
84 81 65 82 74 83 syl22anc ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to \left({S}{×}_{t}{R}\right){↾}_{𝑡}\left({k}×{X}\right)=\left({S}{↾}_{𝑡}{k}\right){×}_{t}\left({R}{↾}_{𝑡}{X}\right)$
85 toponuni ${⊢}{R}\in \mathrm{TopOn}\left({X}\right)\to {X}=\bigcup {R}$
86 63 85 syl ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {X}=\bigcup {R}$
87 86 oveq2d ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {R}{↾}_{𝑡}{X}={R}{↾}_{𝑡}\bigcup {R}$
88 60 restid ${⊢}{R}\in \mathrm{TopOn}\left({X}\right)\to {R}{↾}_{𝑡}\bigcup {R}={R}$
89 63 88 syl ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {R}{↾}_{𝑡}\bigcup {R}={R}$
90 87 89 eqtrd ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {R}{↾}_{𝑡}{X}={R}$
91 90 oveq2d ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to \left({S}{↾}_{𝑡}{k}\right){×}_{t}\left({R}{↾}_{𝑡}{X}\right)=\left({S}{↾}_{𝑡}{k}\right){×}_{t}{R}$
92 84 91 eqtrd ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to \left({S}{×}_{t}{R}\right){↾}_{𝑡}\left({k}×{X}\right)=\left({S}{↾}_{𝑡}{k}\right){×}_{t}{R}$
93 80 92 eleqtrd ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {v}\cap \left({k}×{X}\right)\in \left(\left({S}{↾}_{𝑡}{k}\right){×}_{t}{R}\right)$
94 23 adantr ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {S}\in \mathrm{TopOn}\left({Y}\right)$
95 26 adantr ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {k}\subseteq {Y}$
96 resttopon ${⊢}\left({S}\in \mathrm{TopOn}\left({Y}\right)\wedge {k}\subseteq {Y}\right)\to {S}{↾}_{𝑡}{k}\in \mathrm{TopOn}\left({k}\right)$
97 94 95 96 syl2anc ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {S}{↾}_{𝑡}{k}\in \mathrm{TopOn}\left({k}\right)$
98 toponuni ${⊢}{S}{↾}_{𝑡}{k}\in \mathrm{TopOn}\left({k}\right)\to {k}=\bigcup \left({S}{↾}_{𝑡}{k}\right)$
99 97 98 syl ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {k}=\bigcup \left({S}{↾}_{𝑡}{k}\right)$
100 99 xpeq1d ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {k}×\left\{{w}\right\}=\bigcup \left({S}{↾}_{𝑡}{k}\right)×\left\{{w}\right\}$
101 simprr ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {k}×\left\{{w}\right\}\subseteq {v}$
102 simprl ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {w}\in {X}$
103 102 snssd ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to \left\{{w}\right\}\subseteq {X}$
104 xpss2 ${⊢}\left\{{w}\right\}\subseteq {X}\to {k}×\left\{{w}\right\}\subseteq {k}×{X}$
105 103 104 syl ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {k}×\left\{{w}\right\}\subseteq {k}×{X}$
106 101 105 ssind ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {k}×\left\{{w}\right\}\subseteq {v}\cap \left({k}×{X}\right)$
107 100 106 eqsstrrd ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to \bigcup \left({S}{↾}_{𝑡}{k}\right)×\left\{{w}\right\}\subseteq {v}\cap \left({k}×{X}\right)$
108 102 86 eleqtrd ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to {w}\in \bigcup {R}$
109 59 60 61 65 93 107 108 txtube ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to \exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({w}\in {r}\wedge \bigcup \left({S}{↾}_{𝑡}{k}\right)×{r}\subseteq {v}\cap \left({k}×{X}\right)\right)$
110 toponss ${⊢}\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {r}\in {R}\right)\to {r}\subseteq {X}$
111 63 110 sylan ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\wedge {r}\in {R}\right)\to {r}\subseteq {X}$
112 ssrab ${⊢}{r}\subseteq \left\{{x}\in {X}|{k}×\left\{{x}\right\}\subseteq {v}\right\}↔\left({r}\subseteq {X}\wedge \forall {x}\in {r}\phantom{\rule{.4em}{0ex}}{k}×\left\{{x}\right\}\subseteq {v}\right)$
113 112 baib ${⊢}{r}\subseteq {X}\to \left({r}\subseteq \left\{{x}\in {X}|{k}×\left\{{x}\right\}\subseteq {v}\right\}↔\forall {x}\in {r}\phantom{\rule{.4em}{0ex}}{k}×\left\{{x}\right\}\subseteq {v}\right)$
114 111 113 syl ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\wedge {r}\in {R}\right)\to \left({r}\subseteq \left\{{x}\in {X}|{k}×\left\{{x}\right\}\subseteq {v}\right\}↔\forall {x}\in {r}\phantom{\rule{.4em}{0ex}}{k}×\left\{{x}\right\}\subseteq {v}\right)$
115 xpss2 ${⊢}{r}\subseteq {X}\to {k}×{r}\subseteq {k}×{X}$
116 111 115 syl ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\wedge {r}\in {R}\right)\to {k}×{r}\subseteq {k}×{X}$
117 116 biantrud ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\wedge {r}\in {R}\right)\to \left({k}×{r}\subseteq {v}↔\left({k}×{r}\subseteq {v}\wedge {k}×{r}\subseteq {k}×{X}\right)\right)$
118 iunid ${⊢}\bigcup _{{x}\in {r}}\left\{{x}\right\}={r}$
119 118 xpeq2i ${⊢}{k}×\bigcup _{{x}\in {r}}\left\{{x}\right\}={k}×{r}$
120 xpiundi ${⊢}{k}×\bigcup _{{x}\in {r}}\left\{{x}\right\}=\bigcup _{{x}\in {r}}\left({k}×\left\{{x}\right\}\right)$
121 119 120 eqtr3i ${⊢}{k}×{r}=\bigcup _{{x}\in {r}}\left({k}×\left\{{x}\right\}\right)$
122 121 sseq1i ${⊢}{k}×{r}\subseteq {v}↔\bigcup _{{x}\in {r}}\left({k}×\left\{{x}\right\}\right)\subseteq {v}$
123 iunss ${⊢}\bigcup _{{x}\in {r}}\left({k}×\left\{{x}\right\}\right)\subseteq {v}↔\forall {x}\in {r}\phantom{\rule{.4em}{0ex}}{k}×\left\{{x}\right\}\subseteq {v}$
124 122 123 bitri ${⊢}{k}×{r}\subseteq {v}↔\forall {x}\in {r}\phantom{\rule{.4em}{0ex}}{k}×\left\{{x}\right\}\subseteq {v}$
125 ssin ${⊢}\left({k}×{r}\subseteq {v}\wedge {k}×{r}\subseteq {k}×{X}\right)↔{k}×{r}\subseteq {v}\cap \left({k}×{X}\right)$
126 117 124 125 3bitr3g ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\wedge {r}\in {R}\right)\to \left(\forall {x}\in {r}\phantom{\rule{.4em}{0ex}}{k}×\left\{{x}\right\}\subseteq {v}↔{k}×{r}\subseteq {v}\cap \left({k}×{X}\right)\right)$
127 99 adantr ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\wedge {r}\in {R}\right)\to {k}=\bigcup \left({S}{↾}_{𝑡}{k}\right)$
128 127 xpeq1d ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\wedge {r}\in {R}\right)\to {k}×{r}=\bigcup \left({S}{↾}_{𝑡}{k}\right)×{r}$
129 128 sseq1d ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\wedge {r}\in {R}\right)\to \left({k}×{r}\subseteq {v}\cap \left({k}×{X}\right)↔\bigcup \left({S}{↾}_{𝑡}{k}\right)×{r}\subseteq {v}\cap \left({k}×{X}\right)\right)$
130 114 126 129 3bitrd ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\wedge {r}\in {R}\right)\to \left({r}\subseteq \left\{{x}\in {X}|{k}×\left\{{x}\right\}\subseteq {v}\right\}↔\bigcup \left({S}{↾}_{𝑡}{k}\right)×{r}\subseteq {v}\cap \left({k}×{X}\right)\right)$
131 130 anbi2d ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\wedge {r}\in {R}\right)\to \left(\left({w}\in {r}\wedge {r}\subseteq \left\{{x}\in {X}|{k}×\left\{{x}\right\}\subseteq {v}\right\}\right)↔\left({w}\in {r}\wedge \bigcup \left({S}{↾}_{𝑡}{k}\right)×{r}\subseteq {v}\cap \left({k}×{X}\right)\right)\right)$
132 131 rexbidva ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to \left(\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({w}\in {r}\wedge {r}\subseteq \left\{{x}\in {X}|{k}×\left\{{x}\right\}\subseteq {v}\right\}\right)↔\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({w}\in {r}\wedge \bigcup \left({S}{↾}_{𝑡}{k}\right)×{r}\subseteq {v}\cap \left({k}×{X}\right)\right)\right)$
133 109 132 mpbird ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge \left({w}\in {X}\wedge {k}×\left\{{w}\right\}\subseteq {v}\right)\right)\to \exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({w}\in {r}\wedge {r}\subseteq \left\{{x}\in {X}|{k}×\left\{{x}\right\}\subseteq {v}\right\}\right)$
134 58 133 sylan2b ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\wedge {w}\in \left\{{x}\in {X}|{k}×\left\{{x}\right\}\subseteq {v}\right\}\right)\to \exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({w}\in {r}\wedge {r}\subseteq \left\{{x}\in {X}|{k}×\left\{{x}\right\}\subseteq {v}\right\}\right)$
135 134 ralrimiva ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\to \forall {w}\in \left\{{x}\in {X}|{k}×\left\{{x}\right\}\subseteq {v}\right\}\phantom{\rule{.4em}{0ex}}\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({w}\in {r}\wedge {r}\subseteq \left\{{x}\in {X}|{k}×\left\{{x}\right\}\subseteq {v}\right\}\right)$
136 eltop2 ${⊢}{R}\in \mathrm{Top}\to \left(\left\{{x}\in {X}|{k}×\left\{{x}\right\}\subseteq {v}\right\}\in {R}↔\forall {w}\in \left\{{x}\in {X}|{k}×\left\{{x}\right\}\subseteq {v}\right\}\phantom{\rule{.4em}{0ex}}\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({w}\in {r}\wedge {r}\subseteq \left\{{x}\in {X}|{k}×\left\{{x}\right\}\subseteq {v}\right\}\right)\right)$
137 14 68 136 3syl ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\to \left(\left\{{x}\in {X}|{k}×\left\{{x}\right\}\subseteq {v}\right\}\in {R}↔\forall {w}\in \left\{{x}\in {X}|{k}×\left\{{x}\right\}\subseteq {v}\right\}\phantom{\rule{.4em}{0ex}}\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({w}\in {r}\wedge {r}\subseteq \left\{{x}\in {X}|{k}×\left\{{x}\right\}\subseteq {v}\right\}\right)\right)$
138 135 137 mpbird ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\to \left\{{x}\in {X}|{k}×\left\{{x}\right\}\subseteq {v}\right\}\in {R}$
139 54 138 eqeltrd ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\to \left\{{x}\in {X}|\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\in \left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right\}\in {R}$
140 imaeq2 ${⊢}{z}=\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\to {{F}}^{-1}\left[{z}\right]={{F}}^{-1}\left[\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right]$
141 1 mptpreima ${⊢}{{F}}^{-1}\left[\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right]=\left\{{x}\in {X}|\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\in \left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right\}$
142 140 141 syl6eq ${⊢}{z}=\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\to {{F}}^{-1}\left[{z}\right]=\left\{{x}\in {X}|\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\in \left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right\}$
143 142 eleq1d ${⊢}{z}=\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\to \left({{F}}^{-1}\left[{z}\right]\in {R}↔\left\{{x}\in {X}|\left({y}\in {Y}⟼⟨{y},{x}⟩\right)\in \left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right\}\in {R}\right)$
144 139 143 syl5ibrcom ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\wedge {S}{↾}_{𝑡}{k}\in \mathrm{Comp}\right)\to \left({z}=\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\to {{F}}^{-1}\left[{z}\right]\in {R}\right)$
145 144 expimpd ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({k}\in 𝒫\bigcup {S}\wedge {v}\in \left({S}{×}_{t}{R}\right)\right)\right)\to \left(\left({S}{↾}_{𝑡}{k}\in \mathrm{Comp}\wedge {z}=\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right)\to {{F}}^{-1}\left[{z}\right]\in {R}\right)$
146 145 rexlimdvva ${⊢}\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left(\exists {k}\in 𝒫\bigcup {S}\phantom{\rule{.4em}{0ex}}\exists {v}\in \left({S}{×}_{t}{R}\right)\phantom{\rule{.4em}{0ex}}\left({S}{↾}_{𝑡}{k}\in \mathrm{Comp}\wedge {z}=\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right)\to {{F}}^{-1}\left[{z}\right]\in {R}\right)$
147 13 146 syl5bi ${⊢}\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left({z}\in \mathrm{ran}\left({k}\in \left\{{w}\in 𝒫\bigcup {S}|{S}{↾}_{𝑡}{w}\in \mathrm{Comp}\right\},{v}\in \left({S}{×}_{t}{R}\right)⟼\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right)\to {{F}}^{-1}\left[{z}\right]\in {R}\right)$
148 147 ralrimiv ${⊢}\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\to \forall {z}\in \mathrm{ran}\left({k}\in \left\{{w}\in 𝒫\bigcup {S}|{S}{↾}_{𝑡}{w}\in \mathrm{Comp}\right\},{v}\in \left({S}{×}_{t}{R}\right)⟼\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{z}\right]\in {R}$
149 simpl ${⊢}\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\to {R}\in \mathrm{TopOn}\left({X}\right)$
150 ovex ${⊢}{S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\in \mathrm{V}$
151 150 pwex ${⊢}𝒫\left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)\in \mathrm{V}$
152 9 10 11 xkotf ${⊢}\left({k}\in \left\{{w}\in 𝒫\bigcup {S}|{S}{↾}_{𝑡}{w}\in \mathrm{Comp}\right\},{v}\in \left({S}{×}_{t}{R}\right)⟼\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right):\left\{{w}\in 𝒫\bigcup {S}|{S}{↾}_{𝑡}{w}\in \mathrm{Comp}\right\}×\left({S}{×}_{t}{R}\right)⟶𝒫\left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)$
153 frn ${⊢}\left({k}\in \left\{{w}\in 𝒫\bigcup {S}|{S}{↾}_{𝑡}{w}\in \mathrm{Comp}\right\},{v}\in \left({S}{×}_{t}{R}\right)⟼\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right):\left\{{w}\in 𝒫\bigcup {S}|{S}{↾}_{𝑡}{w}\in \mathrm{Comp}\right\}×\left({S}{×}_{t}{R}\right)⟶𝒫\left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)\to \mathrm{ran}\left({k}\in \left\{{w}\in 𝒫\bigcup {S}|{S}{↾}_{𝑡}{w}\in \mathrm{Comp}\right\},{v}\in \left({S}{×}_{t}{R}\right)⟼\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right)\subseteq 𝒫\left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)$
154 152 153 ax-mp ${⊢}\mathrm{ran}\left({k}\in \left\{{w}\in 𝒫\bigcup {S}|{S}{↾}_{𝑡}{w}\in \mathrm{Comp}\right\},{v}\in \left({S}{×}_{t}{R}\right)⟼\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right)\subseteq 𝒫\left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)$
155 151 154 ssexi ${⊢}\mathrm{ran}\left({k}\in \left\{{w}\in 𝒫\bigcup {S}|{S}{↾}_{𝑡}{w}\in \mathrm{Comp}\right\},{v}\in \left({S}{×}_{t}{R}\right)⟼\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right)\in \mathrm{V}$
156 155 a1i ${⊢}\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\to \mathrm{ran}\left({k}\in \left\{{w}\in 𝒫\bigcup {S}|{S}{↾}_{𝑡}{w}\in \mathrm{Comp}\right\},{v}\in \left({S}{×}_{t}{R}\right)⟼\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right)\in \mathrm{V}$
157 9 10 11 xkoval ${⊢}\left({S}\in \mathrm{Top}\wedge {S}{×}_{t}{R}\in \mathrm{Top}\right)\to \left({S}{×}_{t}{R}\right){^}_{\mathrm{ko}}{S}=\mathrm{topGen}\left(\mathrm{fi}\left(\mathrm{ran}\left({k}\in \left\{{w}\in 𝒫\bigcup {S}|{S}{↾}_{𝑡}{w}\in \mathrm{Comp}\right\},{v}\in \left({S}{×}_{t}{R}\right)⟼\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right)\right)\right)$
158 67 70 157 syl2anc ${⊢}\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left({S}{×}_{t}{R}\right){^}_{\mathrm{ko}}{S}=\mathrm{topGen}\left(\mathrm{fi}\left(\mathrm{ran}\left({k}\in \left\{{w}\in 𝒫\bigcup {S}|{S}{↾}_{𝑡}{w}\in \mathrm{Comp}\right\},{v}\in \left({S}{×}_{t}{R}\right)⟼\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right)\right)\right)$
159 eqid ${⊢}\left({S}{×}_{t}{R}\right){^}_{\mathrm{ko}}{S}=\left({S}{×}_{t}{R}\right){^}_{\mathrm{ko}}{S}$
160 159 xkotopon ${⊢}\left({S}\in \mathrm{Top}\wedge {S}{×}_{t}{R}\in \mathrm{Top}\right)\to \left({S}{×}_{t}{R}\right){^}_{\mathrm{ko}}{S}\in \mathrm{TopOn}\left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)$
161 67 70 160 syl2anc ${⊢}\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left({S}{×}_{t}{R}\right){^}_{\mathrm{ko}}{S}\in \mathrm{TopOn}\left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)$
162 149 156 158 161 subbascn ${⊢}\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left({F}\in \left({R}\mathrm{Cn}\left(\left({S}{×}_{t}{R}\right){^}_{\mathrm{ko}}{S}\right)\right)↔\left({F}:{X}⟶{S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\wedge \forall {z}\in \mathrm{ran}\left({k}\in \left\{{w}\in 𝒫\bigcup {S}|{S}{↾}_{𝑡}{w}\in \mathrm{Comp}\right\},{v}\in \left({S}{×}_{t}{R}\right)⟼\left\{{f}\in \left({S}\mathrm{Cn}\left({S}{×}_{t}{R}\right)\right)|{f}\left[{k}\right]\subseteq {v}\right\}\right)\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{z}\right]\in {R}\right)\right)$
163 8 148 162 mpbir2and ${⊢}\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\to {F}\in \left({R}\mathrm{Cn}\left(\left({S}{×}_{t}{R}\right){^}_{\mathrm{ko}}{S}\right)\right)$