# Metamath Proof Explorer

## Theorem tgcl

Description: Show that a basis generates a topology. Remark in Munkres p. 79. (Contributed by NM, 17-Jul-2006)

Ref Expression
Assertion tgcl ${⊢}{B}\in \mathrm{TopBases}\to \mathrm{topGen}\left({B}\right)\in \mathrm{Top}$

### Proof

Step Hyp Ref Expression
1 uniss ${⊢}{u}\subseteq \mathrm{topGen}\left({B}\right)\to \bigcup {u}\subseteq \bigcup \mathrm{topGen}\left({B}\right)$
2 1 adantl ${⊢}\left({B}\in \mathrm{TopBases}\wedge {u}\subseteq \mathrm{topGen}\left({B}\right)\right)\to \bigcup {u}\subseteq \bigcup \mathrm{topGen}\left({B}\right)$
3 unitg ${⊢}{B}\in \mathrm{TopBases}\to \bigcup \mathrm{topGen}\left({B}\right)=\bigcup {B}$
4 3 adantr ${⊢}\left({B}\in \mathrm{TopBases}\wedge {u}\subseteq \mathrm{topGen}\left({B}\right)\right)\to \bigcup \mathrm{topGen}\left({B}\right)=\bigcup {B}$
5 2 4 sseqtrd ${⊢}\left({B}\in \mathrm{TopBases}\wedge {u}\subseteq \mathrm{topGen}\left({B}\right)\right)\to \bigcup {u}\subseteq \bigcup {B}$
6 eluni2 ${⊢}{x}\in \bigcup {u}↔\exists {t}\in {u}\phantom{\rule{.4em}{0ex}}{x}\in {t}$
7 ssel2 ${⊢}\left({u}\subseteq \mathrm{topGen}\left({B}\right)\wedge {t}\in {u}\right)\to {t}\in \mathrm{topGen}\left({B}\right)$
8 eltg2b ${⊢}{B}\in \mathrm{TopBases}\to \left({t}\in \mathrm{topGen}\left({B}\right)↔\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {t}\right)\right)$
9 rsp ${⊢}\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {t}\right)\to \left({x}\in {t}\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {t}\right)\right)$
10 8 9 syl6bi ${⊢}{B}\in \mathrm{TopBases}\to \left({t}\in \mathrm{topGen}\left({B}\right)\to \left({x}\in {t}\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {t}\right)\right)\right)$
11 10 imp31 ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {t}\in \mathrm{topGen}\left({B}\right)\right)\wedge {x}\in {t}\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {t}\right)$
12 11 an32s ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {x}\in {t}\right)\wedge {t}\in \mathrm{topGen}\left({B}\right)\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {t}\right)$
13 7 12 sylan2 ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {x}\in {t}\right)\wedge \left({u}\subseteq \mathrm{topGen}\left({B}\right)\wedge {t}\in {u}\right)\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {t}\right)$
14 13 an42s ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {u}\subseteq \mathrm{topGen}\left({B}\right)\right)\wedge \left({t}\in {u}\wedge {x}\in {t}\right)\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {t}\right)$
15 elssuni ${⊢}{t}\in {u}\to {t}\subseteq \bigcup {u}$
16 sstr2 ${⊢}{y}\subseteq {t}\to \left({t}\subseteq \bigcup {u}\to {y}\subseteq \bigcup {u}\right)$
17 15 16 syl5com ${⊢}{t}\in {u}\to \left({y}\subseteq {t}\to {y}\subseteq \bigcup {u}\right)$
18 17 anim2d ${⊢}{t}\in {u}\to \left(\left({x}\in {y}\wedge {y}\subseteq {t}\right)\to \left({x}\in {y}\wedge {y}\subseteq \bigcup {u}\right)\right)$
19 18 reximdv ${⊢}{t}\in {u}\to \left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {t}\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq \bigcup {u}\right)\right)$
20 19 ad2antrl ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {u}\subseteq \mathrm{topGen}\left({B}\right)\right)\wedge \left({t}\in {u}\wedge {x}\in {t}\right)\right)\to \left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {t}\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq \bigcup {u}\right)\right)$
21 14 20 mpd ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {u}\subseteq \mathrm{topGen}\left({B}\right)\right)\wedge \left({t}\in {u}\wedge {x}\in {t}\right)\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq \bigcup {u}\right)$
22 21 rexlimdvaa ${⊢}\left({B}\in \mathrm{TopBases}\wedge {u}\subseteq \mathrm{topGen}\left({B}\right)\right)\to \left(\exists {t}\in {u}\phantom{\rule{.4em}{0ex}}{x}\in {t}\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq \bigcup {u}\right)\right)$
23 6 22 syl5bi ${⊢}\left({B}\in \mathrm{TopBases}\wedge {u}\subseteq \mathrm{topGen}\left({B}\right)\right)\to \left({x}\in \bigcup {u}\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq \bigcup {u}\right)\right)$
24 23 ralrimiv ${⊢}\left({B}\in \mathrm{TopBases}\wedge {u}\subseteq \mathrm{topGen}\left({B}\right)\right)\to \forall {x}\in \bigcup {u}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq \bigcup {u}\right)$
25 5 24 jca ${⊢}\left({B}\in \mathrm{TopBases}\wedge {u}\subseteq \mathrm{topGen}\left({B}\right)\right)\to \left(\bigcup {u}\subseteq \bigcup {B}\wedge \forall {x}\in \bigcup {u}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq \bigcup {u}\right)\right)$
26 25 ex ${⊢}{B}\in \mathrm{TopBases}\to \left({u}\subseteq \mathrm{topGen}\left({B}\right)\to \left(\bigcup {u}\subseteq \bigcup {B}\wedge \forall {x}\in \bigcup {u}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq \bigcup {u}\right)\right)\right)$
27 eltg2 ${⊢}{B}\in \mathrm{TopBases}\to \left(\bigcup {u}\in \mathrm{topGen}\left({B}\right)↔\left(\bigcup {u}\subseteq \bigcup {B}\wedge \forall {x}\in \bigcup {u}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq \bigcup {u}\right)\right)\right)$
28 26 27 sylibrd ${⊢}{B}\in \mathrm{TopBases}\to \left({u}\subseteq \mathrm{topGen}\left({B}\right)\to \bigcup {u}\in \mathrm{topGen}\left({B}\right)\right)$
29 28 alrimiv ${⊢}{B}\in \mathrm{TopBases}\to \forall {u}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq \mathrm{topGen}\left({B}\right)\to \bigcup {u}\in \mathrm{topGen}\left({B}\right)\right)$
30 inss1 ${⊢}{u}\cap {v}\subseteq {u}$
31 tg1 ${⊢}{u}\in \mathrm{topGen}\left({B}\right)\to {u}\subseteq \bigcup {B}$
32 30 31 sstrid ${⊢}{u}\in \mathrm{topGen}\left({B}\right)\to {u}\cap {v}\subseteq \bigcup {B}$
33 32 ad2antrl ${⊢}\left({B}\in \mathrm{TopBases}\wedge \left({u}\in \mathrm{topGen}\left({B}\right)\wedge {v}\in \mathrm{topGen}\left({B}\right)\right)\right)\to {u}\cap {v}\subseteq \bigcup {B}$
34 eltg2 ${⊢}{B}\in \mathrm{TopBases}\to \left({u}\in \mathrm{topGen}\left({B}\right)↔\left({u}\subseteq \bigcup {B}\wedge \forall {x}\in {u}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {z}\wedge {z}\subseteq {u}\right)\right)\right)$
35 34 simplbda ${⊢}\left({B}\in \mathrm{TopBases}\wedge {u}\in \mathrm{topGen}\left({B}\right)\right)\to \forall {x}\in {u}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {z}\wedge {z}\subseteq {u}\right)$
36 rsp ${⊢}\forall {x}\in {u}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {z}\wedge {z}\subseteq {u}\right)\to \left({x}\in {u}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {z}\wedge {z}\subseteq {u}\right)\right)$
37 35 36 syl ${⊢}\left({B}\in \mathrm{TopBases}\wedge {u}\in \mathrm{topGen}\left({B}\right)\right)\to \left({x}\in {u}\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {z}\wedge {z}\subseteq {u}\right)\right)$
38 eltg2 ${⊢}{B}\in \mathrm{TopBases}\to \left({v}\in \mathrm{topGen}\left({B}\right)↔\left({v}\subseteq \bigcup {B}\wedge \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {w}\subseteq {v}\right)\right)\right)$
39 38 simplbda ${⊢}\left({B}\in \mathrm{TopBases}\wedge {v}\in \mathrm{topGen}\left({B}\right)\right)\to \forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {w}\subseteq {v}\right)$
40 rsp ${⊢}\forall {x}\in {v}\phantom{\rule{.4em}{0ex}}\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {w}\subseteq {v}\right)\to \left({x}\in {v}\to \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {w}\subseteq {v}\right)\right)$
41 39 40 syl ${⊢}\left({B}\in \mathrm{TopBases}\wedge {v}\in \mathrm{topGen}\left({B}\right)\right)\to \left({x}\in {v}\to \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {w}\subseteq {v}\right)\right)$
42 37 41 im2anan9 ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {u}\in \mathrm{topGen}\left({B}\right)\right)\wedge \left({B}\in \mathrm{TopBases}\wedge {v}\in \mathrm{topGen}\left({B}\right)\right)\right)\to \left(\left({x}\in {u}\wedge {x}\in {v}\right)\to \left(\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {z}\wedge {z}\subseteq {u}\right)\wedge \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {w}\subseteq {v}\right)\right)\right)$
43 elin ${⊢}{x}\in \left({u}\cap {v}\right)↔\left({x}\in {u}\wedge {x}\in {v}\right)$
44 reeanv ${⊢}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {z}\wedge {z}\subseteq {u}\right)\wedge \left({x}\in {w}\wedge {w}\subseteq {v}\right)\right)↔\left(\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {z}\wedge {z}\subseteq {u}\right)\wedge \exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge {w}\subseteq {v}\right)\right)$
45 42 43 44 3imtr4g ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {u}\in \mathrm{topGen}\left({B}\right)\right)\wedge \left({B}\in \mathrm{TopBases}\wedge {v}\in \mathrm{topGen}\left({B}\right)\right)\right)\to \left({x}\in \left({u}\cap {v}\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {z}\wedge {z}\subseteq {u}\right)\wedge \left({x}\in {w}\wedge {w}\subseteq {v}\right)\right)\right)$
46 45 anandis ${⊢}\left({B}\in \mathrm{TopBases}\wedge \left({u}\in \mathrm{topGen}\left({B}\right)\wedge {v}\in \mathrm{topGen}\left({B}\right)\right)\right)\to \left({x}\in \left({u}\cap {v}\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {z}\wedge {z}\subseteq {u}\right)\wedge \left({x}\in {w}\wedge {w}\subseteq {v}\right)\right)\right)$
47 elin ${⊢}{x}\in \left({z}\cap {w}\right)↔\left({x}\in {z}\wedge {x}\in {w}\right)$
48 47 biimpri ${⊢}\left({x}\in {z}\wedge {x}\in {w}\right)\to {x}\in \left({z}\cap {w}\right)$
49 ss2in ${⊢}\left({z}\subseteq {u}\wedge {w}\subseteq {v}\right)\to {z}\cap {w}\subseteq {u}\cap {v}$
50 48 49 anim12i ${⊢}\left(\left({x}\in {z}\wedge {x}\in {w}\right)\wedge \left({z}\subseteq {u}\wedge {w}\subseteq {v}\right)\right)\to \left({x}\in \left({z}\cap {w}\right)\wedge {z}\cap {w}\subseteq {u}\cap {v}\right)$
51 50 an4s ${⊢}\left(\left({x}\in {z}\wedge {z}\subseteq {u}\right)\wedge \left({x}\in {w}\wedge {w}\subseteq {v}\right)\right)\to \left({x}\in \left({z}\cap {w}\right)\wedge {z}\cap {w}\subseteq {u}\cap {v}\right)$
52 basis2 ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {z}\in {B}\right)\wedge \left({w}\in {B}\wedge {x}\in \left({z}\cap {w}\right)\right)\right)\to \exists {t}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {t}\wedge {t}\subseteq {z}\cap {w}\right)$
53 52 adantllr ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {x}\in \left({u}\cap {v}\right)\right)\wedge {z}\in {B}\right)\wedge \left({w}\in {B}\wedge {x}\in \left({z}\cap {w}\right)\right)\right)\to \exists {t}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {t}\wedge {t}\subseteq {z}\cap {w}\right)$
54 53 adantrrr ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {x}\in \left({u}\cap {v}\right)\right)\wedge {z}\in {B}\right)\wedge \left({w}\in {B}\wedge \left({x}\in \left({z}\cap {w}\right)\wedge {z}\cap {w}\subseteq {u}\cap {v}\right)\right)\right)\to \exists {t}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {t}\wedge {t}\subseteq {z}\cap {w}\right)$
55 sstr2 ${⊢}{t}\subseteq {z}\cap {w}\to \left({z}\cap {w}\subseteq {u}\cap {v}\to {t}\subseteq {u}\cap {v}\right)$
56 55 com12 ${⊢}{z}\cap {w}\subseteq {u}\cap {v}\to \left({t}\subseteq {z}\cap {w}\to {t}\subseteq {u}\cap {v}\right)$
57 56 anim2d ${⊢}{z}\cap {w}\subseteq {u}\cap {v}\to \left(\left({x}\in {t}\wedge {t}\subseteq {z}\cap {w}\right)\to \left({x}\in {t}\wedge {t}\subseteq {u}\cap {v}\right)\right)$
58 57 reximdv ${⊢}{z}\cap {w}\subseteq {u}\cap {v}\to \left(\exists {t}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {t}\wedge {t}\subseteq {z}\cap {w}\right)\to \exists {t}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {t}\wedge {t}\subseteq {u}\cap {v}\right)\right)$
59 58 adantl ${⊢}\left({x}\in \left({z}\cap {w}\right)\wedge {z}\cap {w}\subseteq {u}\cap {v}\right)\to \left(\exists {t}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {t}\wedge {t}\subseteq {z}\cap {w}\right)\to \exists {t}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {t}\wedge {t}\subseteq {u}\cap {v}\right)\right)$
60 59 ad2antll ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {x}\in \left({u}\cap {v}\right)\right)\wedge {z}\in {B}\right)\wedge \left({w}\in {B}\wedge \left({x}\in \left({z}\cap {w}\right)\wedge {z}\cap {w}\subseteq {u}\cap {v}\right)\right)\right)\to \left(\exists {t}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {t}\wedge {t}\subseteq {z}\cap {w}\right)\to \exists {t}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {t}\wedge {t}\subseteq {u}\cap {v}\right)\right)$
61 54 60 mpd ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {x}\in \left({u}\cap {v}\right)\right)\wedge {z}\in {B}\right)\wedge \left({w}\in {B}\wedge \left({x}\in \left({z}\cap {w}\right)\wedge {z}\cap {w}\subseteq {u}\cap {v}\right)\right)\right)\to \exists {t}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {t}\wedge {t}\subseteq {u}\cap {v}\right)$
62 51 61 sylanr2 ${⊢}\left(\left(\left({B}\in \mathrm{TopBases}\wedge {x}\in \left({u}\cap {v}\right)\right)\wedge {z}\in {B}\right)\wedge \left({w}\in {B}\wedge \left(\left({x}\in {z}\wedge {z}\subseteq {u}\right)\wedge \left({x}\in {w}\wedge {w}\subseteq {v}\right)\right)\right)\right)\to \exists {t}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {t}\wedge {t}\subseteq {u}\cap {v}\right)$
63 62 rexlimdvaa ${⊢}\left(\left({B}\in \mathrm{TopBases}\wedge {x}\in \left({u}\cap {v}\right)\right)\wedge {z}\in {B}\right)\to \left(\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {z}\wedge {z}\subseteq {u}\right)\wedge \left({x}\in {w}\wedge {w}\subseteq {v}\right)\right)\to \exists {t}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {t}\wedge {t}\subseteq {u}\cap {v}\right)\right)$
64 63 rexlimdva ${⊢}\left({B}\in \mathrm{TopBases}\wedge {x}\in \left({u}\cap {v}\right)\right)\to \left(\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {z}\wedge {z}\subseteq {u}\right)\wedge \left({x}\in {w}\wedge {w}\subseteq {v}\right)\right)\to \exists {t}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {t}\wedge {t}\subseteq {u}\cap {v}\right)\right)$
65 64 ex ${⊢}{B}\in \mathrm{TopBases}\to \left({x}\in \left({u}\cap {v}\right)\to \left(\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {z}\wedge {z}\subseteq {u}\right)\wedge \left({x}\in {w}\wedge {w}\subseteq {v}\right)\right)\to \exists {t}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {t}\wedge {t}\subseteq {u}\cap {v}\right)\right)\right)$
66 65 a2d ${⊢}{B}\in \mathrm{TopBases}\to \left(\left({x}\in \left({u}\cap {v}\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {z}\wedge {z}\subseteq {u}\right)\wedge \left({x}\in {w}\wedge {w}\subseteq {v}\right)\right)\right)\to \left({x}\in \left({u}\cap {v}\right)\to \exists {t}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {t}\wedge {t}\subseteq {u}\cap {v}\right)\right)\right)$
67 66 imp ${⊢}\left({B}\in \mathrm{TopBases}\wedge \left({x}\in \left({u}\cap {v}\right)\to \exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\exists {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {z}\wedge {z}\subseteq {u}\right)\wedge \left({x}\in {w}\wedge {w}\subseteq {v}\right)\right)\right)\right)\to \left({x}\in \left({u}\cap {v}\right)\to \exists {t}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {t}\wedge {t}\subseteq {u}\cap {v}\right)\right)$
68 46 67 syldan ${⊢}\left({B}\in \mathrm{TopBases}\wedge \left({u}\in \mathrm{topGen}\left({B}\right)\wedge {v}\in \mathrm{topGen}\left({B}\right)\right)\right)\to \left({x}\in \left({u}\cap {v}\right)\to \exists {t}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {t}\wedge {t}\subseteq {u}\cap {v}\right)\right)$
69 68 ralrimiv ${⊢}\left({B}\in \mathrm{TopBases}\wedge \left({u}\in \mathrm{topGen}\left({B}\right)\wedge {v}\in \mathrm{topGen}\left({B}\right)\right)\right)\to \forall {x}\in \left({u}\cap {v}\right)\phantom{\rule{.4em}{0ex}}\exists {t}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {t}\wedge {t}\subseteq {u}\cap {v}\right)$
70 33 69 jca ${⊢}\left({B}\in \mathrm{TopBases}\wedge \left({u}\in \mathrm{topGen}\left({B}\right)\wedge {v}\in \mathrm{topGen}\left({B}\right)\right)\right)\to \left({u}\cap {v}\subseteq \bigcup {B}\wedge \forall {x}\in \left({u}\cap {v}\right)\phantom{\rule{.4em}{0ex}}\exists {t}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {t}\wedge {t}\subseteq {u}\cap {v}\right)\right)$
71 70 ex ${⊢}{B}\in \mathrm{TopBases}\to \left(\left({u}\in \mathrm{topGen}\left({B}\right)\wedge {v}\in \mathrm{topGen}\left({B}\right)\right)\to \left({u}\cap {v}\subseteq \bigcup {B}\wedge \forall {x}\in \left({u}\cap {v}\right)\phantom{\rule{.4em}{0ex}}\exists {t}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {t}\wedge {t}\subseteq {u}\cap {v}\right)\right)\right)$
72 eltg2 ${⊢}{B}\in \mathrm{TopBases}\to \left({u}\cap {v}\in \mathrm{topGen}\left({B}\right)↔\left({u}\cap {v}\subseteq \bigcup {B}\wedge \forall {x}\in \left({u}\cap {v}\right)\phantom{\rule{.4em}{0ex}}\exists {t}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {t}\wedge {t}\subseteq {u}\cap {v}\right)\right)\right)$
73 71 72 sylibrd ${⊢}{B}\in \mathrm{TopBases}\to \left(\left({u}\in \mathrm{topGen}\left({B}\right)\wedge {v}\in \mathrm{topGen}\left({B}\right)\right)\to {u}\cap {v}\in \mathrm{topGen}\left({B}\right)\right)$
74 73 ralrimivv ${⊢}{B}\in \mathrm{TopBases}\to \forall {u}\in \mathrm{topGen}\left({B}\right)\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{topGen}\left({B}\right)\phantom{\rule{.4em}{0ex}}{u}\cap {v}\in \mathrm{topGen}\left({B}\right)$
75 fvex ${⊢}\mathrm{topGen}\left({B}\right)\in \mathrm{V}$
76 istopg ${⊢}\mathrm{topGen}\left({B}\right)\in \mathrm{V}\to \left(\mathrm{topGen}\left({B}\right)\in \mathrm{Top}↔\left(\forall {u}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq \mathrm{topGen}\left({B}\right)\to \bigcup {u}\in \mathrm{topGen}\left({B}\right)\right)\wedge \forall {u}\in \mathrm{topGen}\left({B}\right)\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{topGen}\left({B}\right)\phantom{\rule{.4em}{0ex}}{u}\cap {v}\in \mathrm{topGen}\left({B}\right)\right)\right)$
77 75 76 ax-mp ${⊢}\mathrm{topGen}\left({B}\right)\in \mathrm{Top}↔\left(\forall {u}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq \mathrm{topGen}\left({B}\right)\to \bigcup {u}\in \mathrm{topGen}\left({B}\right)\right)\wedge \forall {u}\in \mathrm{topGen}\left({B}\right)\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{topGen}\left({B}\right)\phantom{\rule{.4em}{0ex}}{u}\cap {v}\in \mathrm{topGen}\left({B}\right)\right)$
78 29 74 77 sylanbrc ${⊢}{B}\in \mathrm{TopBases}\to \mathrm{topGen}\left({B}\right)\in \mathrm{Top}$