# Metamath Proof Explorer

## Theorem bastg

Description: A member of a basis is a subset of the topology it generates. (Contributed by NM, 16-Jul-2006) (Revised by Mario Carneiro, 10-Jan-2015)

Ref Expression
Assertion bastg ${⊢}{B}\in {V}\to {B}\subseteq \mathrm{topGen}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 simpr ${⊢}\left({B}\in {V}\wedge {x}\in {B}\right)\to {x}\in {B}$
2 vex ${⊢}{x}\in \mathrm{V}$
3 2 pwid ${⊢}{x}\in 𝒫{x}$
4 3 a1i ${⊢}\left({B}\in {V}\wedge {x}\in {B}\right)\to {x}\in 𝒫{x}$
5 1 4 elind ${⊢}\left({B}\in {V}\wedge {x}\in {B}\right)\to {x}\in \left({B}\cap 𝒫{x}\right)$
6 elssuni ${⊢}{x}\in \left({B}\cap 𝒫{x}\right)\to {x}\subseteq \bigcup \left({B}\cap 𝒫{x}\right)$
7 5 6 syl ${⊢}\left({B}\in {V}\wedge {x}\in {B}\right)\to {x}\subseteq \bigcup \left({B}\cap 𝒫{x}\right)$
8 7 ex ${⊢}{B}\in {V}\to \left({x}\in {B}\to {x}\subseteq \bigcup \left({B}\cap 𝒫{x}\right)\right)$
9 eltg ${⊢}{B}\in {V}\to \left({x}\in \mathrm{topGen}\left({B}\right)↔{x}\subseteq \bigcup \left({B}\cap 𝒫{x}\right)\right)$
10 8 9 sylibrd ${⊢}{B}\in {V}\to \left({x}\in {B}\to {x}\in \mathrm{topGen}\left({B}\right)\right)$
11 10 ssrdv ${⊢}{B}\in {V}\to {B}\subseteq \mathrm{topGen}\left({B}\right)$