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

Metamath Proof Explorer

Theorem tsetndxnstarvndx

Description: The slot for the topology is not the slot for the involution in an extensible structure. Formerly part of proof for cnfldfunALT . (Contributed by AV, 11-Nov-2024)

		Ref	Expression
	Assertion	tsetndxnstarvndx	$⊢ TopSet (ndx) \neq *_{ndx}$

Proof

Step	Hyp	Ref	Expression
1		4re	$⊢ 4 \in ℝ$
2		4lt9	$⊢ 4 < 9$
3	1 2	gtneii	$⊢ 9 \neq 4$
4		tsetndx	$⊢ TopSet (ndx) = 9$
5		starvndx	$⊢ *_{ndx} = 4$
6	4 5	neeq12i	$⊢ TopSet (ndx) \neq *_{ndx} \leftrightarrow 9 \neq 4$
7	3 6	mpbir	$⊢ TopSet (ndx) \neq *_{ndx}$