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 ) ≠ ( *𝑟 ‘ ndx )

Proof

Step Hyp Ref Expression
1 4re ⊢ 4 ∈ ℝ
2 4lt9 ⊢ 4 < 9
3 1 2 gtneii ⊢ 9 ≠ 4
4 tsetndx ⊢ ( TopSet ‘ ndx ) = 9
5 starvndx ⊢ ( *𝑟 ‘ ndx ) = 4
6 4 5 neeq12i ⊢ ( ( TopSet ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ↔ 9 ≠ 4 )
7 3 6 mpbir ⊢ ( TopSet ‘ ndx ) ≠ ( *𝑟 ‘ ndx )