Theorem oppglemOLD

Description: Obsolete version of setsplusg as of 18-Oct-2024. Lemma for oppgbas . (Contributed by Stefan O'Rear, 26-Aug-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	oppgbas.1	|- O = ( oppG ` R )
	oppglemOLD.2	|- E = Slot N
	oppglemOLD.3	|- N e. NN
	oppglemOLD.4	|- N =/= 2
Assertion	oppglemOLD	|- ( E ` R ) = ( E ` O )

Proof

Step	Hyp	Ref	Expression
1		oppgbas.1	|- O = ( oppG ` R )
2		oppglemOLD.2	|- E = Slot N
3		oppglemOLD.3	|- N e. NN
4		oppglemOLD.4	|- N =/= 2
5	2 3	ndxid	|- E = Slot ( E ` ndx )
6	2 3	ndxarg	|- ( E ` ndx ) = N
7		plusgndx	|- ( +g ` ndx ) = 2
8	6 7	neeq12i	|- ( ( E ` ndx ) =/= ( +g ` ndx ) <-> N =/= 2 )
9	4 8	mpbir	|- ( E ` ndx ) =/= ( +g ` ndx )
10	5 9	setsnid	|- ( E ` R ) = ( E ` ( R sSet <. ( +g ` ndx ) , tpos ( +g ` R ) >. ) )
11		eqid	|- ( +g ` R ) = ( +g ` R )
12	11 1	oppgval	|- O = ( R sSet <. ( +g ` ndx ) , tpos ( +g ` R ) >. )
13	12	fveq2i	|- ( E ` O ) = ( E ` ( R sSet <. ( +g ` ndx ) , tpos ( +g ` R ) >. ) )
14	10 13	eqtr4i	|- ( E ` R ) = ( E ` O )