This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ V , s ∈ V ⟼ x y | x y ⊆ Base g ∧ inv g ⁡ g ⁡ x + g y ∈ s
3 2 relmpoopab ⊢ Rel ⁡ G ~ QG S
4 1 releqi ⊢ Rel ⁡ R ↔ Rel ⁡ G ~ QG S
5 3 4 mpbir ⊢ Rel ⁡ R