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

Metamath Proof Explorer

Theorem unifndxntsetndx

Description: The slot for the uniform set is not the slot for the topology in an extensible structure. Formerly part of proof for tuslem . (Contributed by AV, 28-Oct-2024)

		Ref	Expression
	Assertion	unifndxntsetndx	$⊢ UnifSet (ndx) \neq TopSet (ndx)$

Proof

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