Theorem lidlincl

Description: Ideals are closed under intersection. (Contributed by Thierry Arnoux, 5-Jul-2024)

	Ref	Expression
Hypothesis	lidlincl.1	|- U = ( LIdeal ` R )
Assertion	lidlincl	|- ( ( R e. Ring /\ I e. U /\ J e. U ) -> ( I i^i J ) e. U )

Proof

Step	Hyp	Ref	Expression
1		lidlincl.1	|- U = ( LIdeal ` R )
2		eqid	|- ( Base ` R ) = ( Base ` R )
3	2 1	lidlacs	|- ( R e. Ring -> U e. ( ACS ` ( Base ` R ) ) )
4	3	acsmred	|- ( R e. Ring -> U e. ( Moore ` ( Base ` R ) ) )
5		mreincl	|- ( ( U e. ( Moore ` ( Base ` R ) ) /\ I e. U /\ J e. U ) -> ( I i^i J ) e. U )
6	4 5	syl3an1	|- ( ( R e. Ring /\ I e. U /\ J e. U ) -> ( I i^i J ) e. U )