Theorem 2idl0

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

	Ref	Expression
Hypotheses	2idl0.u	|- I = ( 2Ideal ` R )
	2idl0.z	|- .0. = ( 0g ` R )
Assertion	2idl0	|- ( R e. Ring -> { .0. } e. I )

Proof

Step	Hyp	Ref	Expression
1		2idl0.u	|- I = ( 2Ideal ` R )
2		2idl0.z	|- .0. = ( 0g ` R )
3		eqid	|- ( LIdeal ` R ) = ( LIdeal ` R )
4	3 2	lidl0	|- ( R e. Ring -> { .0. } e. ( LIdeal ` R ) )
5		eqid	|- ( LIdeal ` ( oppR ` R ) ) = ( LIdeal ` ( oppR ` R ) )
6	5 2	ridl0	|- ( R e. Ring -> { .0. } e. ( LIdeal ` ( oppR ` R ) ) )
7	4 6	elind	|- ( R e. Ring -> { .0. } 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 -> { .0. } e. I )