Metamath Proof Explorer


Theorem bastop1

Description: A subset of a topology is a basis for the topology iff every member of the topology is a union of members of the basis. We use the idiom " ( topGenB ) = J " to express " B is a basis for topology J " since we do not have a separate notation for this. Definition 15.35 of Schechter p. 428. (Contributed by NM, 2-Feb-2008) (Proof shortened by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion bastop1 J Top B J topGen B = J x J y y B x = y

Proof

Step Hyp Ref Expression
1 tgss J Top B J topGen B topGen J
2 tgtop J Top topGen J = J
3 2 adantr J Top B J topGen J = J
4 1 3 sseqtrd J Top B J topGen B J
5 eqss topGen B = J topGen B J J topGen B
6 5 baib topGen B J topGen B = J J topGen B
7 4 6 syl J Top B J topGen B = J J topGen B
8 dfss3 J topGen B x J x topGen B
9 7 8 bitrdi J Top B J topGen B = J x J x topGen B
10 ssexg B J J Top B V
11 10 ancoms J Top B J B V
12 eltg3 B V x topGen B y y B x = y
13 11 12 syl J Top B J x topGen B y y B x = y
14 13 ralbidv J Top B J x J x topGen B x J y y B x = y
15 9 14 bitrd J Top B J topGen B = J x J y y B x = y