Theorem rrgss

Description: Left-regular elements are a subset of the base set. (Contributed by Stefan O'Rear, 22-Mar-2015)

	Ref	Expression
Hypotheses	rrgss.e	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
	rrgss.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	rrgss	⊢ 𝐸 ⊆ 𝐵

Proof

Step	Hyp	Ref	Expression
1		rrgss.e	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
2		rrgss.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
4		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
5	1 2 3 4	rrgval	⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) → 𝑦 = ( 0g ‘ 𝑅 ) ) }
6	5	ssrab3	⊢ 𝐸 ⊆ 𝐵