# Metamath Proof Explorer

## Theorem tx1stc

Description: The topological product of two first-countable spaces is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion tx1stc ${⊢}\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\to {R}{×}_{t}{S}\in {1}^{st}𝜔$

### Proof

Step Hyp Ref Expression
1 1stctop ${⊢}{R}\in {1}^{st}𝜔\to {R}\in \mathrm{Top}$
2 1stctop ${⊢}{S}\in {1}^{st}𝜔\to {S}\in \mathrm{Top}$
3 txtop ${⊢}\left({R}\in \mathrm{Top}\wedge {S}\in \mathrm{Top}\right)\to {R}{×}_{t}{S}\in \mathrm{Top}$
4 1 2 3 syl2an ${⊢}\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\to {R}{×}_{t}{S}\in \mathrm{Top}$
5 eqid ${⊢}\bigcup {R}=\bigcup {R}$
6 5 1stcclb ${⊢}\left({R}\in {1}^{st}𝜔\wedge {u}\in \bigcup {R}\right)\to \exists {a}\in 𝒫{R}\phantom{\rule{.4em}{0ex}}\left({a}\preccurlyeq \mathrm{\omega }\wedge \forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\right)$
7 6 ad2ant2r ${⊢}\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\to \exists {a}\in 𝒫{R}\phantom{\rule{.4em}{0ex}}\left({a}\preccurlyeq \mathrm{\omega }\wedge \forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\right)$
8 eqid ${⊢}\bigcup {S}=\bigcup {S}$
9 8 1stcclb ${⊢}\left({S}\in {1}^{st}𝜔\wedge {v}\in \bigcup {S}\right)\to \exists {b}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({b}\preccurlyeq \mathrm{\omega }\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)$
10 9 ad2ant2l ${⊢}\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\to \exists {b}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({b}\preccurlyeq \mathrm{\omega }\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)$
11 reeanv ${⊢}\exists {a}\in 𝒫{R}\phantom{\rule{.4em}{0ex}}\exists {b}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left(\left({a}\preccurlyeq \mathrm{\omega }\wedge \forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\right)\wedge \left({b}\preccurlyeq \mathrm{\omega }\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\right)↔\left(\exists {a}\in 𝒫{R}\phantom{\rule{.4em}{0ex}}\left({a}\preccurlyeq \mathrm{\omega }\wedge \forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\right)\wedge \exists {b}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({b}\preccurlyeq \mathrm{\omega }\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\right)$
12 an4 ${⊢}\left(\left({a}\preccurlyeq \mathrm{\omega }\wedge \forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\right)\wedge \left({b}\preccurlyeq \mathrm{\omega }\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\right)↔\left(\left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\wedge \left(\forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\right)$
13 txopn ${⊢}\left(\left({R}\in \mathrm{Top}\wedge {S}\in \mathrm{Top}\right)\wedge \left({m}\in {R}\wedge {n}\in {S}\right)\right)\to {m}×{n}\in \left({R}{×}_{t}{S}\right)$
14 13 ralrimivva ${⊢}\left({R}\in \mathrm{Top}\wedge {S}\in \mathrm{Top}\right)\to \forall {m}\in {R}\phantom{\rule{.4em}{0ex}}\forall {n}\in {S}\phantom{\rule{.4em}{0ex}}{m}×{n}\in \left({R}{×}_{t}{S}\right)$
15 1 2 14 syl2an ${⊢}\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\to \forall {m}\in {R}\phantom{\rule{.4em}{0ex}}\forall {n}\in {S}\phantom{\rule{.4em}{0ex}}{m}×{n}\in \left({R}{×}_{t}{S}\right)$
16 15 adantr ${⊢}\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\to \forall {m}\in {R}\phantom{\rule{.4em}{0ex}}\forall {n}\in {S}\phantom{\rule{.4em}{0ex}}{m}×{n}\in \left({R}{×}_{t}{S}\right)$
17 elpwi ${⊢}{a}\in 𝒫{R}\to {a}\subseteq {R}$
18 ssralv ${⊢}{a}\subseteq {R}\to \left(\forall {m}\in {R}\phantom{\rule{.4em}{0ex}}\forall {n}\in {S}\phantom{\rule{.4em}{0ex}}{m}×{n}\in \left({R}{×}_{t}{S}\right)\to \forall {m}\in {a}\phantom{\rule{.4em}{0ex}}\forall {n}\in {S}\phantom{\rule{.4em}{0ex}}{m}×{n}\in \left({R}{×}_{t}{S}\right)\right)$
19 17 18 syl ${⊢}{a}\in 𝒫{R}\to \left(\forall {m}\in {R}\phantom{\rule{.4em}{0ex}}\forall {n}\in {S}\phantom{\rule{.4em}{0ex}}{m}×{n}\in \left({R}{×}_{t}{S}\right)\to \forall {m}\in {a}\phantom{\rule{.4em}{0ex}}\forall {n}\in {S}\phantom{\rule{.4em}{0ex}}{m}×{n}\in \left({R}{×}_{t}{S}\right)\right)$
20 elpwi ${⊢}{b}\in 𝒫{S}\to {b}\subseteq {S}$
21 ssralv ${⊢}{b}\subseteq {S}\to \left(\forall {n}\in {S}\phantom{\rule{.4em}{0ex}}{m}×{n}\in \left({R}{×}_{t}{S}\right)\to \forall {n}\in {b}\phantom{\rule{.4em}{0ex}}{m}×{n}\in \left({R}{×}_{t}{S}\right)\right)$
22 20 21 syl ${⊢}{b}\in 𝒫{S}\to \left(\forall {n}\in {S}\phantom{\rule{.4em}{0ex}}{m}×{n}\in \left({R}{×}_{t}{S}\right)\to \forall {n}\in {b}\phantom{\rule{.4em}{0ex}}{m}×{n}\in \left({R}{×}_{t}{S}\right)\right)$
23 22 ralimdv ${⊢}{b}\in 𝒫{S}\to \left(\forall {m}\in {a}\phantom{\rule{.4em}{0ex}}\forall {n}\in {S}\phantom{\rule{.4em}{0ex}}{m}×{n}\in \left({R}{×}_{t}{S}\right)\to \forall {m}\in {a}\phantom{\rule{.4em}{0ex}}\forall {n}\in {b}\phantom{\rule{.4em}{0ex}}{m}×{n}\in \left({R}{×}_{t}{S}\right)\right)$
24 19 23 sylan9 ${⊢}\left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\to \left(\forall {m}\in {R}\phantom{\rule{.4em}{0ex}}\forall {n}\in {S}\phantom{\rule{.4em}{0ex}}{m}×{n}\in \left({R}{×}_{t}{S}\right)\to \forall {m}\in {a}\phantom{\rule{.4em}{0ex}}\forall {n}\in {b}\phantom{\rule{.4em}{0ex}}{m}×{n}\in \left({R}{×}_{t}{S}\right)\right)$
25 16 24 mpan9 ${⊢}\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\to \forall {m}\in {a}\phantom{\rule{.4em}{0ex}}\forall {n}\in {b}\phantom{\rule{.4em}{0ex}}{m}×{n}\in \left({R}{×}_{t}{S}\right)$
26 eqid ${⊢}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)=\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)$
27 26 fmpo ${⊢}\forall {m}\in {a}\phantom{\rule{.4em}{0ex}}\forall {n}\in {b}\phantom{\rule{.4em}{0ex}}{m}×{n}\in \left({R}{×}_{t}{S}\right)↔\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right):{a}×{b}⟶{R}{×}_{t}{S}$
28 25 27 sylib ${⊢}\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\to \left({m}\in {a},{n}\in {b}⟼{m}×{n}\right):{a}×{b}⟶{R}{×}_{t}{S}$
29 28 frnd ${⊢}\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\to \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\subseteq {R}{×}_{t}{S}$
30 ovex ${⊢}{R}{×}_{t}{S}\in \mathrm{V}$
31 30 elpw2 ${⊢}\mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\in 𝒫\left({R}{×}_{t}{S}\right)↔\mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\subseteq {R}{×}_{t}{S}$
32 29 31 sylibr ${⊢}\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\to \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\in 𝒫\left({R}{×}_{t}{S}\right)$
33 32 adantr ${⊢}\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left(\left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\wedge \left(\forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\right)\right)\to \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\in 𝒫\left({R}{×}_{t}{S}\right)$
34 omelon ${⊢}\mathrm{\omega }\in \mathrm{On}$
35 xpct ${⊢}\left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\to \left({a}×{b}\right)\preccurlyeq \mathrm{\omega }$
36 ondomen ${⊢}\left(\mathrm{\omega }\in \mathrm{On}\wedge \left({a}×{b}\right)\preccurlyeq \mathrm{\omega }\right)\to {a}×{b}\in \mathrm{dom}\mathrm{card}$
37 34 35 36 sylancr ${⊢}\left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\to {a}×{b}\in \mathrm{dom}\mathrm{card}$
38 vex ${⊢}{m}\in \mathrm{V}$
39 vex ${⊢}{n}\in \mathrm{V}$
40 38 39 xpex ${⊢}{m}×{n}\in \mathrm{V}$
41 26 40 fnmpoi ${⊢}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)Fn\left({a}×{b}\right)$
42 dffn4 ${⊢}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)Fn\left({a}×{b}\right)↔\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right):{a}×{b}\underset{onto}{⟶}\mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)$
43 41 42 mpbi ${⊢}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right):{a}×{b}\underset{onto}{⟶}\mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)$
44 fodomnum ${⊢}{a}×{b}\in \mathrm{dom}\mathrm{card}\to \left(\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right):{a}×{b}\underset{onto}{⟶}\mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\to \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\preccurlyeq \left({a}×{b}\right)\right)$
45 37 43 44 mpisyl ${⊢}\left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\to \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\preccurlyeq \left({a}×{b}\right)$
46 domtr ${⊢}\left(\mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\preccurlyeq \left({a}×{b}\right)\wedge \left({a}×{b}\right)\preccurlyeq \mathrm{\omega }\right)\to \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\preccurlyeq \mathrm{\omega }$
47 45 35 46 syl2anc ${⊢}\left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\to \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\preccurlyeq \mathrm{\omega }$
48 47 ad2antrl ${⊢}\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left(\left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\wedge \left(\forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\right)\right)\to \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\preccurlyeq \mathrm{\omega }$
49 1 2 anim12i ${⊢}\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\to \left({R}\in \mathrm{Top}\wedge {S}\in \mathrm{Top}\right)$
50 49 ad3antrrr ${⊢}\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left(\left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\wedge \left(\forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\right)\right)\to \left({R}\in \mathrm{Top}\wedge {S}\in \mathrm{Top}\right)$
51 eltx ${⊢}\left({R}\in \mathrm{Top}\wedge {S}\in \mathrm{Top}\right)\to \left({z}\in \left({R}{×}_{t}{S}\right)↔\forall {w}\in {z}\phantom{\rule{.4em}{0ex}}\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({w}\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)\right)$
52 50 51 syl ${⊢}\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left(\left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\wedge \left(\forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\right)\right)\to \left({z}\in \left({R}{×}_{t}{S}\right)↔\forall {w}\in {z}\phantom{\rule{.4em}{0ex}}\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({w}\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)\right)$
53 eleq1 ${⊢}{w}=⟨{u},{v}⟩\to \left({w}\in \left({r}×{s}\right)↔⟨{u},{v}⟩\in \left({r}×{s}\right)\right)$
54 53 anbi1d ${⊢}{w}=⟨{u},{v}⟩\to \left(\left({w}\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)↔\left(⟨{u},{v}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)\right)$
55 54 2rexbidv ${⊢}{w}=⟨{u},{v}⟩\to \left(\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({w}\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)↔\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)\right)$
56 55 rspccv ${⊢}\forall {w}\in {z}\phantom{\rule{.4em}{0ex}}\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({w}\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)\to \left(⟨{u},{v}⟩\in {z}\to \exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)\right)$
57 r19.27v ${⊢}\left(\forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\to \forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)$
58 r19.29 ${⊢}\left(\forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\wedge \exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to \exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\left(\left(\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\wedge \exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)\right)$
59 r19.29 ${⊢}\left(\forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge \exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to \exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge \left(⟨{u},{v}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)\right)$
60 opelxp ${⊢}⟨{u},{v}⟩\in \left({r}×{s}\right)↔\left({u}\in {r}\wedge {v}\in {s}\right)$
61 pm3.35 ${⊢}\left({u}\in {r}\wedge \left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\right)\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)$
62 pm3.35 ${⊢}\left({v}\in {s}\wedge \left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)$
63 61 62 anim12i ${⊢}\left(\left({u}\in {r}\wedge \left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\right)\wedge \left({v}\in {s}\wedge \left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\right)\to \left(\exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)$
64 63 an4s ${⊢}\left(\left({u}\in {r}\wedge {v}\in {s}\right)\wedge \left(\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\right)\to \left(\exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)$
65 60 64 sylanb ${⊢}\left(⟨{u},{v}⟩\in \left({r}×{s}\right)\wedge \left(\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\right)\to \left(\exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)$
66 65 anim1i ${⊢}\left(\left(⟨{u},{v}⟩\in \left({r}×{s}\right)\wedge \left(\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\right)\wedge {r}×{s}\subseteq {z}\right)\to \left(\left(\exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)$
67 66 anasss ${⊢}\left(⟨{u},{v}⟩\in \left({r}×{s}\right)\wedge \left(\left(\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to \left(\left(\exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)$
68 67 an12s ${⊢}\left(\left(\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\wedge \left(⟨{u},{v}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to \left(\left(\exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)$
69 68 expl ${⊢}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\to \left(\left(\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge \left(⟨{u},{v}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to \left(\left(\exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)\right)$
70 69 reximdv ${⊢}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\to \left(\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge \left(⟨{u},{v}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to \exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(\left(\exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)\right)$
71 59 70 syl5 ${⊢}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\to \left(\left(\forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge \exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to \exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(\left(\exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)\right)$
72 71 impl ${⊢}\left(\left(\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\wedge \exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to \exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(\left(\exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)$
73 72 reximi ${⊢}\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\left(\left(\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\wedge \exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to \exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(\left(\exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)$
74 58 73 syl ${⊢}\left(\forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\wedge \exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to \exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(\left(\exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)$
75 57 74 sylan ${⊢}\left(\left(\forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\wedge \exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to \exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(\left(\exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)$
76 reeanv ${⊢}\exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)↔\left(\exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)$
77 simpr1l ${⊢}\left(\left(\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\right)\wedge \left({r}\in {R}\wedge {s}\in {S}\right)\right)\wedge \left(\left({p}\in {a}\wedge {q}\in {b}\right)\wedge \left(\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to {p}\in {a}$
78 simpr1r ${⊢}\left(\left(\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\right)\wedge \left({r}\in {R}\wedge {s}\in {S}\right)\right)\wedge \left(\left({p}\in {a}\wedge {q}\in {b}\right)\wedge \left(\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to {q}\in {b}$
79 eqidd ${⊢}\left(\left(\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\right)\wedge \left({r}\in {R}\wedge {s}\in {S}\right)\right)\wedge \left(\left({p}\in {a}\wedge {q}\in {b}\right)\wedge \left(\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to {p}×{q}={p}×{q}$
80 xpeq1 ${⊢}{m}={p}\to {m}×{n}={p}×{n}$
81 80 eqeq2d ${⊢}{m}={p}\to \left({p}×{q}={m}×{n}↔{p}×{q}={p}×{n}\right)$
82 xpeq2 ${⊢}{n}={q}\to {p}×{n}={p}×{q}$
83 82 eqeq2d ${⊢}{n}={q}\to \left({p}×{q}={p}×{n}↔{p}×{q}={p}×{q}\right)$
84 81 83 rspc2ev ${⊢}\left({p}\in {a}\wedge {q}\in {b}\wedge {p}×{q}={p}×{q}\right)\to \exists {m}\in {a}\phantom{\rule{.4em}{0ex}}\exists {n}\in {b}\phantom{\rule{.4em}{0ex}}{p}×{q}={m}×{n}$
85 77 78 79 84 syl3anc ${⊢}\left(\left(\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\right)\wedge \left({r}\in {R}\wedge {s}\in {S}\right)\right)\wedge \left(\left({p}\in {a}\wedge {q}\in {b}\right)\wedge \left(\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to \exists {m}\in {a}\phantom{\rule{.4em}{0ex}}\exists {n}\in {b}\phantom{\rule{.4em}{0ex}}{p}×{q}={m}×{n}$
86 vex ${⊢}{p}\in \mathrm{V}$
87 vex ${⊢}{q}\in \mathrm{V}$
88 86 87 xpex ${⊢}{p}×{q}\in \mathrm{V}$
89 eqeq1 ${⊢}{x}={p}×{q}\to \left({x}={m}×{n}↔{p}×{q}={m}×{n}\right)$
90 89 2rexbidv ${⊢}{x}={p}×{q}\to \left(\exists {m}\in {a}\phantom{\rule{.4em}{0ex}}\exists {n}\in {b}\phantom{\rule{.4em}{0ex}}{x}={m}×{n}↔\exists {m}\in {a}\phantom{\rule{.4em}{0ex}}\exists {n}\in {b}\phantom{\rule{.4em}{0ex}}{p}×{q}={m}×{n}\right)$
91 88 90 elab ${⊢}{p}×{q}\in \left\{{x}|\exists {m}\in {a}\phantom{\rule{.4em}{0ex}}\exists {n}\in {b}\phantom{\rule{.4em}{0ex}}{x}={m}×{n}\right\}↔\exists {m}\in {a}\phantom{\rule{.4em}{0ex}}\exists {n}\in {b}\phantom{\rule{.4em}{0ex}}{p}×{q}={m}×{n}$
92 85 91 sylibr ${⊢}\left(\left(\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\right)\wedge \left({r}\in {R}\wedge {s}\in {S}\right)\right)\wedge \left(\left({p}\in {a}\wedge {q}\in {b}\right)\wedge \left(\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to {p}×{q}\in \left\{{x}|\exists {m}\in {a}\phantom{\rule{.4em}{0ex}}\exists {n}\in {b}\phantom{\rule{.4em}{0ex}}{x}={m}×{n}\right\}$
93 26 rnmpo ${⊢}\mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)=\left\{{x}|\exists {m}\in {a}\phantom{\rule{.4em}{0ex}}\exists {n}\in {b}\phantom{\rule{.4em}{0ex}}{x}={m}×{n}\right\}$
94 92 93 eleqtrrdi ${⊢}\left(\left(\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\right)\wedge \left({r}\in {R}\wedge {s}\in {S}\right)\right)\wedge \left(\left({p}\in {a}\wedge {q}\in {b}\right)\wedge \left(\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to {p}×{q}\in \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)$
95 simpr2 ${⊢}\left(\left(\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\right)\wedge \left({r}\in {R}\wedge {s}\in {S}\right)\right)\wedge \left(\left({p}\in {a}\wedge {q}\in {b}\right)\wedge \left(\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to \left(\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)$
96 opelxpi ${⊢}\left({u}\in {p}\wedge {v}\in {q}\right)\to ⟨{u},{v}⟩\in \left({p}×{q}\right)$
97 96 ad2ant2r ${⊢}\left(\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\to ⟨{u},{v}⟩\in \left({p}×{q}\right)$
98 95 97 syl ${⊢}\left(\left(\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\right)\wedge \left({r}\in {R}\wedge {s}\in {S}\right)\right)\wedge \left(\left({p}\in {a}\wedge {q}\in {b}\right)\wedge \left(\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to ⟨{u},{v}⟩\in \left({p}×{q}\right)$
99 xpss12 ${⊢}\left({p}\subseteq {r}\wedge {q}\subseteq {s}\right)\to {p}×{q}\subseteq {r}×{s}$
100 99 ad2ant2l ${⊢}\left(\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\to {p}×{q}\subseteq {r}×{s}$
101 95 100 syl ${⊢}\left(\left(\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\right)\wedge \left({r}\in {R}\wedge {s}\in {S}\right)\right)\wedge \left(\left({p}\in {a}\wedge {q}\in {b}\right)\wedge \left(\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to {p}×{q}\subseteq {r}×{s}$
102 simpr3 ${⊢}\left(\left(\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\right)\wedge \left({r}\in {R}\wedge {s}\in {S}\right)\right)\wedge \left(\left({p}\in {a}\wedge {q}\in {b}\right)\wedge \left(\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to {r}×{s}\subseteq {z}$
103 101 102 sstrd ${⊢}\left(\left(\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\right)\wedge \left({r}\in {R}\wedge {s}\in {S}\right)\right)\wedge \left(\left({p}\in {a}\wedge {q}\in {b}\right)\wedge \left(\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to {p}×{q}\subseteq {z}$
104 eleq2 ${⊢}{w}={p}×{q}\to \left(⟨{u},{v}⟩\in {w}↔⟨{u},{v}⟩\in \left({p}×{q}\right)\right)$
105 sseq1 ${⊢}{w}={p}×{q}\to \left({w}\subseteq {z}↔{p}×{q}\subseteq {z}\right)$
106 104 105 anbi12d ${⊢}{w}={p}×{q}\to \left(\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)↔\left(⟨{u},{v}⟩\in \left({p}×{q}\right)\wedge {p}×{q}\subseteq {z}\right)\right)$
107 106 rspcev ${⊢}\left({p}×{q}\in \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\wedge \left(⟨{u},{v}⟩\in \left({p}×{q}\right)\wedge {p}×{q}\subseteq {z}\right)\right)\to \exists {w}\in \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)$
108 94 98 103 107 syl12anc ${⊢}\left(\left(\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\right)\wedge \left({r}\in {R}\wedge {s}\in {S}\right)\right)\wedge \left(\left({p}\in {a}\wedge {q}\in {b}\right)\wedge \left(\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to \exists {w}\in \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)$
109 108 3exp2 ${⊢}\left(\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\right)\wedge \left({r}\in {R}\wedge {s}\in {S}\right)\right)\to \left(\left({p}\in {a}\wedge {q}\in {b}\right)\to \left(\left(\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\to \left({r}×{s}\subseteq {z}\to \exists {w}\in \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)\right)$
110 109 rexlimdvv ${⊢}\left(\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\right)\wedge \left({r}\in {R}\wedge {s}\in {S}\right)\right)\to \left(\exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\to \left({r}×{s}\subseteq {z}\to \exists {w}\in \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)$
111 76 110 syl5bir ${⊢}\left(\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\right)\wedge \left({r}\in {R}\wedge {s}\in {S}\right)\right)\to \left(\left(\exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\to \left({r}×{s}\subseteq {z}\to \exists {w}\in \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)$
112 111 impd ${⊢}\left(\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\right)\wedge \left({r}\in {R}\wedge {s}\in {S}\right)\right)\to \left(\left(\left(\exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)\to \exists {w}\in \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)$
113 112 rexlimdvva ${⊢}\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\right)\to \left(\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(\left(\exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\wedge \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\wedge {r}×{s}\subseteq {z}\right)\to \exists {w}\in \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)$
114 75 113 syl5 ${⊢}\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\right)\to \left(\left(\left(\forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\wedge \exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)\right)\to \exists {w}\in \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)$
115 114 expd ${⊢}\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\right)\to \left(\left(\forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\to \left(\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)\to \exists {w}\in \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)$
116 115 impr ${⊢}\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left(\left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\wedge \left(\forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\right)\right)\to \left(\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)\to \exists {w}\in \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)$
117 56 116 syl9r ${⊢}\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left(\left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\wedge \left(\forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\right)\right)\to \left(\forall {w}\in {z}\phantom{\rule{.4em}{0ex}}\exists {r}\in {R}\phantom{\rule{.4em}{0ex}}\exists {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({w}\in \left({r}×{s}\right)\wedge {r}×{s}\subseteq {z}\right)\to \left(⟨{u},{v}⟩\in {z}\to \exists {w}\in \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)$
118 52 117 sylbid ${⊢}\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left(\left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\wedge \left(\forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\right)\right)\to \left({z}\in \left({R}{×}_{t}{S}\right)\to \left(⟨{u},{v}⟩\in {z}\to \exists {w}\in \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)$
119 118 ralrimiv ${⊢}\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left(\left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\wedge \left(\forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\right)\right)\to \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {z}\to \exists {w}\in \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)$
120 breq1 ${⊢}{y}=\mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\to \left({y}\preccurlyeq \mathrm{\omega }↔\mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\preccurlyeq \mathrm{\omega }\right)$
121 rexeq ${⊢}{y}=\mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\to \left(\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)↔\exists {w}\in \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)$
122 121 imbi2d ${⊢}{y}=\mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\to \left(\left(⟨{u},{v}⟩\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)↔\left(⟨{u},{v}⟩\in {z}\to \exists {w}\in \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)$
123 122 ralbidv ${⊢}{y}=\mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\to \left(\forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)↔\forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {z}\to \exists {w}\in \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)$
124 120 123 anbi12d ${⊢}{y}=\mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\to \left(\left({y}\preccurlyeq \mathrm{\omega }\wedge \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)↔\left(\mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\preccurlyeq \mathrm{\omega }\wedge \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {z}\to \exists {w}\in \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)\right)$
125 124 rspcev ${⊢}\left(\mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\in 𝒫\left({R}{×}_{t}{S}\right)\wedge \left(\mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\preccurlyeq \mathrm{\omega }\wedge \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {z}\to \exists {w}\in \mathrm{ran}\left({m}\in {a},{n}\in {b}⟼{m}×{n}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)\right)\to \exists {y}\in 𝒫\left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({y}\preccurlyeq \mathrm{\omega }\wedge \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)$
126 33 48 119 125 syl12anc ${⊢}\left(\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\wedge \left(\left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\wedge \left(\forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\right)\right)\to \exists {y}\in 𝒫\left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({y}\preccurlyeq \mathrm{\omega }\wedge \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)$
127 126 ex ${⊢}\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\to \left(\left(\left({a}\preccurlyeq \mathrm{\omega }\wedge {b}\preccurlyeq \mathrm{\omega }\right)\wedge \left(\forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\right)\to \exists {y}\in 𝒫\left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({y}\preccurlyeq \mathrm{\omega }\wedge \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)\right)$
128 12 127 syl5bi ${⊢}\left(\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\wedge \left({a}\in 𝒫{R}\wedge {b}\in 𝒫{S}\right)\right)\to \left(\left(\left({a}\preccurlyeq \mathrm{\omega }\wedge \forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\right)\wedge \left({b}\preccurlyeq \mathrm{\omega }\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\right)\to \exists {y}\in 𝒫\left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({y}\preccurlyeq \mathrm{\omega }\wedge \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)\right)$
129 128 rexlimdvva ${⊢}\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\to \left(\exists {a}\in 𝒫{R}\phantom{\rule{.4em}{0ex}}\exists {b}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left(\left({a}\preccurlyeq \mathrm{\omega }\wedge \forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\right)\wedge \left({b}\preccurlyeq \mathrm{\omega }\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\right)\to \exists {y}\in 𝒫\left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({y}\preccurlyeq \mathrm{\omega }\wedge \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)\right)$
130 11 129 syl5bir ${⊢}\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\to \left(\left(\exists {a}\in 𝒫{R}\phantom{\rule{.4em}{0ex}}\left({a}\preccurlyeq \mathrm{\omega }\wedge \forall {r}\in {R}\phantom{\rule{.4em}{0ex}}\left({u}\in {r}\to \exists {p}\in {a}\phantom{\rule{.4em}{0ex}}\left({u}\in {p}\wedge {p}\subseteq {r}\right)\right)\right)\wedge \exists {b}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({b}\preccurlyeq \mathrm{\omega }\wedge \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}\left({v}\in {s}\to \exists {q}\in {b}\phantom{\rule{.4em}{0ex}}\left({v}\in {q}\wedge {q}\subseteq {s}\right)\right)\right)\right)\to \exists {y}\in 𝒫\left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({y}\preccurlyeq \mathrm{\omega }\wedge \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)\right)$
131 7 10 130 mp2and ${⊢}\left(\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\wedge \left({u}\in \bigcup {R}\wedge {v}\in \bigcup {S}\right)\right)\to \exists {y}\in 𝒫\left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({y}\preccurlyeq \mathrm{\omega }\wedge \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)$
132 131 ralrimivva ${⊢}\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\to \forall {u}\in \bigcup {R}\phantom{\rule{.4em}{0ex}}\forall {v}\in \bigcup {S}\phantom{\rule{.4em}{0ex}}\exists {y}\in 𝒫\left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({y}\preccurlyeq \mathrm{\omega }\wedge \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)$
133 eleq1 ${⊢}{x}=⟨{u},{v}⟩\to \left({x}\in {z}↔⟨{u},{v}⟩\in {z}\right)$
134 eleq1 ${⊢}{x}=⟨{u},{v}⟩\to \left({x}\in {w}↔⟨{u},{v}⟩\in {w}\right)$
135 134 anbi1d ${⊢}{x}=⟨{u},{v}⟩\to \left(\left({x}\in {w}\wedge {w}\subseteq {z}\right)↔\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)$
136 135 rexbidv ${⊢}{x}=⟨{u},{v}⟩\to \left(\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {w}\subseteq {z}\right)↔\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)$
137 133 136 imbi12d ${⊢}{x}=⟨{u},{v}⟩\to \left(\left({x}\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {w}\subseteq {z}\right)\right)↔\left(⟨{u},{v}⟩\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)$
138 137 ralbidv ${⊢}{x}=⟨{u},{v}⟩\to \left(\forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {w}\subseteq {z}\right)\right)↔\forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)$
139 138 anbi2d ${⊢}{x}=⟨{u},{v}⟩\to \left(\left({y}\preccurlyeq \mathrm{\omega }\wedge \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {w}\subseteq {z}\right)\right)\right)↔\left({y}\preccurlyeq \mathrm{\omega }\wedge \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)\right)$
140 139 rexbidv ${⊢}{x}=⟨{u},{v}⟩\to \left(\exists {y}\in 𝒫\left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({y}\preccurlyeq \mathrm{\omega }\wedge \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {w}\subseteq {z}\right)\right)\right)↔\exists {y}\in 𝒫\left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({y}\preccurlyeq \mathrm{\omega }\wedge \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)\right)$
141 140 ralxp ${⊢}\forall {x}\in \left(\bigcup {R}×\bigcup {S}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in 𝒫\left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({y}\preccurlyeq \mathrm{\omega }\wedge \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {w}\subseteq {z}\right)\right)\right)↔\forall {u}\in \bigcup {R}\phantom{\rule{.4em}{0ex}}\forall {v}\in \bigcup {S}\phantom{\rule{.4em}{0ex}}\exists {y}\in 𝒫\left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({y}\preccurlyeq \mathrm{\omega }\wedge \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left(⟨{u},{v}⟩\in {w}\wedge {w}\subseteq {z}\right)\right)\right)$
142 132 141 sylibr ${⊢}\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\to \forall {x}\in \left(\bigcup {R}×\bigcup {S}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in 𝒫\left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({y}\preccurlyeq \mathrm{\omega }\wedge \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {w}\subseteq {z}\right)\right)\right)$
143 5 8 txuni ${⊢}\left({R}\in \mathrm{Top}\wedge {S}\in \mathrm{Top}\right)\to \bigcup {R}×\bigcup {S}=\bigcup \left({R}{×}_{t}{S}\right)$
144 1 2 143 syl2an ${⊢}\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\to \bigcup {R}×\bigcup {S}=\bigcup \left({R}{×}_{t}{S}\right)$
145 144 raleqdv ${⊢}\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\to \left(\forall {x}\in \left(\bigcup {R}×\bigcup {S}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in 𝒫\left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({y}\preccurlyeq \mathrm{\omega }\wedge \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {w}\subseteq {z}\right)\right)\right)↔\forall {x}\in \bigcup \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in 𝒫\left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({y}\preccurlyeq \mathrm{\omega }\wedge \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {w}\subseteq {z}\right)\right)\right)\right)$
146 142 145 mpbid ${⊢}\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\to \forall {x}\in \bigcup \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in 𝒫\left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({y}\preccurlyeq \mathrm{\omega }\wedge \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {w}\subseteq {z}\right)\right)\right)$
147 eqid ${⊢}\bigcup \left({R}{×}_{t}{S}\right)=\bigcup \left({R}{×}_{t}{S}\right)$
148 147 is1stc2 ${⊢}{R}{×}_{t}{S}\in {1}^{st}𝜔↔\left({R}{×}_{t}{S}\in \mathrm{Top}\wedge \forall {x}\in \bigcup \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\exists {y}\in 𝒫\left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({y}\preccurlyeq \mathrm{\omega }\wedge \forall {z}\in \left({R}{×}_{t}{S}\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {z}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {w}\subseteq {z}\right)\right)\right)\right)$
149 4 146 148 sylanbrc ${⊢}\left({R}\in {1}^{st}𝜔\wedge {S}\in {1}^{st}𝜔\right)\to {R}{×}_{t}{S}\in {1}^{st}𝜔$