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	⊢ oppr = ( 𝑓 ∈ V ↦ ( 𝑓 sSet ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑓 ) ⟩ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		coppr	⊢ oppr
1		vf	⊢ 𝑓
2		cvv	⊢ V
3	1	cv	⊢ 𝑓
4		csts	⊢ sSet
5		cmulr	⊢ .r
6		cnx	⊢ ndx
7	6 5	cfv	⊢ ( .r ‘ ndx )
8	3 5	cfv	⊢ ( .r ‘ 𝑓 )
9	8	ctpos	⊢ tpos ( .r ‘ 𝑓 )
10	7 9	cop	⊢ ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑓 ) ⟩
11	3 10 4	co	⊢ ( 𝑓 sSet ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑓 ) ⟩ )
12	1 2 11	cmpt	⊢ ( 𝑓 ∈ V ↦ ( 𝑓 sSet ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑓 ) ⟩ ) )
13	0 12	wceq	⊢ oppr = ( 𝑓 ∈ V ↦ ( 𝑓 sSet ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑓 ) ⟩ ) )