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	⊢ 𝐵 = ( Base ‘ 𝑊 )
	2idlss.i	⊢ 𝐼 = ( 2Ideal ‘ 𝑊 )
Assertion	2idlss	⊢ ( 𝑈 ∈ 𝐼 → 𝑈 ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		2idlss.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		2idlss.i	⊢ 𝐼 = ( 2Ideal ‘ 𝑊 )
3	2	eleq2i	⊢ ( 𝑈 ∈ 𝐼 ↔ 𝑈 ∈ ( 2Ideal ‘ 𝑊 ) )
4	3	biimpi	⊢ ( 𝑈 ∈ 𝐼 → 𝑈 ∈ ( 2Ideal ‘ 𝑊 ) )
5	4	2idllidld	⊢ ( 𝑈 ∈ 𝐼 → 𝑈 ∈ ( LIdeal ‘ 𝑊 ) )
6		eqid	⊢ ( LIdeal ‘ 𝑊 ) = ( LIdeal ‘ 𝑊 )
7	1 6	lidlss	⊢ ( 𝑈 ∈ ( LIdeal ‘ 𝑊 ) → 𝑈 ⊆ 𝐵 )
8	5 7	syl	⊢ ( 𝑈 ∈ 𝐼 → 𝑈 ⊆ 𝐵 )