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={\mathrm{Base}}_W$$
	2idlss.i	$$⊢I=\mathrm{2Ideal}\left(W\right)$$
Assertion	2idlss	$$⊢U\in I\to U\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		2idlss.b	$$⊢B={\mathrm{Base}}_W$$
2		2idlss.i	$$⊢I=\mathrm{2Ideal}\left(W\right)$$
3	2	eleq2i	$$⊢U\in I\leftrightarrow U\in \mathrm{2Ideal}\left(W\right)$$
4	3	biimpi	$$⊢U\in I\to U\in \mathrm{2Ideal}\left(W\right)$$
5	4	2idllidld	$$⊢U\in I\to U\in \mathrm{LIdeal}\left(W\right)$$
6		eqid	$$⊢\mathrm{LIdeal}\left(W\right)=\mathrm{LIdeal}\left(W\right)$$
7	1 6	lidlss	$$⊢U\in \mathrm{LIdeal}\left(W\right)\to U\subseteq B$$
8	5 7	syl	$$⊢U\in I\to U\subseteq B$$