Description: Value of the topology extractor function when the topology is defined over the same set as the base. (Contributed by Mario Carneiro, 13-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | topnval.1 | ⊢ 𝐵 = ( Base ‘ 𝑊 ) | |
topnval.2 | ⊢ 𝐽 = ( TopSet ‘ 𝑊 ) | ||
Assertion | topnid | ⊢ ( 𝐽 ⊆ 𝒫 𝐵 → 𝐽 = ( TopOpen ‘ 𝑊 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | topnval.1 | ⊢ 𝐵 = ( Base ‘ 𝑊 ) | |
2 | topnval.2 | ⊢ 𝐽 = ( TopSet ‘ 𝑊 ) | |
3 | 1 | fvexi | ⊢ 𝐵 ∈ V |
4 | restid2 | ⊢ ( ( 𝐵 ∈ V ∧ 𝐽 ⊆ 𝒫 𝐵 ) → ( 𝐽 ↾t 𝐵 ) = 𝐽 ) | |
5 | 3 4 | mpan | ⊢ ( 𝐽 ⊆ 𝒫 𝐵 → ( 𝐽 ↾t 𝐵 ) = 𝐽 ) |
6 | 1 2 | topnval | ⊢ ( 𝐽 ↾t 𝐵 ) = ( TopOpen ‘ 𝑊 ) |
7 | 5 6 | eqtr3di | ⊢ ( 𝐽 ⊆ 𝒫 𝐵 → 𝐽 = ( TopOpen ‘ 𝑊 ) ) |