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

Metamath Proof Explorer

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 \in I \to U \subseteq B$

Proof

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