Metamath Proof Explorer


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 Ring I U J U I J U

Proof

Step Hyp Ref Expression
1 lidlincl.1 U = LIdeal R
2 eqid Base R = Base R
3 2 1 lidlacs R Ring U ACS Base R
4 3 acsmred R Ring U Moore Base R
5 mreincl U Moore Base R I U J U I J U
6 4 5 syl3an1 R Ring I U J U I J U