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) \neq TopSet (ndx)$

Proof

Step	Hyp	Ref	Expression
1		9re	$⊢ 9 \in ℝ$
2		1nn	$⊢ 1 \in ℕ$
3		2nn0	$⊢ 2 \in ℕ_{0}$
4		9nn0	$⊢ 9 \in ℕ_{0}$
5		9lt10	$⊢ 9 < 10$
6	2 3 4 5	declti	$⊢ 9 < 12$
7	1 6	gtneii	$⊢ 12 \neq 9$
8		dsndx	$⊢ dist (ndx) = 12$
9		tsetndx	$⊢ TopSet (ndx) = 9$
10	8 9	neeq12i	$⊢ dist (ndx) \neq TopSet (ndx) \leftrightarrow 12 \neq 9$
11	7 10	mpbir	$⊢ dist (ndx) \neq TopSet (ndx)$