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