Metamath Proof Explorer

Theorem bastop

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

Ref Expression
Assertion bastop ⊢ B ∈ TopBases → B ∈ Top ↔ topGen ⁡ B = B

Proof

Step Hyp Ref Expression
1 tgtop ⊢ B ∈ Top → topGen ⁡ B = B
2 tgcl ⊢ B ∈ TopBases → topGen ⁡ B ∈ Top
3 eleq1 ⊢ topGen ⁡ B = B → topGen ⁡ B ∈ Top ↔ B ∈ Top
4 2 3 syl5ibcom ⊢ B ∈ TopBases → topGen ⁡ B = B → B ∈ Top
5 1 4 impbid2 ⊢ B ∈ TopBases → B ∈ Top ↔ topGen ⁡ B = B