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 JTopBJJtopGenBtopGenB=J

Proof

Step Hyp Ref Expression
1 tgss JTopBJtopGenBtopGenJ
2 1 3adant3 JTopBJJtopGenBtopGenBtopGenJ
3 tgtop JToptopGenJ=J
4 3 3ad2ant1 JTopBJJtopGenBtopGenJ=J
5 2 4 sseqtrd JTopBJJtopGenBtopGenBJ
6 simp3 JTopBJJtopGenBJtopGenB
7 5 6 eqssd JTopBJJtopGenBtopGenB=J