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 ‘ 𝐵 ) = ∪ 𝐵 ) |
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 ‘ 𝐵 ) = ∪ 𝐵 ) |