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

Metamath Proof Explorer

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 = RLReg ⁡ R
rrgss.b ⊢ B = Base R
Assertion rrgss ⊢ E ⊆ B

Proof

Step Hyp Ref Expression
1 rrgss.e ⊢ E = RLReg ⁡ R
2 rrgss.b ⊢ B = Base R
3 eqid ⊢ ⋅ R = ⋅ R
4 eqid ⊢ 0 R = 0 R
5 1 2 3 4 rrgval ⊢ E = x ∈ B | ∀ y ∈ B x ⋅ R y = 0 R → y = 0 R
6 5 ssrab3 ⊢ E ⊆ B