Theorem setsplusg

Description: The other components of an extensible structure remain unchanged if the +g component is set/substituted. (Contributed by Stefan O'Rear, 26-Aug-2015) Generalisation of the former oppglem and mgplem. (Revised by AV, 18-Oct-2024)

	Ref	Expression
Hypotheses	setsplusg.o	$$⊢O=R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},S⟩$$
	setsplusg.e	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
	setsplusg.i	$$⊢E\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}$$
Assertion	setsplusg	$$⊢E\left(R\right)=E\left(O\right)$$

Proof

Step	Hyp	Ref	Expression
1		setsplusg.o	$$⊢O=R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},S⟩$$
2		setsplusg.e	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
3		setsplusg.i	$$⊢E\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}$$
4	2 3	setsnid	$$⊢E\left(R\right)=E\left(R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},S⟩\right)$$
5	1	fveq2i	$$⊢E\left(O\right)=E\left(R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},S⟩\right)$$
6	4 5	eqtr4i	$$⊢E\left(R\right)=E\left(O\right)$$