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	|- .+ = ( +g ` R )
	oppgval.3	|- O = ( oppG ` R )
Assertion	oppgval	|- O = ( R sSet <. ( +g ` ndx ) , tpos .+ >. )

Proof

Step	Hyp	Ref	Expression
1		oppgval.2	|- .+ = ( +g ` R )
2		oppgval.3	|- O = ( oppG ` R )
3		id	|- ( x = R -> x = R )
4		fveq2	|- ( x = R -> ( +g ` x ) = ( +g ` R ) )
5	4 1	eqtr4di	|- ( x = R -> ( +g ` x ) = .+ )
6	5	tposeqd	|- ( x = R -> tpos ( +g ` x ) = tpos .+ )
7	6	opeq2d	|- ( x = R -> <. ( +g ` ndx ) , tpos ( +g ` x ) >. = <. ( +g ` ndx ) , tpos .+ >. )
8	3 7	oveq12d	|- ( x = R -> ( x sSet <. ( +g ` ndx ) , tpos ( +g ` x ) >. ) = ( R sSet <. ( +g ` ndx ) , tpos .+ >. ) )
9		df-oppg	|- oppG = ( x e. _V |-> ( x sSet <. ( +g ` ndx ) , tpos ( +g ` x ) >. ) )
10		ovex	|- ( R sSet <. ( +g ` ndx ) , tpos .+ >. ) e. _V
11	8 9 10	fvmpt	|- ( R e. _V -> ( oppG ` R ) = ( R sSet <. ( +g ` ndx ) , tpos .+ >. ) )
12		fvprc	|- ( -. R e. _V -> ( oppG ` R ) = (/) )
13		reldmsets	|- Rel dom sSet
14	13	ovprc1	|- ( -. R e. _V -> ( R sSet <. ( +g ` ndx ) , tpos .+ >. ) = (/) )
15	12 14	eqtr4d	|- ( -. R e. _V -> ( oppG ` R ) = ( R sSet <. ( +g ` ndx ) , tpos .+ >. ) )
16	11 15	pm2.61i	|- ( oppG ` R ) = ( R sSet <. ( +g ` ndx ) , tpos .+ >. )
17	2 16	eqtri	|- O = ( R sSet <. ( +g ` ndx ) , tpos .+ >. )