bastop

Description: Two ways to express that a basis is a topology. (Contributed by NM, 18-Jul-2006)

		Ref	Expression
	Assertion	bastop	$⊢ B \in TopBases \to (B \in Top \leftrightarrow topGen (B) = B)$

Step	Hyp	Ref	Expression
1		tgtop	$⊢ B \in Top \to topGen (B) = B$
2		tgcl	$⊢ B \in TopBases \to topGen (B) \in Top$
3		eleq1	$⊢ topGen (B) = B \to (topGen (B) \in Top \leftrightarrow B \in Top)$
4	2 3	syl5ibcom	$⊢ B \in TopBases \to (topGen (B) = B \to B \in Top)$
5	1 4	impbid2	$⊢ B \in TopBases \to (B \in Top \leftrightarrow topGen (B) = B)$

Metamath Proof Explorer