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

Metamath Proof Explorer

Theorem dsndxntsetndx

Description: The slot for the distance function is not the slot for the topology in an extensible structure. Formerly part of proof for tngds . (Contributed by AV, 29-Oct-2024)

Ref Expression
Assertion dsndxntsetndx ( dist ‘ ndx ) ≠ ( TopSet ‘ ndx )

Proof

Step Hyp Ref Expression
1 9re ⊢ 9 ∈ ℝ
2 1nn ⊢ 1 ∈ ℕ
3 2nn0 ⊢ 2 ∈ ℕ0
4 9nn0 ⊢ 9 ∈ ℕ0
5 9lt10 ⊢ 9 < 1 0
6 2 3 4 5 declti ⊢ 9 < 1 2
7 1 6 gtneii ⊢ 1 2 ≠ 9
8 dsndx ⊢ ( dist ‘ ndx ) = 1 2
9 tsetndx ⊢ ( TopSet ‘ ndx ) = 9
10 8 9 neeq12i ⊢ ( ( dist ‘ ndx ) ≠ ( TopSet ‘ ndx ) ↔ 1 2 ≠ 9 )
11 7 10 mpbir ⊢ ( dist ‘ ndx ) ≠ ( TopSet ‘ ndx )