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 |
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 |