Metamath Proof Explorer


Theorem topnid

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 ‘ 𝑊 ) )

Proof

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 ‘ 𝑊 ) )