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	$$⊢E=\mathrm{RLReg}\left(R\right)$$
	rrgss.b	$$⊢B={\mathrm{Base}}_R$$
Assertion	rrgss	$$⊢E\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		rrgss.e	$$⊢E=\mathrm{RLReg}\left(R\right)$$
2		rrgss.b	$$⊢B={\mathrm{Base}}_R$$
3		eqid	$$⊢{\cdot }_R={\cdot }_R$$
4		eqid	$$⊢0_R=0_R$$
5	1 2 3 4	rrgval	$$⊢E=\left\{x\in B|\forall y\in B\left(x{\cdot }_{R}y=0_R\to y=0_R\right)\right\}$$
6	5	ssrab3	$$⊢E\subseteq B$$