Theorem bastop

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

	Ref	Expression
Assertion	bastop	⊢ ( 𝐵 ∈ TopBases → ( 𝐵 ∈ Top ↔ ( topGen ‘ 𝐵 ) = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		tgtop	⊢ ( 𝐵 ∈ Top → ( topGen ‘ 𝐵 ) = 𝐵 )
2		tgcl	⊢ ( 𝐵 ∈ TopBases → ( topGen ‘ 𝐵 ) ∈ Top )
3		eleq1	⊢ ( ( topGen ‘ 𝐵 ) = 𝐵 → ( ( topGen ‘ 𝐵 ) ∈ Top ↔ 𝐵 ∈ Top ) )
4	2 3	syl5ibcom	⊢ ( 𝐵 ∈ TopBases → ( ( topGen ‘ 𝐵 ) = 𝐵 → 𝐵 ∈ Top ) )
5	1 4	impbid2	⊢ ( 𝐵 ∈ TopBases → ( 𝐵 ∈ Top ↔ ( topGen ‘ 𝐵 ) = 𝐵 ) )