Theorem releqg

Description: The left coset equivalence relation is a relation. (Contributed by Mario Carneiro, 14-Jun-2015)

	Ref	Expression
Hypothesis	releqg.r	|- R = ( G ~QG S )
Assertion	releqg	|- Rel R

Proof

Step	Hyp	Ref	Expression
1		releqg.r	|- R = ( G ~QG S )
2		df-eqg	|- ~QG = ( g e. _V , s e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` g ) /\ ( ( ( invg ` g ) ` x ) ( +g ` g ) y ) e. s ) } )
3	2	relmpoopab	|- Rel ( G ~QG S )
4	1	releqi	|- ( Rel R <-> Rel ( G ~QG S ) )
5	3 4	mpbir	|- Rel R