Metamath Proof Explorer

Theorem topnval

Description: Value of the topology extractor function. (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Hypotheses topnval.1 ⊢ 𝐵 = ( Base ‘ 𝑊 )
topnval.2 ⊢ 𝐽 = ( TopSet ‘ 𝑊 )
Assertion topnval ( 𝐽 ↾t 𝐵 ) = ( TopOpen ‘ 𝑊 )

Proof

Step Hyp Ref Expression
1 topnval.1 ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 topnval.2 ⊢ 𝐽 = ( TopSet ‘ 𝑊 )
3 fveq2 ⊢ ( 𝑤 = 𝑊 → ( TopSet ‘ 𝑤 ) = ( TopSet ‘ 𝑊 ) )
4 3 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( TopSet ‘ 𝑤 ) = 𝐽 )
5 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
6 5 1 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝐵 )
7 4 6 oveq12d ⊢ ( 𝑤 = 𝑊 → ( ( TopSet ‘ 𝑤 ) ↾t ( Base ‘ 𝑤 ) ) = ( 𝐽 ↾t 𝐵 ) )
8 df-topn ⊢ TopOpen = ( 𝑤 ∈ V ↦ ( ( TopSet ‘ 𝑤 ) ↾t ( Base ‘ 𝑤 ) ) )
9 ovex ⊢ ( 𝐽 ↾t 𝐵 ) ∈ V
10 7 8 9 fvmpt ⊢ ( 𝑊 ∈ V → ( TopOpen ‘ 𝑊 ) = ( 𝐽 ↾t 𝐵 ) )
11 10 eqcomd ⊢ ( 𝑊 ∈ V → ( 𝐽 ↾t 𝐵 ) = ( TopOpen ‘ 𝑊 ) )
12 0rest ⊢ ( ∅ ↾t 𝐵 ) = ∅
13 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( TopSet ‘ 𝑊 ) = ∅ )
14 2 13 syl5eq ⊢ ( ¬ 𝑊 ∈ V → 𝐽 = ∅ )
15 14 oveq1d ⊢ ( ¬ 𝑊 ∈ V → ( 𝐽 ↾t 𝐵 ) = ( ∅ ↾t 𝐵 ) )
16 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( TopOpen ‘ 𝑊 ) = ∅ )
17 12 15 16 3eqtr4a ⊢ ( ¬ 𝑊 ∈ V → ( 𝐽 ↾t 𝐵 ) = ( TopOpen ‘ 𝑊 ) )
18 11 17 pm2.61i ⊢ ( 𝐽 ↾t 𝐵 ) = ( TopOpen ‘ 𝑊 )