# Metamath Proof Explorer

## Theorem txcls

Description: Closure of a rectangle in the product topology. (Contributed by Mario Carneiro, 17-Sep-2015)

Ref Expression
Assertion txcls ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to \mathrm{cls}\left({R}{×}_{t}{S}\right)\left({A}×{B}\right)=\mathrm{cls}\left({R}\right)\left({A}\right)×\mathrm{cls}\left({S}\right)\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 topontop ${⊢}{R}\in \mathrm{TopOn}\left({X}\right)\to {R}\in \mathrm{Top}$
2 1 ad2antrr ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to {R}\in \mathrm{Top}$
3 simprl ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to {A}\subseteq {X}$
4 toponuni ${⊢}{R}\in \mathrm{TopOn}\left({X}\right)\to {X}=\bigcup {R}$
5 4 ad2antrr ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to {X}=\bigcup {R}$
6 3 5 sseqtrd ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to {A}\subseteq \bigcup {R}$
7 eqid ${⊢}\bigcup {R}=\bigcup {R}$
8 7 clscld ${⊢}\left({R}\in \mathrm{Top}\wedge {A}\subseteq \bigcup {R}\right)\to \mathrm{cls}\left({R}\right)\left({A}\right)\in \mathrm{Clsd}\left({R}\right)$
9 2 6 8 syl2anc ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to \mathrm{cls}\left({R}\right)\left({A}\right)\in \mathrm{Clsd}\left({R}\right)$
10 topontop ${⊢}{S}\in \mathrm{TopOn}\left({Y}\right)\to {S}\in \mathrm{Top}$
11 10 ad2antlr ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to {S}\in \mathrm{Top}$
12 simprr ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to {B}\subseteq {Y}$
13 toponuni ${⊢}{S}\in \mathrm{TopOn}\left({Y}\right)\to {Y}=\bigcup {S}$
14 13 ad2antlr ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to {Y}=\bigcup {S}$
15 12 14 sseqtrd ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to {B}\subseteq \bigcup {S}$
16 eqid ${⊢}\bigcup {S}=\bigcup {S}$
17 16 clscld ${⊢}\left({S}\in \mathrm{Top}\wedge {B}\subseteq \bigcup {S}\right)\to \mathrm{cls}\left({S}\right)\left({B}\right)\in \mathrm{Clsd}\left({S}\right)$
18 11 15 17 syl2anc ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to \mathrm{cls}\left({S}\right)\left({B}\right)\in \mathrm{Clsd}\left({S}\right)$
19 txcld ${⊢}\left(\mathrm{cls}\left({R}\right)\left({A}\right)\in \mathrm{Clsd}\left({R}\right)\wedge \mathrm{cls}\left({S}\right)\left({B}\right)\in \mathrm{Clsd}\left({S}\right)\right)\to \mathrm{cls}\left({R}\right)\left({A}\right)×\mathrm{cls}\left({S}\right)\left({B}\right)\in \mathrm{Clsd}\left({R}{×}_{t}{S}\right)$
20 9 18 19 syl2anc ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to \mathrm{cls}\left({R}\right)\left({A}\right)×\mathrm{cls}\left({S}\right)\left({B}\right)\in \mathrm{Clsd}\left({R}{×}_{t}{S}\right)$
21 7 sscls ${⊢}\left({R}\in \mathrm{Top}\wedge {A}\subseteq \bigcup {R}\right)\to {A}\subseteq \mathrm{cls}\left({R}\right)\left({A}\right)$
22 2 6 21 syl2anc ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to {A}\subseteq \mathrm{cls}\left({R}\right)\left({A}\right)$
23 16 sscls ${⊢}\left({S}\in \mathrm{Top}\wedge {B}\subseteq \bigcup {S}\right)\to {B}\subseteq \mathrm{cls}\left({S}\right)\left({B}\right)$
24 11 15 23 syl2anc ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to {B}\subseteq \mathrm{cls}\left({S}\right)\left({B}\right)$
25 xpss12 ${⊢}\left({A}\subseteq \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {B}\subseteq \mathrm{cls}\left({S}\right)\left({B}\right)\right)\to {A}×{B}\subseteq \mathrm{cls}\left({R}\right)\left({A}\right)×\mathrm{cls}\left({S}\right)\left({B}\right)$
26 22 24 25 syl2anc ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to {A}×{B}\subseteq \mathrm{cls}\left({R}\right)\left({A}\right)×\mathrm{cls}\left({S}\right)\left({B}\right)$
27 eqid ${⊢}\bigcup \left({R}{×}_{t}{S}\right)=\bigcup \left({R}{×}_{t}{S}\right)$
28 27 clsss2 ${⊢}\left(\mathrm{cls}\left({R}\right)\left({A}\right)×\mathrm{cls}\left({S}\right)\left({B}\right)\in \mathrm{Clsd}\left({R}{×}_{t}{S}\right)\wedge {A}×{B}\subseteq \mathrm{cls}\left({R}\right)\left({A}\right)×\mathrm{cls}\left({S}\right)\left({B}\right)\right)\to \mathrm{cls}\left({R}{×}_{t}{S}\right)\left({A}×{B}\right)\subseteq \mathrm{cls}\left({R}\right)\left({A}\right)×\mathrm{cls}\left({S}\right)\left({B}\right)$
29 20 26 28 syl2anc ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to \mathrm{cls}\left({R}{×}_{t}{S}\right)\left({A}×{B}\right)\subseteq \mathrm{cls}\left({R}\right)\left({A}\right)×\mathrm{cls}\left({S}\right)\left({B}\right)$
30 relxp ${⊢}\mathrm{Rel}\left(\mathrm{cls}\left({R}\right)\left({A}\right)×\mathrm{cls}\left({S}\right)\left({B}\right)\right)$
31 30 a1i ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to \mathrm{Rel}\left(\mathrm{cls}\left({R}\right)\left({A}\right)×\mathrm{cls}\left({S}\right)\left({B}\right)\right)$
32 opelxp ${⊢}⟨{x},{y}⟩\in \left(\mathrm{cls}\left({R}\right)\left({A}\right)×\mathrm{cls}\left({S}\right)\left({B}\right)\right)↔\left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)$
33 eltx ${⊢}\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left({u}\in \left({R}{×}_{t}{S}\right)↔\forall {z}\in {u}\phantom{\rule{.4em}{0ex}}\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({z}\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)$
34 33 ad2antrr ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\to \left({u}\in \left({R}{×}_{t}{S}\right)↔\forall {z}\in {u}\phantom{\rule{.4em}{0ex}}\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({z}\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)$
35 eleq1 ${⊢}{z}=⟨{x},{y}⟩\to \left({z}\in \left({r}×{s}\right)↔⟨{x},{y}⟩\in \left({r}×{s}\right)\right)$
36 35 anbi1d ${⊢}{z}=⟨{x},{y}⟩\to \left(\left({z}\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)↔\left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)$
37 36 2rexbidv ${⊢}{z}=⟨{x},{y}⟩\to \left(\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({z}\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)↔\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)$
38 37 rspccva ${⊢}\left(\forall {z}\in {u}\phantom{\rule{.4em}{0ex}}\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({z}\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\wedge ⟨{x},{y}⟩\in {u}\right)\to \exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)$
39 2 ad2antrr ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\to {R}\in \mathrm{Top}$
40 6 ad2antrr ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\to {A}\subseteq \bigcup {R}$
41 simplrl ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\to {x}\in \mathrm{cls}\left({R}\right)\left({A}\right)$
42 simprll ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\to {r}\in {R}$
43 simprrl ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\to ⟨{x},{y}⟩\in \left({r}×{s}\right)$
44 opelxp ${⊢}⟨{x},{y}⟩\in \left({r}×{s}\right)↔\left({x}\in {r}\wedge {y}\in {s}\right)$
45 43 44 sylib ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\to \left({x}\in {r}\wedge {y}\in {s}\right)$
46 45 simpld ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\to {x}\in {r}$
47 7 clsndisj ${⊢}\left(\left({R}\in \mathrm{Top}\wedge {A}\subseteq \bigcup {R}\wedge {x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\right)\wedge \left({r}\in {R}\wedge {x}\in {r}\right)\right)\to {r}\cap {A}\ne \varnothing$
48 39 40 41 42 46 47 syl32anc ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\to {r}\cap {A}\ne \varnothing$
49 n0 ${⊢}{r}\cap {A}\ne \varnothing ↔\exists {z}\phantom{\rule{.4em}{0ex}}{z}\in \left({r}\cap {A}\right)$
50 48 49 sylib ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\to \exists {z}\phantom{\rule{.4em}{0ex}}{z}\in \left({r}\cap {A}\right)$
51 11 ad2antrr ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\to {S}\in \mathrm{Top}$
52 15 ad2antrr ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\to {B}\subseteq \bigcup {S}$
53 simplrr ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\to {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)$
54 simprlr ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\to {s}\in {S}$
55 45 simprd ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\to {y}\in {s}$
56 16 clsndisj ${⊢}\left(\left({S}\in \mathrm{Top}\wedge {B}\subseteq \bigcup {S}\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\wedge \left({s}\in {S}\wedge {y}\in {s}\right)\right)\to {s}\cap {B}\ne \varnothing$
57 51 52 53 54 55 56 syl32anc ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\to {s}\cap {B}\ne \varnothing$
58 n0 ${⊢}{s}\cap {B}\ne \varnothing ↔\exists {w}\phantom{\rule{.4em}{0ex}}{w}\in \left({s}\cap {B}\right)$
59 57 58 sylib ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\to \exists {w}\phantom{\rule{.4em}{0ex}}{w}\in \left({s}\cap {B}\right)$
60 exdistrv ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({z}\in \left({r}\cap {A}\right)\wedge {w}\in \left({s}\cap {B}\right)\right)↔\left(\exists {z}\phantom{\rule{.4em}{0ex}}{z}\in \left({r}\cap {A}\right)\wedge \exists {w}\phantom{\rule{.4em}{0ex}}{w}\in \left({s}\cap {B}\right)\right)$
61 opelxpi ${⊢}\left({z}\in \left({r}\cap {A}\right)\wedge {w}\in \left({s}\cap {B}\right)\right)\to ⟨{z},{w}⟩\in \left(\left({r}\cap {A}\right)×\left({s}\cap {B}\right)\right)$
62 inxp ${⊢}\left({r}×{s}\right)\cap \left({A}×{B}\right)=\left({r}\cap {A}\right)×\left({s}\cap {B}\right)$
63 61 62 eleqtrrdi ${⊢}\left({z}\in \left({r}\cap {A}\right)\wedge {w}\in \left({s}\cap {B}\right)\right)\to ⟨{z},{w}⟩\in \left(\left({r}×{s}\right)\cap \left({A}×{B}\right)\right)$
64 63 elin1d ${⊢}\left({z}\in \left({r}\cap {A}\right)\wedge {w}\in \left({s}\cap {B}\right)\right)\to ⟨{z},{w}⟩\in \left({r}×{s}\right)$
65 simprrr ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\to {r}×{s}\subseteq {u}$
66 65 sselda ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\wedge ⟨{z},{w}⟩\in \left({r}×{s}\right)\right)\to ⟨{z},{w}⟩\in {u}$
67 64 66 sylan2 ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\wedge \left({z}\in \left({r}\cap {A}\right)\wedge {w}\in \left({s}\cap {B}\right)\right)\right)\to ⟨{z},{w}⟩\in {u}$
68 63 elin2d ${⊢}\left({z}\in \left({r}\cap {A}\right)\wedge {w}\in \left({s}\cap {B}\right)\right)\to ⟨{z},{w}⟩\in \left({A}×{B}\right)$
69 68 adantl ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\wedge \left({z}\in \left({r}\cap {A}\right)\wedge {w}\in \left({s}\cap {B}\right)\right)\right)\to ⟨{z},{w}⟩\in \left({A}×{B}\right)$
70 inelcm ${⊢}\left(⟨{z},{w}⟩\in {u}\wedge ⟨{z},{w}⟩\in \left({A}×{B}\right)\right)\to {u}\cap \left({A}×{B}\right)\ne \varnothing$
71 67 69 70 syl2anc ${⊢}\left(\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\wedge \left({z}\in \left({r}\cap {A}\right)\wedge {w}\in \left({s}\cap {B}\right)\right)\right)\to {u}\cap \left({A}×{B}\right)\ne \varnothing$
72 71 ex ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\to \left(\left({z}\in \left({r}\cap {A}\right)\wedge {w}\in \left({s}\cap {B}\right)\right)\to {u}\cap \left({A}×{B}\right)\ne \varnothing \right)$
73 72 exlimdvv ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\to \left(\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({z}\in \left({r}\cap {A}\right)\wedge {w}\in \left({s}\cap {B}\right)\right)\to {u}\cap \left({A}×{B}\right)\ne \varnothing \right)$
74 60 73 syl5bir ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\to \left(\left(\exists {z}\phantom{\rule{.4em}{0ex}}{z}\in \left({r}\cap {A}\right)\wedge \exists {w}\phantom{\rule{.4em}{0ex}}{w}\in \left({s}\cap {B}\right)\right)\to {u}\cap \left({A}×{B}\right)\ne \varnothing \right)$
75 50 59 74 mp2and ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left(\left({r}\in {R}\wedge {s}\in {S}\right)\wedge \left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\right)\right)\to {u}\cap \left({A}×{B}\right)\ne \varnothing$
76 75 expr ${⊢}\left(\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\wedge \left({r}\in {R}\wedge {s}\in {S}\right)\right)\to \left(\left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\to {u}\cap \left({A}×{B}\right)\ne \varnothing \right)$
77 76 rexlimdvva ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\to \left(\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\to {u}\cap \left({A}×{B}\right)\ne \varnothing \right)$
78 38 77 syl5 ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\to \left(\left(\forall {z}\in {u}\phantom{\rule{.4em}{0ex}}\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({z}\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\wedge ⟨{x},{y}⟩\in {u}\right)\to {u}\cap \left({A}×{B}\right)\ne \varnothing \right)$
79 78 expd ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\to \left(\forall {z}\in {u}\phantom{\rule{.4em}{0ex}}\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({z}\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {u}\right)\to \left(⟨{x},{y}⟩\in {u}\to {u}\cap \left({A}×{B}\right)\ne \varnothing \right)\right)$
80 34 79 sylbid ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\to \left({u}\in \left({R}{×}_{t}{S}\right)\to \left(⟨{x},{y}⟩\in {u}\to {u}\cap \left({A}×{B}\right)\ne \varnothing \right)\right)$
81 80 ralrimiv ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\to \forall {u}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {u}\to {u}\cap \left({A}×{B}\right)\ne \varnothing \right)$
82 txtopon ${⊢}\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\to {R}{×}_{t}{S}\in \mathrm{TopOn}\left({X}×{Y}\right)$
83 82 ad2antrr ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\to {R}{×}_{t}{S}\in \mathrm{TopOn}\left({X}×{Y}\right)$
84 topontop ${⊢}{R}{×}_{t}{S}\in \mathrm{TopOn}\left({X}×{Y}\right)\to {R}{×}_{t}{S}\in \mathrm{Top}$
85 83 84 syl ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\to {R}{×}_{t}{S}\in \mathrm{Top}$
86 xpss12 ${⊢}\left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\to {A}×{B}\subseteq {X}×{Y}$
87 86 ad2antlr ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\to {A}×{B}\subseteq {X}×{Y}$
88 toponuni ${⊢}{R}{×}_{t}{S}\in \mathrm{TopOn}\left({X}×{Y}\right)\to {X}×{Y}=\bigcup \left({R}{×}_{t}{S}\right)$
89 83 88 syl ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\to {X}×{Y}=\bigcup \left({R}{×}_{t}{S}\right)$
90 87 89 sseqtrd ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\to {A}×{B}\subseteq \bigcup \left({R}{×}_{t}{S}\right)$
91 7 clsss3 ${⊢}\left({R}\in \mathrm{Top}\wedge {A}\subseteq \bigcup {R}\right)\to \mathrm{cls}\left({R}\right)\left({A}\right)\subseteq \bigcup {R}$
92 2 6 91 syl2anc ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to \mathrm{cls}\left({R}\right)\left({A}\right)\subseteq \bigcup {R}$
93 92 5 sseqtrrd ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to \mathrm{cls}\left({R}\right)\left({A}\right)\subseteq {X}$
94 93 sselda ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge {x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\right)\to {x}\in {X}$
95 94 adantrr ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\to {x}\in {X}$
96 16 clsss3 ${⊢}\left({S}\in \mathrm{Top}\wedge {B}\subseteq \bigcup {S}\right)\to \mathrm{cls}\left({S}\right)\left({B}\right)\subseteq \bigcup {S}$
97 11 15 96 syl2anc ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to \mathrm{cls}\left({S}\right)\left({B}\right)\subseteq \bigcup {S}$
98 97 14 sseqtrrd ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to \mathrm{cls}\left({S}\right)\left({B}\right)\subseteq {Y}$
99 98 sselda ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\to {y}\in {Y}$
100 99 adantrl ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\to {y}\in {Y}$
101 95 100 opelxpd ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\to ⟨{x},{y}⟩\in \left({X}×{Y}\right)$
102 101 89 eleqtrd ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\to ⟨{x},{y}⟩\in \bigcup \left({R}{×}_{t}{S}\right)$
103 27 elcls ${⊢}\left({R}{×}_{t}{S}\in \mathrm{Top}\wedge {A}×{B}\subseteq \bigcup \left({R}{×}_{t}{S}\right)\wedge ⟨{x},{y}⟩\in \bigcup \left({R}{×}_{t}{S}\right)\right)\to \left(⟨{x},{y}⟩\in \mathrm{cls}\left({R}{×}_{t}{S}\right)\left({A}×{B}\right)↔\forall {u}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {u}\to {u}\cap \left({A}×{B}\right)\ne \varnothing \right)\right)$
104 85 90 102 103 syl3anc ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\to \left(⟨{x},{y}⟩\in \mathrm{cls}\left({R}{×}_{t}{S}\right)\left({A}×{B}\right)↔\forall {u}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {u}\to {u}\cap \left({A}×{B}\right)\ne \varnothing \right)\right)$
105 81 104 mpbird ${⊢}\left(\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\wedge \left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\right)\to ⟨{x},{y}⟩\in \mathrm{cls}\left({R}{×}_{t}{S}\right)\left({A}×{B}\right)$
106 105 ex ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to \left(\left({x}\in \mathrm{cls}\left({R}\right)\left({A}\right)\wedge {y}\in \mathrm{cls}\left({S}\right)\left({B}\right)\right)\to ⟨{x},{y}⟩\in \mathrm{cls}\left({R}{×}_{t}{S}\right)\left({A}×{B}\right)\right)$
107 32 106 syl5bi ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to \left(⟨{x},{y}⟩\in \left(\mathrm{cls}\left({R}\right)\left({A}\right)×\mathrm{cls}\left({S}\right)\left({B}\right)\right)\to ⟨{x},{y}⟩\in \mathrm{cls}\left({R}{×}_{t}{S}\right)\left({A}×{B}\right)\right)$
108 31 107 relssdv ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to \mathrm{cls}\left({R}\right)\left({A}\right)×\mathrm{cls}\left({S}\right)\left({B}\right)\subseteq \mathrm{cls}\left({R}{×}_{t}{S}\right)\left({A}×{B}\right)$
109 29 108 eqssd ${⊢}\left(\left({R}\in \mathrm{TopOn}\left({X}\right)\wedge {S}\in \mathrm{TopOn}\left({Y}\right)\right)\wedge \left({A}\subseteq {X}\wedge {B}\subseteq {Y}\right)\right)\to \mathrm{cls}\left({R}{×}_{t}{S}\right)\left({A}×{B}\right)=\mathrm{cls}\left({R}\right)\left({A}\right)×\mathrm{cls}\left({S}\right)\left({B}\right)$