Theorem 2idl1

Description: Every ring contains a unit two-sided ideal. (Contributed by AV, 13-Feb-2025)

	Ref	Expression
Hypotheses	2idl0.u	|- I = ( 2Ideal ` R )
	2idl1.b	|- B = ( Base ` R )
Assertion	2idl1	|- ( R e. Ring -> B e. I )

Proof

Step	Hyp	Ref	Expression
1		2idl0.u	|- I = ( 2Ideal ` R )
2		2idl1.b	|- B = ( Base ` R )
3		eqid	|- ( LIdeal ` R ) = ( LIdeal ` R )
4	3 2	lidl1	|- ( R e. Ring -> B e. ( LIdeal ` R ) )
5		eqid	|- ( LIdeal ` ( oppR ` R ) ) = ( LIdeal ` ( oppR ` R ) )
6	5 2	ridl1	|- ( R e. Ring -> B e. ( LIdeal ` ( oppR ` R ) ) )
7	4 6	elind	|- ( R e. Ring -> B e. ( ( LIdeal ` R ) i^i ( LIdeal ` ( oppR ` R ) ) ) )
8		eqid	|- ( oppR ` R ) = ( oppR ` R )
9	3 8 5 1	2idlval	|- I = ( ( LIdeal ` R ) i^i ( LIdeal ` ( oppR ` R ) ) )
10	7 9	eleqtrrdi	|- ( R e. Ring -> B e. I )