Metamath Proof Explorer


Theorem unitg

Description: The topology generated by a basis B is a topology on U. B . Importantly, this theorem means that we don't have to specify separately the base set for the topological space generated by a basis. In other words, any member of the class TopBases completely specifies the basis it corresponds to. (Contributed by NM, 16-Jul-2006) (Proof shortened by OpenAI, 30-Mar-2020)

Ref Expression
Assertion unitg ( 𝐵𝑉 ( topGen ‘ 𝐵 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 tg1 ( 𝑥 ∈ ( topGen ‘ 𝐵 ) → 𝑥 𝐵 )
2 velpw ( 𝑥 ∈ 𝒫 𝐵𝑥 𝐵 )
3 1 2 sylibr ( 𝑥 ∈ ( topGen ‘ 𝐵 ) → 𝑥 ∈ 𝒫 𝐵 )
4 3 ssriv ( topGen ‘ 𝐵 ) ⊆ 𝒫 𝐵
5 sspwuni ( ( topGen ‘ 𝐵 ) ⊆ 𝒫 𝐵 ( topGen ‘ 𝐵 ) ⊆ 𝐵 )
6 4 5 mpbi ( topGen ‘ 𝐵 ) ⊆ 𝐵
7 6 a1i ( 𝐵𝑉 ( topGen ‘ 𝐵 ) ⊆ 𝐵 )
8 bastg ( 𝐵𝑉𝐵 ⊆ ( topGen ‘ 𝐵 ) )
9 8 unissd ( 𝐵𝑉 𝐵 ( topGen ‘ 𝐵 ) )
10 7 9 eqssd ( 𝐵𝑉 ( topGen ‘ 𝐵 ) = 𝐵 )