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{~}_{\mathit{QG}}S$$
Assertion	releqg	$$⊢\mathrm{Rel}R$$

Proof

Step	Hyp	Ref	Expression
1		releqg.r	$$⊢R=G{~}_{\mathit{QG}}S$$
2		df-eqg	$$⊢{~}_{\mathit{QG}}=\left(g\in \mathrm{V},s\in \mathrm{V}⟼\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq {\mathrm{Base}}_g\wedge {inv}_g\left(g\right)\left(x\right){+}_{g}y\in s\right)\right\}\right)$$
3	2	relmpoopab	$$⊢\mathrm{Rel}\left(G{~}_{\mathit{QG}}S\right)$$
4	1	releqi	$$⊢\mathrm{Rel}R\leftrightarrow \mathrm{Rel}\left(G{~}_{\mathit{QG}}S\right)$$
5	3 4	mpbir	$$⊢\mathrm{Rel}R$$