This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem topnpropd

Description: The topology extractor function depends only on the base and topology components. (Contributed by NM, 18-Jul-2006)

Ref Expression
Hypotheses topnpropd.1 ⊢ φ → Base K = Base L
topnpropd.2 ⊢ φ → TopSet ⁡ K = TopSet ⁡ L
Assertion topnpropd ⊢ φ → TopOpen ⁡ K = TopOpen ⁡ L

Proof

Step Hyp Ref Expression
1 topnpropd.1 ⊢ φ → Base K = Base L
2 topnpropd.2 ⊢ φ → TopSet ⁡ K = TopSet ⁡ L
3 2 1 oveq12d ⊢ φ → TopSet ⁡ K ↾ 𝑡 Base K = TopSet ⁡ L ↾ 𝑡 Base L
4 eqid ⊢ Base K = Base K
5 eqid ⊢ TopSet ⁡ K = TopSet ⁡ K
6 4 5 topnval ⊢ TopSet ⁡ K ↾ 𝑡 Base K = TopOpen ⁡ K
7 eqid ⊢ Base L = Base L
8 eqid ⊢ TopSet ⁡ L = TopSet ⁡ L
9 7 8 topnval ⊢ TopSet ⁡ L ↾ 𝑡 Base L = TopOpen ⁡ L
10 3 6 9 3eqtr3g ⊢ φ → TopOpen ⁡ K = TopOpen ⁡ L