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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr | |
|
2 | vex | |
|
3 | 2 | pwid | |
4 | 3 | a1i | |
5 | 1 4 | elind | |
6 | elssuni | |
|
7 | 5 6 | syl | |
8 | 7 | ex | |
9 | eltg | |
|
10 | 8 9 | sylibrd | |
11 | 10 | ssrdv | |