This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC ALGEBRAIC STRUCTURES Subring algebras and ideals Two-sided ideals and quotient rings 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 ⊢ ( 𝑈 ∈ 𝐼 → 𝑈 ⊆ 𝐵 )