# Metamath Proof Explorer

## Theorem 2ndcctbss

Description: If a topology is second-countable, every base has a countable subset which is a base. Exercise 16B2 in Willard. (Contributed by Jeff Hankins, 28-Jan-2010) (Proof shortened by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypotheses 2ndcctbss.1 ${⊢}{J}=\mathrm{topGen}\left({B}\right)$
2ndcctbss.2 ${⊢}{S}=\left\{⟨{u},{v}⟩|\left({u}\in {c}\wedge {v}\in {c}\wedge \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {w}\wedge {w}\subseteq {v}\right)\right)\right\}$
Assertion 2ndcctbss ${⊢}\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\to \exists {b}\in \mathrm{TopBases}\phantom{\rule{.4em}{0ex}}\left({b}\preccurlyeq \mathrm{\omega }\wedge {b}\subseteq {B}\wedge {J}=\mathrm{topGen}\left({b}\right)\right)$

### Proof

Step Hyp Ref Expression
1 2ndcctbss.1 ${⊢}{J}=\mathrm{topGen}\left({B}\right)$
2 2ndcctbss.2 ${⊢}{S}=\left\{⟨{u},{v}⟩|\left({u}\in {c}\wedge {v}\in {c}\wedge \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {w}\wedge {w}\subseteq {v}\right)\right)\right\}$
3 simpr ${⊢}\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\to {J}\in {2}^{nd}𝜔$
4 is2ndc ${⊢}{J}\in {2}^{nd}𝜔↔\exists {c}\in \mathrm{TopBases}\phantom{\rule{.4em}{0ex}}\left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)$
5 3 4 sylib ${⊢}\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\to \exists {c}\in \mathrm{TopBases}\phantom{\rule{.4em}{0ex}}\left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)$
6 vex ${⊢}{c}\in \mathrm{V}$
7 6 6 xpex ${⊢}{c}×{c}\in \mathrm{V}$
8 3simpa ${⊢}\left({u}\in {c}\wedge {v}\in {c}\wedge \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {w}\wedge {w}\subseteq {v}\right)\right)\to \left({u}\in {c}\wedge {v}\in {c}\right)$
9 8 ssopab2i ${⊢}\left\{⟨{u},{v}⟩|\left({u}\in {c}\wedge {v}\in {c}\wedge \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {w}\wedge {w}\subseteq {v}\right)\right)\right\}\subseteq \left\{⟨{u},{v}⟩|\left({u}\in {c}\wedge {v}\in {c}\right)\right\}$
10 df-xp ${⊢}{c}×{c}=\left\{⟨{u},{v}⟩|\left({u}\in {c}\wedge {v}\in {c}\right)\right\}$
11 9 2 10 3sstr4i ${⊢}{S}\subseteq {c}×{c}$
12 ssdomg ${⊢}{c}×{c}\in \mathrm{V}\to \left({S}\subseteq {c}×{c}\to {S}\preccurlyeq \left({c}×{c}\right)\right)$
13 7 11 12 mp2 ${⊢}{S}\preccurlyeq \left({c}×{c}\right)$
14 6 xpdom1 ${⊢}{c}\preccurlyeq \mathrm{\omega }\to \left({c}×{c}\right)\preccurlyeq \left(\mathrm{\omega }×{c}\right)$
15 omex ${⊢}\mathrm{\omega }\in \mathrm{V}$
16 15 xpdom2 ${⊢}{c}\preccurlyeq \mathrm{\omega }\to \left(\mathrm{\omega }×{c}\right)\preccurlyeq \left(\mathrm{\omega }×\mathrm{\omega }\right)$
17 domtr ${⊢}\left(\left({c}×{c}\right)\preccurlyeq \left(\mathrm{\omega }×{c}\right)\wedge \left(\mathrm{\omega }×{c}\right)\preccurlyeq \left(\mathrm{\omega }×\mathrm{\omega }\right)\right)\to \left({c}×{c}\right)\preccurlyeq \left(\mathrm{\omega }×\mathrm{\omega }\right)$
18 14 16 17 syl2anc ${⊢}{c}\preccurlyeq \mathrm{\omega }\to \left({c}×{c}\right)\preccurlyeq \left(\mathrm{\omega }×\mathrm{\omega }\right)$
19 xpomen ${⊢}\left(\mathrm{\omega }×\mathrm{\omega }\right)\approx \mathrm{\omega }$
20 domentr ${⊢}\left(\left({c}×{c}\right)\preccurlyeq \left(\mathrm{\omega }×\mathrm{\omega }\right)\wedge \left(\mathrm{\omega }×\mathrm{\omega }\right)\approx \mathrm{\omega }\right)\to \left({c}×{c}\right)\preccurlyeq \mathrm{\omega }$
21 18 19 20 sylancl ${⊢}{c}\preccurlyeq \mathrm{\omega }\to \left({c}×{c}\right)\preccurlyeq \mathrm{\omega }$
22 21 adantr ${⊢}\left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\to \left({c}×{c}\right)\preccurlyeq \mathrm{\omega }$
23 22 ad2antll ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\to \left({c}×{c}\right)\preccurlyeq \mathrm{\omega }$
24 domtr ${⊢}\left({S}\preccurlyeq \left({c}×{c}\right)\wedge \left({c}×{c}\right)\preccurlyeq \mathrm{\omega }\right)\to {S}\preccurlyeq \mathrm{\omega }$
25 13 23 24 sylancr ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\to {S}\preccurlyeq \mathrm{\omega }$
26 2 relopabi ${⊢}\mathrm{Rel}{S}$
27 simpr ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge {x}\in {S}\right)\to {x}\in {S}$
28 1st2nd ${⊢}\left(\mathrm{Rel}{S}\wedge {x}\in {S}\right)\to {x}=⟨{1}^{st}\left({x}\right),{2}^{nd}\left({x}\right)⟩$
29 26 27 28 sylancr ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge {x}\in {S}\right)\to {x}=⟨{1}^{st}\left({x}\right),{2}^{nd}\left({x}\right)⟩$
30 29 27 eqeltrrd ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge {x}\in {S}\right)\to ⟨{1}^{st}\left({x}\right),{2}^{nd}\left({x}\right)⟩\in {S}$
31 df-br ${⊢}{1}^{st}\left({x}\right){S}{2}^{nd}\left({x}\right)↔⟨{1}^{st}\left({x}\right),{2}^{nd}\left({x}\right)⟩\in {S}$
32 fvex ${⊢}{1}^{st}\left({x}\right)\in \mathrm{V}$
33 fvex ${⊢}{2}^{nd}\left({x}\right)\in \mathrm{V}$
34 simpl ${⊢}\left({u}={1}^{st}\left({x}\right)\wedge {v}={2}^{nd}\left({x}\right)\right)\to {u}={1}^{st}\left({x}\right)$
35 34 eleq1d ${⊢}\left({u}={1}^{st}\left({x}\right)\wedge {v}={2}^{nd}\left({x}\right)\right)\to \left({u}\in {c}↔{1}^{st}\left({x}\right)\in {c}\right)$
36 simpr ${⊢}\left({u}={1}^{st}\left({x}\right)\wedge {v}={2}^{nd}\left({x}\right)\right)\to {v}={2}^{nd}\left({x}\right)$
37 36 eleq1d ${⊢}\left({u}={1}^{st}\left({x}\right)\wedge {v}={2}^{nd}\left({x}\right)\right)\to \left({v}\in {c}↔{2}^{nd}\left({x}\right)\in {c}\right)$
38 sseq1 ${⊢}{u}={1}^{st}\left({x}\right)\to \left({u}\subseteq {w}↔{1}^{st}\left({x}\right)\subseteq {w}\right)$
39 sseq2 ${⊢}{v}={2}^{nd}\left({x}\right)\to \left({w}\subseteq {v}↔{w}\subseteq {2}^{nd}\left({x}\right)\right)$
40 38 39 bi2anan9 ${⊢}\left({u}={1}^{st}\left({x}\right)\wedge {v}={2}^{nd}\left({x}\right)\right)\to \left(\left({u}\subseteq {w}\wedge {w}\subseteq {v}\right)↔\left({1}^{st}\left({x}\right)\subseteq {w}\wedge {w}\subseteq {2}^{nd}\left({x}\right)\right)\right)$
41 40 rexbidv ${⊢}\left({u}={1}^{st}\left({x}\right)\wedge {v}={2}^{nd}\left({x}\right)\right)\to \left(\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {w}\wedge {w}\subseteq {v}\right)↔\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {w}\wedge {w}\subseteq {2}^{nd}\left({x}\right)\right)\right)$
42 35 37 41 3anbi123d ${⊢}\left({u}={1}^{st}\left({x}\right)\wedge {v}={2}^{nd}\left({x}\right)\right)\to \left(\left({u}\in {c}\wedge {v}\in {c}\wedge \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {w}\wedge {w}\subseteq {v}\right)\right)↔\left({1}^{st}\left({x}\right)\in {c}\wedge {2}^{nd}\left({x}\right)\in {c}\wedge \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {w}\wedge {w}\subseteq {2}^{nd}\left({x}\right)\right)\right)\right)$
43 32 33 42 2 braba ${⊢}{1}^{st}\left({x}\right){S}{2}^{nd}\left({x}\right)↔\left({1}^{st}\left({x}\right)\in {c}\wedge {2}^{nd}\left({x}\right)\in {c}\wedge \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {w}\wedge {w}\subseteq {2}^{nd}\left({x}\right)\right)\right)$
44 31 43 bitr3i ${⊢}⟨{1}^{st}\left({x}\right),{2}^{nd}\left({x}\right)⟩\in {S}↔\left({1}^{st}\left({x}\right)\in {c}\wedge {2}^{nd}\left({x}\right)\in {c}\wedge \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {w}\wedge {w}\subseteq {2}^{nd}\left({x}\right)\right)\right)$
45 44 simp3bi ${⊢}⟨{1}^{st}\left({x}\right),{2}^{nd}\left({x}\right)⟩\in {S}\to \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {w}\wedge {w}\subseteq {2}^{nd}\left({x}\right)\right)$
46 30 45 syl ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge {x}\in {S}\right)\to \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {w}\wedge {w}\subseteq {2}^{nd}\left({x}\right)\right)$
47 fvi ${⊢}{B}\in \mathrm{TopBases}\to \mathrm{I}\left({B}\right)={B}$
48 47 ad3antrrr ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge {x}\in {S}\right)\to \mathrm{I}\left({B}\right)={B}$
49 48 rexeqdv ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge {x}\in {S}\right)\to \left(\exists {w}\in \mathrm{I}\left({B}\right)\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {w}\wedge {w}\subseteq {2}^{nd}\left({x}\right)\right)↔\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {w}\wedge {w}\subseteq {2}^{nd}\left({x}\right)\right)\right)$
50 46 49 mpbird ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge {x}\in {S}\right)\to \exists {w}\in \mathrm{I}\left({B}\right)\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {w}\wedge {w}\subseteq {2}^{nd}\left({x}\right)\right)$
51 50 ralrimiva ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\to \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\exists {w}\in \mathrm{I}\left({B}\right)\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {w}\wedge {w}\subseteq {2}^{nd}\left({x}\right)\right)$
52 fvex ${⊢}\mathrm{I}\left({B}\right)\in \mathrm{V}$
53 sseq2 ${⊢}{w}={f}\left({x}\right)\to \left({1}^{st}\left({x}\right)\subseteq {w}↔{1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\right)$
54 sseq1 ${⊢}{w}={f}\left({x}\right)\to \left({w}\subseteq {2}^{nd}\left({x}\right)↔{f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)$
55 53 54 anbi12d ${⊢}{w}={f}\left({x}\right)\to \left(\left({1}^{st}\left({x}\right)\subseteq {w}\wedge {w}\subseteq {2}^{nd}\left({x}\right)\right)↔\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)$
56 52 55 axcc4dom ${⊢}\left({S}\preccurlyeq \mathrm{\omega }\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\exists {w}\in \mathrm{I}\left({B}\right)\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {w}\wedge {w}\subseteq {2}^{nd}\left({x}\right)\right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{S}⟶\mathrm{I}\left({B}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)$
57 25 51 56 syl2anc ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{S}⟶\mathrm{I}\left({B}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)$
58 47 ad2antrr ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\to \mathrm{I}\left({B}\right)={B}$
59 58 feq3d ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\to \left({f}:{S}⟶\mathrm{I}\left({B}\right)↔{f}:{S}⟶{B}\right)$
60 59 anbi1d ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\to \left(\left({f}:{S}⟶\mathrm{I}\left({B}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)↔\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\right)$
61 2ndctop ${⊢}{J}\in {2}^{nd}𝜔\to {J}\in \mathrm{Top}$
62 61 adantl ${⊢}\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\to {J}\in \mathrm{Top}$
63 62 ad2antrr ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\right)\to {J}\in \mathrm{Top}$
64 frn ${⊢}{f}:{S}⟶{B}\to \mathrm{ran}{f}\subseteq {B}$
65 64 ad2antrl ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\right)\to \mathrm{ran}{f}\subseteq {B}$
66 bastg ${⊢}{B}\in \mathrm{TopBases}\to {B}\subseteq \mathrm{topGen}\left({B}\right)$
67 66 ad3antrrr ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\right)\to {B}\subseteq \mathrm{topGen}\left({B}\right)$
68 67 1 sseqtrrdi ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\right)\to {B}\subseteq {J}$
69 65 68 sstrd ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\right)\to \mathrm{ran}{f}\subseteq {J}$
70 simprrl ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\to {o}\in {J}$
71 simprr ${⊢}\left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\to \mathrm{topGen}\left({c}\right)={J}$
72 71 ad2antlr ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\to \mathrm{topGen}\left({c}\right)={J}$
73 70 72 eleqtrrd ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\to {o}\in \mathrm{topGen}\left({c}\right)$
74 simprrr ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\to {t}\in {o}$
75 tg2 ${⊢}\left({o}\in \mathrm{topGen}\left({c}\right)\wedge {t}\in {o}\right)\to \exists {d}\in {c}\phantom{\rule{.4em}{0ex}}\left({t}\in {d}\wedge {d}\subseteq {o}\right)$
76 73 74 75 syl2anc ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\to \exists {d}\in {c}\phantom{\rule{.4em}{0ex}}\left({t}\in {d}\wedge {d}\subseteq {o}\right)$
77 bastg ${⊢}{c}\in \mathrm{TopBases}\to {c}\subseteq \mathrm{topGen}\left({c}\right)$
78 77 ad2antrl ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\to {c}\subseteq \mathrm{topGen}\left({c}\right)$
79 78 ad2antrr ${⊢}\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\to {c}\subseteq \mathrm{topGen}\left({c}\right)$
80 1 eqeq2i ${⊢}\mathrm{topGen}\left({c}\right)={J}↔\mathrm{topGen}\left({c}\right)=\mathrm{topGen}\left({B}\right)$
81 80 biimpi ${⊢}\mathrm{topGen}\left({c}\right)={J}\to \mathrm{topGen}\left({c}\right)=\mathrm{topGen}\left({B}\right)$
82 81 adantl ${⊢}\left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\to \mathrm{topGen}\left({c}\right)=\mathrm{topGen}\left({B}\right)$
83 82 ad2antll ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\to \mathrm{topGen}\left({c}\right)=\mathrm{topGen}\left({B}\right)$
84 83 ad2antrr ${⊢}\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\to \mathrm{topGen}\left({c}\right)=\mathrm{topGen}\left({B}\right)$
85 79 84 sseqtrd ${⊢}\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\to {c}\subseteq \mathrm{topGen}\left({B}\right)$
86 simprl ${⊢}\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\to {d}\in {c}$
87 85 86 sseldd ${⊢}\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\to {d}\in \mathrm{topGen}\left({B}\right)$
88 simprrl ${⊢}\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\to {t}\in {d}$
89 tg2 ${⊢}\left({d}\in \mathrm{topGen}\left({B}\right)\wedge {t}\in {d}\right)\to \exists {m}\in {B}\phantom{\rule{.4em}{0ex}}\left({t}\in {m}\wedge {m}\subseteq {d}\right)$
90 87 88 89 syl2anc ${⊢}\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\to \exists {m}\in {B}\phantom{\rule{.4em}{0ex}}\left({t}\in {m}\wedge {m}\subseteq {d}\right)$
91 66 ad3antrrr ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\to {B}\subseteq \mathrm{topGen}\left({B}\right)$
92 91 ad2antrr ${⊢}\left(\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\to {B}\subseteq \mathrm{topGen}\left({B}\right)$
93 72 ad2antrr ${⊢}\left(\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\to \mathrm{topGen}\left({c}\right)={J}$
94 93 1 syl6req ${⊢}\left(\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\to \mathrm{topGen}\left({B}\right)=\mathrm{topGen}\left({c}\right)$
95 92 94 sseqtrd ${⊢}\left(\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\to {B}\subseteq \mathrm{topGen}\left({c}\right)$
96 simprl ${⊢}\left(\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\to {m}\in {B}$
97 95 96 sseldd ${⊢}\left(\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\to {m}\in \mathrm{topGen}\left({c}\right)$
98 simprrl ${⊢}\left(\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\to {t}\in {m}$
99 tg2 ${⊢}\left({m}\in \mathrm{topGen}\left({c}\right)\wedge {t}\in {m}\right)\to \exists {n}\in {c}\phantom{\rule{.4em}{0ex}}\left({t}\in {n}\wedge {n}\subseteq {m}\right)$
100 97 98 99 syl2anc ${⊢}\left(\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\to \exists {n}\in {c}\phantom{\rule{.4em}{0ex}}\left({t}\in {n}\wedge {n}\subseteq {m}\right)$
101 ffn ${⊢}{f}:{S}⟶{B}\to {f}Fn{S}$
102 101 ad2antrr ${⊢}\left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\to {f}Fn{S}$
103 102 ad2antlr ${⊢}\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\to {f}Fn{S}$
104 103 ad2antrr ${⊢}\left(\left(\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\to {f}Fn{S}$
105 simprl ${⊢}\left(\left(\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\to {n}\in {c}$
106 86 ad2antrr ${⊢}\left(\left(\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\to {d}\in {c}$
107 simplrl ${⊢}\left(\left(\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\to {m}\in {B}$
108 simprrr ${⊢}\left(\left(\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\to {n}\subseteq {m}$
109 simprr ${⊢}\left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\to {m}\subseteq {d}$
110 109 ad2antlr ${⊢}\left(\left(\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\to {m}\subseteq {d}$
111 sseq2 ${⊢}{w}={m}\to \left({n}\subseteq {w}↔{n}\subseteq {m}\right)$
112 sseq1 ${⊢}{w}={m}\to \left({w}\subseteq {d}↔{m}\subseteq {d}\right)$
113 111 112 anbi12d ${⊢}{w}={m}\to \left(\left({n}\subseteq {w}\wedge {w}\subseteq {d}\right)↔\left({n}\subseteq {m}\wedge {m}\subseteq {d}\right)\right)$
114 113 rspcev ${⊢}\left({m}\in {B}\wedge \left({n}\subseteq {m}\wedge {m}\subseteq {d}\right)\right)\to \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({n}\subseteq {w}\wedge {w}\subseteq {d}\right)$
115 107 108 110 114 syl12anc ${⊢}\left(\left(\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\to \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({n}\subseteq {w}\wedge {w}\subseteq {d}\right)$
116 df-br ${⊢}{n}{S}{d}↔⟨{n},{d}⟩\in {S}$
117 vex ${⊢}{n}\in \mathrm{V}$
118 vex ${⊢}{d}\in \mathrm{V}$
119 simpl ${⊢}\left({u}={n}\wedge {v}={d}\right)\to {u}={n}$
120 119 eleq1d ${⊢}\left({u}={n}\wedge {v}={d}\right)\to \left({u}\in {c}↔{n}\in {c}\right)$
121 simpr ${⊢}\left({u}={n}\wedge {v}={d}\right)\to {v}={d}$
122 121 eleq1d ${⊢}\left({u}={n}\wedge {v}={d}\right)\to \left({v}\in {c}↔{d}\in {c}\right)$
123 sseq1 ${⊢}{u}={n}\to \left({u}\subseteq {w}↔{n}\subseteq {w}\right)$
124 sseq2 ${⊢}{v}={d}\to \left({w}\subseteq {v}↔{w}\subseteq {d}\right)$
125 123 124 bi2anan9 ${⊢}\left({u}={n}\wedge {v}={d}\right)\to \left(\left({u}\subseteq {w}\wedge {w}\subseteq {v}\right)↔\left({n}\subseteq {w}\wedge {w}\subseteq {d}\right)\right)$
126 125 rexbidv ${⊢}\left({u}={n}\wedge {v}={d}\right)\to \left(\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {w}\wedge {w}\subseteq {v}\right)↔\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({n}\subseteq {w}\wedge {w}\subseteq {d}\right)\right)$
127 120 122 126 3anbi123d ${⊢}\left({u}={n}\wedge {v}={d}\right)\to \left(\left({u}\in {c}\wedge {v}\in {c}\wedge \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq {w}\wedge {w}\subseteq {v}\right)\right)↔\left({n}\in {c}\wedge {d}\in {c}\wedge \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({n}\subseteq {w}\wedge {w}\subseteq {d}\right)\right)\right)$
128 117 118 127 2 braba ${⊢}{n}{S}{d}↔\left({n}\in {c}\wedge {d}\in {c}\wedge \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({n}\subseteq {w}\wedge {w}\subseteq {d}\right)\right)$
129 116 128 bitr3i ${⊢}⟨{n},{d}⟩\in {S}↔\left({n}\in {c}\wedge {d}\in {c}\wedge \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({n}\subseteq {w}\wedge {w}\subseteq {d}\right)\right)$
130 105 106 115 129 syl3anbrc ${⊢}\left(\left(\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\to ⟨{n},{d}⟩\in {S}$
131 fnfvelrn ${⊢}\left({f}Fn{S}\wedge ⟨{n},{d}⟩\in {S}\right)\to {f}\left(⟨{n},{d}⟩\right)\in \mathrm{ran}{f}$
132 104 130 131 syl2anc ${⊢}\left(\left(\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\to {f}\left(⟨{n},{d}⟩\right)\in \mathrm{ran}{f}$
133 simprl ${⊢}\left(\left(\left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\to {n}\in {c}$
134 simplll ${⊢}\left(\left(\left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\to {d}\in {c}$
135 simplrl ${⊢}\left(\left(\left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\to {m}\in {B}$
136 simprrr ${⊢}\left(\left(\left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\to {n}\subseteq {m}$
137 109 ad2antlr ${⊢}\left(\left(\left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\to {m}\subseteq {d}$
138 135 136 137 114 syl12anc ${⊢}\left(\left(\left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\to \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({n}\subseteq {w}\wedge {w}\subseteq {d}\right)$
139 133 134 138 129 syl3anbrc ${⊢}\left(\left(\left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\to ⟨{n},{d}⟩\in {S}$
140 fveq2 ${⊢}{x}=⟨{n},{d}⟩\to {1}^{st}\left({x}\right)={1}^{st}\left(⟨{n},{d}⟩\right)$
141 fveq2 ${⊢}{x}=⟨{n},{d}⟩\to {f}\left({x}\right)={f}\left(⟨{n},{d}⟩\right)$
142 140 141 sseq12d ${⊢}{x}=⟨{n},{d}⟩\to \left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)↔{1}^{st}\left(⟨{n},{d}⟩\right)\subseteq {f}\left(⟨{n},{d}⟩\right)\right)$
143 fveq2 ${⊢}{x}=⟨{n},{d}⟩\to {2}^{nd}\left({x}\right)={2}^{nd}\left(⟨{n},{d}⟩\right)$
144 141 143 sseq12d ${⊢}{x}=⟨{n},{d}⟩\to \left({f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)↔{f}\left(⟨{n},{d}⟩\right)\subseteq {2}^{nd}\left(⟨{n},{d}⟩\right)\right)$
145 142 144 anbi12d ${⊢}{x}=⟨{n},{d}⟩\to \left(\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)↔\left({1}^{st}\left(⟨{n},{d}⟩\right)\subseteq {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {2}^{nd}\left(⟨{n},{d}⟩\right)\right)\right)$
146 145 rspcv ${⊢}⟨{n},{d}⟩\in {S}\to \left(\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\to \left({1}^{st}\left(⟨{n},{d}⟩\right)\subseteq {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {2}^{nd}\left(⟨{n},{d}⟩\right)\right)\right)$
147 139 146 syl ${⊢}\left(\left(\left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\to \left(\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\to \left({1}^{st}\left(⟨{n},{d}⟩\right)\subseteq {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {2}^{nd}\left(⟨{n},{d}⟩\right)\right)\right)$
148 117 118 op1st ${⊢}{1}^{st}\left(⟨{n},{d}⟩\right)={n}$
149 148 sseq1i ${⊢}{1}^{st}\left(⟨{n},{d}⟩\right)\subseteq {f}\left(⟨{n},{d}⟩\right)↔{n}\subseteq {f}\left(⟨{n},{d}⟩\right)$
150 117 118 op2nd ${⊢}{2}^{nd}\left(⟨{n},{d}⟩\right)={d}$
151 150 sseq2i ${⊢}{f}\left(⟨{n},{d}⟩\right)\subseteq {2}^{nd}\left(⟨{n},{d}⟩\right)↔{f}\left(⟨{n},{d}⟩\right)\subseteq {d}$
152 149 151 anbi12i ${⊢}\left({1}^{st}\left(⟨{n},{d}⟩\right)\subseteq {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {2}^{nd}\left(⟨{n},{d}⟩\right)\right)↔\left({n}\subseteq {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {d}\right)$
153 simprl ${⊢}\left(\left(\left(\left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\wedge \left({n}\subseteq {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {d}\right)\right)\to {n}\subseteq {f}\left(⟨{n},{d}⟩\right)$
154 simprl ${⊢}\left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\to {t}\in {n}$
155 154 ad2antlr ${⊢}\left(\left(\left(\left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\wedge \left({n}\subseteq {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {d}\right)\right)\to {t}\in {n}$
156 153 155 sseldd ${⊢}\left(\left(\left(\left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\wedge \left({n}\subseteq {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {d}\right)\right)\to {t}\in {f}\left(⟨{n},{d}⟩\right)$
157 simprr ${⊢}\left(\left(\left(\left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\wedge \left({n}\subseteq {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {d}\right)\right)\to {f}\left(⟨{n},{d}⟩\right)\subseteq {d}$
158 simplrr ${⊢}\left(\left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\to {d}\subseteq {o}$
159 158 ad2antrr ${⊢}\left(\left(\left(\left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\wedge \left({n}\subseteq {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {d}\right)\right)\to {d}\subseteq {o}$
160 157 159 sstrd ${⊢}\left(\left(\left(\left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\wedge \left({n}\subseteq {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {d}\right)\right)\to {f}\left(⟨{n},{d}⟩\right)\subseteq {o}$
161 156 160 jca ${⊢}\left(\left(\left(\left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\wedge \left({n}\subseteq {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {d}\right)\right)\to \left({t}\in {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {o}\right)$
162 161 ex ${⊢}\left(\left(\left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\to \left(\left({n}\subseteq {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {d}\right)\to \left({t}\in {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {o}\right)\right)$
163 152 162 syl5bi ${⊢}\left(\left(\left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\to \left(\left({1}^{st}\left(⟨{n},{d}⟩\right)\subseteq {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {2}^{nd}\left(⟨{n},{d}⟩\right)\right)\to \left({t}\in {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {o}\right)\right)$
164 147 163 syldc ${⊢}\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\to \left(\left(\left(\left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\to \left({t}\in {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {o}\right)\right)$
165 164 exp4c ${⊢}\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\to \left(\left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\to \left(\left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\to \left(\left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\to \left({t}\in {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {o}\right)\right)\right)\right)$
166 165 ad2antlr ${⊢}\left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\to \left(\left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\to \left(\left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\to \left(\left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\to \left({t}\in {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {o}\right)\right)\right)\right)$
167 166 adantl ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\to \left(\left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\to \left(\left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\to \left(\left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\to \left({t}\in {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {o}\right)\right)\right)\right)$
168 167 imp41 ${⊢}\left(\left(\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\to \left({t}\in {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {o}\right)$
169 eleq2 ${⊢}{b}={f}\left(⟨{n},{d}⟩\right)\to \left({t}\in {b}↔{t}\in {f}\left(⟨{n},{d}⟩\right)\right)$
170 sseq1 ${⊢}{b}={f}\left(⟨{n},{d}⟩\right)\to \left({b}\subseteq {o}↔{f}\left(⟨{n},{d}⟩\right)\subseteq {o}\right)$
171 169 170 anbi12d ${⊢}{b}={f}\left(⟨{n},{d}⟩\right)\to \left(\left({t}\in {b}\wedge {b}\subseteq {o}\right)↔\left({t}\in {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {o}\right)\right)$
172 171 rspcev ${⊢}\left({f}\left(⟨{n},{d}⟩\right)\in \mathrm{ran}{f}\wedge \left({t}\in {f}\left(⟨{n},{d}⟩\right)\wedge {f}\left(⟨{n},{d}⟩\right)\subseteq {o}\right)\right)\to \exists {b}\in \mathrm{ran}{f}\phantom{\rule{.4em}{0ex}}\left({t}\in {b}\wedge {b}\subseteq {o}\right)$
173 132 168 172 syl2anc ${⊢}\left(\left(\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\wedge \left({n}\in {c}\wedge \left({t}\in {n}\wedge {n}\subseteq {m}\right)\right)\right)\to \exists {b}\in \mathrm{ran}{f}\phantom{\rule{.4em}{0ex}}\left({t}\in {b}\wedge {b}\subseteq {o}\right)$
174 100 173 rexlimddv ${⊢}\left(\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\wedge \left({m}\in {B}\wedge \left({t}\in {m}\wedge {m}\subseteq {d}\right)\right)\right)\to \exists {b}\in \mathrm{ran}{f}\phantom{\rule{.4em}{0ex}}\left({t}\in {b}\wedge {b}\subseteq {o}\right)$
175 90 174 rexlimddv ${⊢}\left(\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\wedge \left({d}\in {c}\wedge \left({t}\in {d}\wedge {d}\subseteq {o}\right)\right)\right)\to \exists {b}\in \mathrm{ran}{f}\phantom{\rule{.4em}{0ex}}\left({t}\in {b}\wedge {b}\subseteq {o}\right)$
176 76 175 rexlimddv ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\wedge \left({o}\in {J}\wedge {t}\in {o}\right)\right)\right)\to \exists {b}\in \mathrm{ran}{f}\phantom{\rule{.4em}{0ex}}\left({t}\in {b}\wedge {b}\subseteq {o}\right)$
177 176 expr ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\right)\to \left(\left({o}\in {J}\wedge {t}\in {o}\right)\to \exists {b}\in \mathrm{ran}{f}\phantom{\rule{.4em}{0ex}}\left({t}\in {b}\wedge {b}\subseteq {o}\right)\right)$
178 177 ralrimivv ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\right)\to \forall {o}\in {J}\phantom{\rule{.4em}{0ex}}\forall {t}\in {o}\phantom{\rule{.4em}{0ex}}\exists {b}\in \mathrm{ran}{f}\phantom{\rule{.4em}{0ex}}\left({t}\in {b}\wedge {b}\subseteq {o}\right)$
179 basgen2 ${⊢}\left({J}\in \mathrm{Top}\wedge \mathrm{ran}{f}\subseteq {J}\wedge \forall {o}\in {J}\phantom{\rule{.4em}{0ex}}\forall {t}\in {o}\phantom{\rule{.4em}{0ex}}\exists {b}\in \mathrm{ran}{f}\phantom{\rule{.4em}{0ex}}\left({t}\in {b}\wedge {b}\subseteq {o}\right)\right)\to \mathrm{topGen}\left(\mathrm{ran}{f}\right)={J}$
180 63 69 178 179 syl3anc ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\right)\to \mathrm{topGen}\left(\mathrm{ran}{f}\right)={J}$
181 180 63 eqeltrd ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\right)\to \mathrm{topGen}\left(\mathrm{ran}{f}\right)\in \mathrm{Top}$
182 tgclb ${⊢}\mathrm{ran}{f}\in \mathrm{TopBases}↔\mathrm{topGen}\left(\mathrm{ran}{f}\right)\in \mathrm{Top}$
183 181 182 sylibr ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\right)\to \mathrm{ran}{f}\in \mathrm{TopBases}$
184 omelon ${⊢}\mathrm{\omega }\in \mathrm{On}$
185 25 adantr ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\right)\to {S}\preccurlyeq \mathrm{\omega }$
186 ondomen ${⊢}\left(\mathrm{\omega }\in \mathrm{On}\wedge {S}\preccurlyeq \mathrm{\omega }\right)\to {S}\in \mathrm{dom}\mathrm{card}$
187 184 185 186 sylancr ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\right)\to {S}\in \mathrm{dom}\mathrm{card}$
188 101 ad2antrl ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\right)\to {f}Fn{S}$
189 dffn4 ${⊢}{f}Fn{S}↔{f}:{S}\underset{onto}{⟶}\mathrm{ran}{f}$
190 188 189 sylib ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\right)\to {f}:{S}\underset{onto}{⟶}\mathrm{ran}{f}$
191 fodomnum ${⊢}{S}\in \mathrm{dom}\mathrm{card}\to \left({f}:{S}\underset{onto}{⟶}\mathrm{ran}{f}\to \mathrm{ran}{f}\preccurlyeq {S}\right)$
192 187 190 191 sylc ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\right)\to \mathrm{ran}{f}\preccurlyeq {S}$
193 domtr ${⊢}\left(\mathrm{ran}{f}\preccurlyeq {S}\wedge {S}\preccurlyeq \mathrm{\omega }\right)\to \mathrm{ran}{f}\preccurlyeq \mathrm{\omega }$
194 192 185 193 syl2anc ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\right)\to \mathrm{ran}{f}\preccurlyeq \mathrm{\omega }$
195 180 eqcomd ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\right)\to {J}=\mathrm{topGen}\left(\mathrm{ran}{f}\right)$
196 breq1 ${⊢}{b}=\mathrm{ran}{f}\to \left({b}\preccurlyeq \mathrm{\omega }↔\mathrm{ran}{f}\preccurlyeq \mathrm{\omega }\right)$
197 sseq1 ${⊢}{b}=\mathrm{ran}{f}\to \left({b}\subseteq {B}↔\mathrm{ran}{f}\subseteq {B}\right)$
198 fveq2 ${⊢}{b}=\mathrm{ran}{f}\to \mathrm{topGen}\left({b}\right)=\mathrm{topGen}\left(\mathrm{ran}{f}\right)$
199 198 eqeq2d ${⊢}{b}=\mathrm{ran}{f}\to \left({J}=\mathrm{topGen}\left({b}\right)↔{J}=\mathrm{topGen}\left(\mathrm{ran}{f}\right)\right)$
200 196 197 199 3anbi123d ${⊢}{b}=\mathrm{ran}{f}\to \left(\left({b}\preccurlyeq \mathrm{\omega }\wedge {b}\subseteq {B}\wedge {J}=\mathrm{topGen}\left({b}\right)\right)↔\left(\mathrm{ran}{f}\preccurlyeq \mathrm{\omega }\wedge \mathrm{ran}{f}\subseteq {B}\wedge {J}=\mathrm{topGen}\left(\mathrm{ran}{f}\right)\right)\right)$
201 200 rspcev ${⊢}\left(\mathrm{ran}{f}\in \mathrm{TopBases}\wedge \left(\mathrm{ran}{f}\preccurlyeq \mathrm{\omega }\wedge \mathrm{ran}{f}\subseteq {B}\wedge {J}=\mathrm{topGen}\left(\mathrm{ran}{f}\right)\right)\right)\to \exists {b}\in \mathrm{TopBases}\phantom{\rule{.4em}{0ex}}\left({b}\preccurlyeq \mathrm{\omega }\wedge {b}\subseteq {B}\wedge {J}=\mathrm{topGen}\left({b}\right)\right)$
202 183 194 65 195 201 syl13anc ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\wedge \left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\right)\to \exists {b}\in \mathrm{TopBases}\phantom{\rule{.4em}{0ex}}\left({b}\preccurlyeq \mathrm{\omega }\wedge {b}\subseteq {B}\wedge {J}=\mathrm{topGen}\left({b}\right)\right)$
203 202 ex ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\to \left(\left({f}:{S}⟶{B}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\to \exists {b}\in \mathrm{TopBases}\phantom{\rule{.4em}{0ex}}\left({b}\preccurlyeq \mathrm{\omega }\wedge {b}\subseteq {B}\wedge {J}=\mathrm{topGen}\left({b}\right)\right)\right)$
204 60 203 sylbid ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\to \left(\left({f}:{S}⟶\mathrm{I}\left({B}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\to \exists {b}\in \mathrm{TopBases}\phantom{\rule{.4em}{0ex}}\left({b}\preccurlyeq \mathrm{\omega }\wedge {b}\subseteq {B}\wedge {J}=\mathrm{topGen}\left({b}\right)\right)\right)$
205 204 exlimdv ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{S}⟶\mathrm{I}\left({B}\right)\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({x}\right)\subseteq {f}\left({x}\right)\wedge {f}\left({x}\right)\subseteq {2}^{nd}\left({x}\right)\right)\right)\to \exists {b}\in \mathrm{TopBases}\phantom{\rule{.4em}{0ex}}\left({b}\preccurlyeq \mathrm{\omega }\wedge {b}\subseteq {B}\wedge {J}=\mathrm{topGen}\left({b}\right)\right)\right)$
206 57 205 mpd ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\wedge \left({c}\in \mathrm{TopBases}\wedge \left({c}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({c}\right)={J}\right)\right)\right)\to \exists {b}\in \mathrm{TopBases}\phantom{\rule{.4em}{0ex}}\left({b}\preccurlyeq \mathrm{\omega }\wedge {b}\subseteq {B}\wedge {J}=\mathrm{topGen}\left({b}\right)\right)$
207 5 206 rexlimddv ${⊢}\left({B}\in \mathrm{TopBases}\wedge {J}\in {2}^{nd}𝜔\right)\to \exists {b}\in \mathrm{TopBases}\phantom{\rule{.4em}{0ex}}\left({b}\preccurlyeq \mathrm{\omega }\wedge {b}\subseteq {B}\wedge {J}=\mathrm{topGen}\left({b}\right)\right)$