Theorem releqg

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

	Ref	Expression
Hypothesis	releqg.r	⊢ 𝑅 = ( 𝐺 ~QG 𝑆 )
Assertion	releqg	⊢ Rel 𝑅

Proof

Step	Hyp	Ref	Expression
1		releqg.r	⊢ 𝑅 = ( 𝐺 ~QG 𝑆 )
2		df-eqg	⊢ ~QG = ( 𝑔 ∈ V , 𝑠 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑔 ) ∧ ( ( ( invg ‘ 𝑔 ) ‘ 𝑥 ) ( +g ‘ 𝑔 ) 𝑦 ) ∈ 𝑠 ) } )
3	2	relmpoopab	⊢ Rel ( 𝐺 ~QG 𝑆 )
4	1	releqi	⊢ ( Rel 𝑅 ↔ Rel ( 𝐺 ~QG 𝑆 ) )
5	3 4	mpbir	⊢ Rel 𝑅