Definition df-oppg

Description: Define an opposite group, which is the same as the original group but with addition written the other way around. df-oppr does the same thing for multiplication. (Contributed by Stefan O'Rear, 25-Aug-2015)

	Ref	Expression
Assertion	df-oppg	$$⊢{opp}_{𝑔}=\left(w\in \mathrm{V}⟼w\mathrm{sSet}⟨{+}_{\mathrm{ndx}},tpos{+}_w⟩\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		coppg	$$class{opp}_{𝑔}$$
1		vw	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3	1	cv	$$setvarw$$
4		csts	$$class\mathrm{sSet}$$
5		cplusg	$$class{+}_{𝑔}$$
6		cnx	$$class\mathrm{ndx}$$
7	6 5	cfv	$$class{+}_{\mathrm{ndx}}$$
8	3 5	cfv	$$class{+}_w$$
9	8	ctpos	$$classtpos{+}_w$$
10	7 9	cop	$$class⟨{+}_{\mathrm{ndx}},tpos{+}_w⟩$$
11	3 10 4	co	$$class\left(w\mathrm{sSet}⟨{+}_{\mathrm{ndx}},tpos{+}_w⟩\right)$$
12	1 2 11	cmpt	$$class\left(w\in \mathrm{V}⟼w\mathrm{sSet}⟨{+}_{\mathrm{ndx}},tpos{+}_w⟩\right)$$
13	0 12	wceq	$$wff{opp}_{𝑔}=\left(w\in \mathrm{V}⟼w\mathrm{sSet}⟨{+}_{\mathrm{ndx}},tpos{+}_w⟩\right)$$