Definition df-oppr

Description: Define an opposite ring, which is the same as the original ring but with multiplication written the other way around. (Contributed by Mario Carneiro, 1-Dec-2014)

	Ref	Expression
Assertion	df-oppr	$$⊢{opp}_r=\left(f\in \mathrm{V}⟼f\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_f⟩\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		coppr	$$class{opp}_r$$
1		vf	$$setvarf$$
2		cvv	$$class\mathrm{V}$$
3	1	cv	$$setvarf$$
4		csts	$$class\mathrm{sSet}$$
5		cmulr	$$class{\cdot }_{𝑟}$$
6		cnx	$$class\mathrm{ndx}$$
7	6 5	cfv	$$class{\cdot }_{\mathrm{ndx}}$$
8	3 5	cfv	$$class{\cdot }_f$$
9	8	ctpos	$$classtpos{\cdot }_f$$
10	7 9	cop	$$class⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_f⟩$$
11	3 10 4	co	$$class\left(f\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_f⟩\right)$$
12	1 2 11	cmpt	$$class\left(f\in \mathrm{V}⟼f\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_f⟩\right)$$
13	0 12	wceq	$$wff{opp}_r=\left(f\in \mathrm{V}⟼f\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},tpos{\cdot }_f⟩\right)$$