# Metamath Proof Explorer

## Theorem eltg2

Description: Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006) (Revised by Mario Carneiro, 10-Jan-2015)

Ref Expression
Assertion eltg2 ${⊢}{B}\in {V}\to \left({A}\in \mathrm{topGen}\left({B}\right)↔\left({A}\subseteq \bigcup {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {A}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 tgval2 ${⊢}{B}\in {V}\to \mathrm{topGen}\left({B}\right)=\left\{{z}|\left({z}\subseteq \bigcup {B}\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {z}\right)\right)\right\}$
2 1 eleq2d ${⊢}{B}\in {V}\to \left({A}\in \mathrm{topGen}\left({B}\right)↔{A}\in \left\{{z}|\left({z}\subseteq \bigcup {B}\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {z}\right)\right)\right\}\right)$
3 elex ${⊢}{A}\in \left\{{z}|\left({z}\subseteq \bigcup {B}\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {z}\right)\right)\right\}\to {A}\in \mathrm{V}$
4 3 adantl ${⊢}\left({B}\in {V}\wedge {A}\in \left\{{z}|\left({z}\subseteq \bigcup {B}\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {z}\right)\right)\right\}\right)\to {A}\in \mathrm{V}$
5 uniexg ${⊢}{B}\in {V}\to \bigcup {B}\in \mathrm{V}$
6 ssexg ${⊢}\left({A}\subseteq \bigcup {B}\wedge \bigcup {B}\in \mathrm{V}\right)\to {A}\in \mathrm{V}$
7 5 6 sylan2 ${⊢}\left({A}\subseteq \bigcup {B}\wedge {B}\in {V}\right)\to {A}\in \mathrm{V}$
8 7 ancoms ${⊢}\left({B}\in {V}\wedge {A}\subseteq \bigcup {B}\right)\to {A}\in \mathrm{V}$
9 8 adantrr ${⊢}\left({B}\in {V}\wedge \left({A}\subseteq \bigcup {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {A}\right)\right)\right)\to {A}\in \mathrm{V}$
10 sseq1 ${⊢}{z}={A}\to \left({z}\subseteq \bigcup {B}↔{A}\subseteq \bigcup {B}\right)$
11 sseq2 ${⊢}{z}={A}\to \left({y}\subseteq {z}↔{y}\subseteq {A}\right)$
12 11 anbi2d ${⊢}{z}={A}\to \left(\left({x}\in {y}\wedge {y}\subseteq {z}\right)↔\left({x}\in {y}\wedge {y}\subseteq {A}\right)\right)$
13 12 rexbidv ${⊢}{z}={A}\to \left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {z}\right)↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {A}\right)\right)$
14 13 raleqbi1dv ${⊢}{z}={A}\to \left(\forall {x}\in {z}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {z}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {A}\right)\right)$
15 10 14 anbi12d ${⊢}{z}={A}\to \left(\left({z}\subseteq \bigcup {B}\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {z}\right)\right)↔\left({A}\subseteq \bigcup {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {A}\right)\right)\right)$
16 15 elabg ${⊢}{A}\in \mathrm{V}\to \left({A}\in \left\{{z}|\left({z}\subseteq \bigcup {B}\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {z}\right)\right)\right\}↔\left({A}\subseteq \bigcup {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {A}\right)\right)\right)$
17 4 9 16 pm5.21nd ${⊢}{B}\in {V}\to \left({A}\in \left\{{z}|\left({z}\subseteq \bigcup {B}\wedge \forall {x}\in {z}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {z}\right)\right)\right\}↔\left({A}\subseteq \bigcup {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {A}\right)\right)\right)$
18 2 17 bitrd ${⊢}{B}\in {V}\to \left({A}\in \mathrm{topGen}\left({B}\right)↔\left({A}\subseteq \bigcup {B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {A}\right)\right)\right)$