Theorem opprval

Description: Value of the opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014)

	Ref	Expression
Hypotheses	opprval.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
	opprval.2	⊢ · = ( .r ‘ 𝑅 )
	opprval.3	⊢ 𝑂 = ( oppr ‘ 𝑅 )
Assertion	opprval	⊢ 𝑂 = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ )

Proof

Step	Hyp	Ref	Expression
1		opprval.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		opprval.2	⊢ · = ( .r ‘ 𝑅 )
3		opprval.3	⊢ 𝑂 = ( oppr ‘ 𝑅 )
4		id	⊢ ( 𝑥 = 𝑅 → 𝑥 = 𝑅 )
5		fveq2	⊢ ( 𝑥 = 𝑅 → ( .r ‘ 𝑥 ) = ( .r ‘ 𝑅 ) )
6	5 2	eqtr4di	⊢ ( 𝑥 = 𝑅 → ( .r ‘ 𝑥 ) = · )
7	6	tposeqd	⊢ ( 𝑥 = 𝑅 → tpos ( .r ‘ 𝑥 ) = tpos · )
8	7	opeq2d	⊢ ( 𝑥 = 𝑅 → ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑥 ) ⟩ = ⟨ ( .r ‘ ndx ) , tpos · ⟩ )
9	4 8	oveq12d	⊢ ( 𝑥 = 𝑅 → ( 𝑥 sSet ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑥 ) ⟩ ) = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ ) )
10		df-oppr	⊢ oppr = ( 𝑥 ∈ V ↦ ( 𝑥 sSet ⟨ ( .r ‘ ndx ) , tpos ( .r ‘ 𝑥 ) ⟩ ) )
11		ovex	⊢ ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ ) ∈ V
12	9 10 11	fvmpt	⊢ ( 𝑅 ∈ V → ( oppr ‘ 𝑅 ) = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ ) )
13		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( oppr ‘ 𝑅 ) = ∅ )
14		reldmsets	⊢ Rel dom sSet
15	14	ovprc1	⊢ ( ¬ 𝑅 ∈ V → ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ ) = ∅ )
16	13 15	eqtr4d	⊢ ( ¬ 𝑅 ∈ V → ( oppr ‘ 𝑅 ) = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ ) )
17	12 16	pm2.61i	⊢ ( oppr ‘ 𝑅 ) = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ )
18	3 17	eqtri	⊢ 𝑂 = ( 𝑅 sSet ⟨ ( .r ‘ ndx ) , tpos · ⟩ )