Metamath Proof Explorer


Theorem idlss

Description: An ideal of R is a subset of R . (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses idlss.1 G = 1 st R
idlss.2 X = ran G
Assertion idlss R RingOps I Idl R I X

Proof

Step Hyp Ref Expression
1 idlss.1 G = 1 st R
2 idlss.2 X = ran G
3 eqid 2 nd R = 2 nd R
4 eqid GId G = GId G
5 1 3 2 4 isidl R RingOps I Idl R I X GId G I x I y I x G y I z X z 2 nd R x I x 2 nd R z I
6 5 biimpa R RingOps I Idl R I X GId G I x I y I x G y I z X z 2 nd R x I x 2 nd R z I
7 6 simp1d R RingOps I Idl R I X