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 BVBtopGenB

Proof

Step Hyp Ref Expression
1 simpr BVxBxB
2 vex xV
3 2 pwid x𝒫x
4 3 a1i BVxBx𝒫x
5 1 4 elind BVxBxB𝒫x
6 elssuni xB𝒫xxB𝒫x
7 5 6 syl BVxBxB𝒫x
8 7 ex BVxBxB𝒫x
9 eltg BVxtopGenBxB𝒫x
10 8 9 sylibrd BVxBxtopGenB
11 10 ssrdv BVBtopGenB