Metamath Proof Explorer


Theorem basgen

Description: Given a topology J , show that a subset B satisfying the third antecedent is a basis for it. Lemma 2.3 of Munkres p. 81 using abbreviations. (Contributed by NM, 22-Jul-2006) (Revised by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion basgen J Top B J J topGen B topGen B = J

Proof

Step Hyp Ref Expression
1 tgss J Top B J topGen B topGen J
2 1 3adant3 J Top B J J topGen B topGen B topGen J
3 tgtop J Top topGen J = J
4 3 3ad2ant1 J Top B J J topGen B topGen J = J
5 2 4 sseqtrd J Top B J J topGen B topGen B J
6 simp3 J Top B J J topGen B J topGen B
7 5 6 eqssd J Top B J J topGen B topGen B = J