Theorem 2idlss

Description: A two-sided ideal is a subset of the base set. Formerly part of proof for 2idlcpbl . (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by AV, 20-Feb-2025) (Proof shortened by AV, 13-Mar-2025)

	Ref	Expression
Hypotheses	2idlss.b	|- B = ( Base ` W )
	2idlss.i	|- I = ( 2Ideal ` W )
Assertion	2idlss	|- ( U e. I -> U C_ B )

Proof

Step	Hyp	Ref	Expression
1		2idlss.b	|- B = ( Base ` W )
2		2idlss.i	|- I = ( 2Ideal ` W )
3	2	eleq2i	|- ( U e. I <-> U e. ( 2Ideal ` W ) )
4	3	biimpi	|- ( U e. I -> U e. ( 2Ideal ` W ) )
5	4	2idllidld	|- ( U e. I -> U e. ( LIdeal ` W ) )
6		eqid	|- ( LIdeal ` W ) = ( LIdeal ` W )
7	1 6	lidlss	|- ( U e. ( LIdeal ` W ) -> U C_ B )
8	5 7	syl	|- ( U e. I -> U C_ B )