Theorem basendxnplusgndx

Description: The slot for the base set is not the slot for the group operation in an extensible structure. (Contributed by AV, 14-Nov-2021)

	Ref	Expression
Assertion	basendxnplusgndx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {+}_{\mathrm{ndx}}$$

Proof

Step	Hyp	Ref	Expression
1		df-base	$$⊢\mathrm{Base}=\mathrm{Slot}1$$
2		1nn	$$⊢1\in \mathbb{N}$$
3	1 2	ndxarg	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
4		1ne2	$$⊢1\ne 2$$
5		plusgndx	$$⊢{+}_{\mathrm{ndx}}=2$$
6	4 5	neeqtrri	$$⊢1\ne {+}_{\mathrm{ndx}}$$
7	3 6	eqnetri	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {+}_{\mathrm{ndx}}$$