# Metamath Proof Explorer

## Theorem eltg2b

Description: Membership in a topology generated by a basis. (Contributed by Mario Carneiro, 17-Jun-2014) (Revised by Mario Carneiro, 10-Jan-2015)

Ref Expression
Assertion eltg2b ${⊢}{B}\in {V}\to \left({A}\in \mathrm{topGen}\left({B}\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)$

### Proof

Step Hyp Ref Expression
1 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)$
2 simpl ${⊢}\left({x}\in {y}\wedge {y}\subseteq {A}\right)\to {x}\in {y}$
3 2 reximi ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {A}\right)\to \exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\in {y}$
4 eluni2 ${⊢}{x}\in \bigcup {B}↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}\in {y}$
5 3 4 sylibr ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\subseteq {A}\right)\to {x}\in \bigcup {B}$
6 5 ralimi ${⊢}\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)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\in \bigcup {B}$
7 dfss3 ${⊢}{A}\subseteq \bigcup {B}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\in \bigcup {B}$
8 6 7 sylibr ${⊢}\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)\to {A}\subseteq \bigcup {B}$
9 8 pm4.71ri ${⊢}\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)↔\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)$
10 1 9 syl6bbr ${⊢}{B}\in {V}\to \left({A}\in \mathrm{topGen}\left({B}\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)$