# Metamath Proof Explorer

## Theorem tg2

Description: Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006)

Ref Expression
Assertion tg2 ${⊢}\left({A}\in \mathrm{topGen}\left({B}\right)\wedge {C}\in {A}\right)\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({C}\in {x}\wedge {x}\subseteq {A}\right)$

### Proof

Step Hyp Ref Expression
1 elfvdm ${⊢}{A}\in \mathrm{topGen}\left({B}\right)\to {B}\in \mathrm{dom}\mathrm{topGen}$
2 eltg2b ${⊢}{B}\in \mathrm{dom}\mathrm{topGen}\to \left({A}\in \mathrm{topGen}\left({B}\right)↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}\wedge {x}\subseteq {A}\right)\right)$
3 eleq1 ${⊢}{y}={C}\to \left({y}\in {x}↔{C}\in {x}\right)$
4 3 anbi1d ${⊢}{y}={C}\to \left(\left({y}\in {x}\wedge {x}\subseteq {A}\right)↔\left({C}\in {x}\wedge {x}\subseteq {A}\right)\right)$
5 4 rexbidv ${⊢}{y}={C}\to \left(\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}\wedge {x}\subseteq {A}\right)↔\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({C}\in {x}\wedge {x}\subseteq {A}\right)\right)$
6 5 rspccv ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}\wedge {x}\subseteq {A}\right)\to \left({C}\in {A}\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({C}\in {x}\wedge {x}\subseteq {A}\right)\right)$
7 2 6 syl6bi ${⊢}{B}\in \mathrm{dom}\mathrm{topGen}\to \left({A}\in \mathrm{topGen}\left({B}\right)\to \left({C}\in {A}\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({C}\in {x}\wedge {x}\subseteq {A}\right)\right)\right)$
8 1 7 mpcom ${⊢}{A}\in \mathrm{topGen}\left({B}\right)\to \left({C}\in {A}\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({C}\in {x}\wedge {x}\subseteq {A}\right)\right)$
9 8 imp ${⊢}\left({A}\in \mathrm{topGen}\left({B}\right)\wedge {C}\in {A}\right)\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({C}\in {x}\wedge {x}\subseteq {A}\right)$