Metamath Proof Explorer


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