# Metamath Proof Explorer

## 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 ${setvar}{f}$
2 cvv ${class}\mathrm{V}$
3 1 cv ${setvar}{f}$
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 ${class}tpos{\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)$