Theorem oppgval

Description: Value of the opposite group. (Contributed by Stefan O'Rear, 25-Aug-2015) (Revised by Mario Carneiro, 16-Sep-2015) (Revised by Fan Zheng, 26-Jun-2016)

	Ref	Expression
Hypotheses	oppgval.2	$$⊢\underset{\dot{}}{+}={+}_R$$
	oppgval.3	$$⊢O={opp}_{𝑔}\left(R\right)$$
Assertion	oppgval	$$⊢O=R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},tpos\underset{\dot{}}{+}⟩$$

Proof

Step	Hyp	Ref	Expression
1		oppgval.2	$$⊢\underset{\dot{}}{+}={+}_R$$
2		oppgval.3	$$⊢O={opp}_{𝑔}\left(R\right)$$
3		id	$$⊢x=R\to x=R$$
4		fveq2	$$⊢x=R\to {+}_x={+}_R$$
5	4 1	eqtr4di	$$⊢x=R\to {+}_x=\underset{\dot{}}{+}$$
6	5	tposeqd	$$⊢x=R\to tpos{+}_x=tpos\underset{\dot{}}{+}$$
7	6	opeq2d	$$⊢x=R\to ⟨{+}_{\mathrm{ndx}},tpos{+}_x⟩=⟨{+}_{\mathrm{ndx}},tpos\underset{\dot{}}{+}⟩$$
8	3 7	oveq12d	$$⊢x=R\to x\mathrm{sSet}⟨{+}_{\mathrm{ndx}},tpos{+}_x⟩=R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},tpos\underset{\dot{}}{+}⟩$$
9		df-oppg	$$⊢{opp}_{𝑔}=\left(x\in \mathrm{V}⟼x\mathrm{sSet}⟨{+}_{\mathrm{ndx}},tpos{+}_x⟩\right)$$
10		ovex	$$⊢R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},tpos\underset{\dot{}}{+}⟩\in \mathrm{V}$$
11	8 9 10	fvmpt	$$⊢R\in \mathrm{V}\to {opp}_{𝑔}\left(R\right)=R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},tpos\underset{\dot{}}{+}⟩$$
12		fvprc	$$⊢\neg R\in \mathrm{V}\to {opp}_{𝑔}\left(R\right)=\varnothing$$
13		reldmsets	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{sSet}$$
14	13	ovprc1	$$⊢\neg R\in \mathrm{V}\to R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},tpos\underset{\dot{}}{+}⟩=\varnothing$$
15	12 14	eqtr4d	$$⊢\neg R\in \mathrm{V}\to {opp}_{𝑔}\left(R\right)=R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},tpos\underset{\dot{}}{+}⟩$$
16	11 15	pm2.61i	$$⊢{opp}_{𝑔}\left(R\right)=R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},tpos\underset{\dot{}}{+}⟩$$
17	2 16	eqtri	$$⊢O=R\mathrm{sSet}⟨{+}_{\mathrm{ndx}},tpos\underset{\dot{}}{+}⟩$$