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

Metamath Proof Explorer

Theorem plendxnplusgndx

Description: The slot for the "less than or equal to" ordering is not the slot for the group operation in an extensible structure. Formerly part of proof for oppgle . (Contributed by AV, 18-Oct-2024)

		Ref	Expression
	Assertion	plendxnplusgndx	$⊢ \leq_{ndx} \neq +_{ndx}$

Proof

Step	Hyp	Ref	Expression
1		2re	$⊢ 2 \in ℝ$
2		2lt10	$⊢ 2 < 10$
3	1 2	gtneii	$⊢ 10 \neq 2$
4		plendx	$⊢ \leq_{ndx} = 10$
5		plusgndx	$⊢ +_{ndx} = 2$
6	4 5	neeq12i	$⊢ \leq_{ndx} \neq +_{ndx} \leftrightarrow 10 \neq 2$
7	3 6	mpbir	$⊢ \leq_{ndx} \neq +_{ndx}$