Metamath Proof Explorer

Theorem lidlunin0

Description: The union of a nonempty subset of ideals in a ring is nonempty. (Contributed by AV, 28-Jun-2026)

Ref Expression
Assertion lidlunin0 
|- ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) -> U. C =/= (/) )

Proof

Step Hyp Ref Expression
1 n0 
 |-  ( C =/= (/) <-> E. y y e. C )
2 simpl 
 |-  ( ( R e. Ring /\ C C_ ( LIdeal ` R ) ) -> R e. Ring )
3 ssel 
 |-  ( C C_ ( LIdeal ` R ) -> ( y e. C -> y e. ( LIdeal ` R ) ) )
4 3 adantl 
 |-  ( ( R e. Ring /\ C C_ ( LIdeal ` R ) ) -> ( y e. C -> y e. ( LIdeal ` R ) ) )
5 4 imp 
 |-  ( ( ( R e. Ring /\ C C_ ( LIdeal ` R ) ) /\ y e. C ) -> y e. ( LIdeal ` R ) )
6 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
7 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
8 6 7 lidl0cl 
 |-  ( ( R e. Ring /\ y e. ( LIdeal ` R ) ) -> ( 0g ` R ) e. y )
9 2 5 8 syl2an2r 
 |-  ( ( ( R e. Ring /\ C C_ ( LIdeal ` R ) ) /\ y e. C ) -> ( 0g ` R ) e. y )
10 simpr 
 |-  ( ( ( R e. Ring /\ C C_ ( LIdeal ` R ) ) /\ y e. C ) -> y e. C )
11 9 10 jca 
 |-  ( ( ( R e. Ring /\ C C_ ( LIdeal ` R ) ) /\ y e. C ) -> ( ( 0g ` R ) e. y /\ y e. C ) )
12 11 ex 
 |-  ( ( R e. Ring /\ C C_ ( LIdeal ` R ) ) -> ( y e. C -> ( ( 0g ` R ) e. y /\ y e. C ) ) )
13 12 eximdv 
 |-  ( ( R e. Ring /\ C C_ ( LIdeal ` R ) ) -> ( E. y y e. C -> E. y ( ( 0g ` R ) e. y /\ y e. C ) ) )
14 1 13 biimtrid 
 |-  ( ( R e. Ring /\ C C_ ( LIdeal ` R ) ) -> ( C =/= (/) -> E. y ( ( 0g ` R ) e. y /\ y e. C ) ) )
15 14 ex 
 |-  ( R e. Ring -> ( C C_ ( LIdeal ` R ) -> ( C =/= (/) -> E. y ( ( 0g ` R ) e. y /\ y e. C ) ) ) )
16 15 com23 
 |-  ( R e. Ring -> ( C =/= (/) -> ( C C_ ( LIdeal ` R ) -> E. y ( ( 0g ` R ) e. y /\ y e. C ) ) ) )
17 16 3imp 
 |-  ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) -> E. y ( ( 0g ` R ) e. y /\ y e. C ) )
18 eluni 
 |-  ( ( 0g ` R ) e. U. C <-> E. y ( ( 0g ` R ) e. y /\ y e. C ) )
19 17 18 sylibr 
 |-  ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) -> ( 0g ` R ) e. U. C )
20 19 ne0d 
 |-  ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) -> U. C =/= (/) )