This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: The base set of a topology on a given base set. (Contributed by Mario
Carneiro, 13-Aug-2015)
|
|
Ref |
Expression |
|
Assertion |
toponuni |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → 𝐵 = ∪ 𝐽 ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
istopon |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ↔ ( 𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽 ) ) |
| 2 |
1
|
simprbi |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → 𝐵 = ∪ 𝐽 ) |