Theorem 2idlelb

Description: Membership in a two-sided ideal. Formerly part of proof for 2idlcpbl . (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by AV, 20-Feb-2025)

	Ref	Expression
Hypotheses	2idlel.i	⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
	2idlel.o	⊢ 𝑂 = ( oppr ‘ 𝑅 )
	2idlel.j	⊢ 𝐽 = ( LIdeal ‘ 𝑂 )
	2idlel.t	⊢ 𝑇 = ( 2Ideal ‘ 𝑅 )
Assertion	2idlelb	⊢ ( 𝑈 ∈ 𝑇 ↔ ( 𝑈 ∈ 𝐼 ∧ 𝑈 ∈ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		2idlel.i	⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
2		2idlel.o	⊢ 𝑂 = ( oppr ‘ 𝑅 )
3		2idlel.j	⊢ 𝐽 = ( LIdeal ‘ 𝑂 )
4		2idlel.t	⊢ 𝑇 = ( 2Ideal ‘ 𝑅 )
5	1 2 3 4	2idlval	⊢ 𝑇 = ( 𝐼 ∩ 𝐽 )
6	5	elin2	⊢ ( 𝑈 ∈ 𝑇 ↔ ( 𝑈 ∈ 𝐼 ∧ 𝑈 ∈ 𝐽 ) )