This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssdifidl

Description: Let R be a ring, and let I be an ideal of R disjoint with a set S . Then there exists an ideal i , maximal among the set P of ideals containing I and disjoint with S . (Contributed by Thierry Arnoux, 3-Jun-2025)

Ref Expression
Hypotheses ssdifidl.1 
|- B = ( Base ` R )
ssdifidl.2 
|- ( ph -> R e. Ring )
ssdifidl.3 
|- ( ph -> I e. ( LIdeal ` R ) )
ssdifidl.4 
|- ( ph -> S C_ B )
ssdifidl.5 
|- ( ph -> ( S i^i I ) = (/) )
ssdifidl.6 
|- P = { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ I C_ p ) }
Assertion ssdifidl 
|- ( ph -> E. i e. P A. j e. P -. i C. j )

Proof

Step Hyp Ref Expression
1 ssdifidl.1 
 |-  B = ( Base ` R )
2 ssdifidl.2 
 |-  ( ph -> R e. Ring )
3 ssdifidl.3 
 |-  ( ph -> I e. ( LIdeal ` R ) )
4 ssdifidl.4 
 |-  ( ph -> S C_ B )
5 ssdifidl.5 
 |-  ( ph -> ( S i^i I ) = (/) )
6 ssdifidl.6 
 |-  P = { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ I C_ p ) }
7 ineq2 
 |-  ( p = I -> ( S i^i p ) = ( S i^i I ) )
8 7 eqeq1d 
 |-  ( p = I -> ( ( S i^i p ) = (/) <-> ( S i^i I ) = (/) ) )
9 sseq2 
 |-  ( p = I -> ( I C_ p <-> I C_ I ) )
10 8 9 anbi12d 
 |-  ( p = I -> ( ( ( S i^i p ) = (/) /\ I C_ p ) <-> ( ( S i^i I ) = (/) /\ I C_ I ) ) )
11 ssidd 
 |-  ( ph -> I C_ I )
12 5 11 jca 
 |-  ( ph -> ( ( S i^i I ) = (/) /\ I C_ I ) )
13 10 3 12 elrabd 
 |-  ( ph -> I e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ I C_ p ) } )
14 13 6 eleqtrrdi 
 |-  ( ph -> I e. P )
15 14 ne0d 
 |-  ( ph -> P =/= (/) )
16 2 adantr 
 |-  ( ( ph /\ ( z C_ P /\ z =/= (/) /\ [C.] Or z ) ) -> R e. Ring )
17 3 adantr 
 |-  ( ( ph /\ ( z C_ P /\ z =/= (/) /\ [C.] Or z ) ) -> I e. ( LIdeal ` R ) )
18 4 adantr 
 |-  ( ( ph /\ ( z C_ P /\ z =/= (/) /\ [C.] Or z ) ) -> S C_ B )
19 5 adantr 
 |-  ( ( ph /\ ( z C_ P /\ z =/= (/) /\ [C.] Or z ) ) -> ( S i^i I ) = (/) )
20 simpr1 
 |-  ( ( ph /\ ( z C_ P /\ z =/= (/) /\ [C.] Or z ) ) -> z C_ P )
21 simpr2 
 |-  ( ( ph /\ ( z C_ P /\ z =/= (/) /\ [C.] Or z ) ) -> z =/= (/) )
22 simpr3 
 |-  ( ( ph /\ ( z C_ P /\ z =/= (/) /\ [C.] Or z ) ) -> [C.] Or z )
23 1 16 17 18 19 6 20 21 22 ssdifidllem 
 |-  ( ( ph /\ ( z C_ P /\ z =/= (/) /\ [C.] Or z ) ) -> U. z e. P )
24 23 ex 
 |-  ( ph -> ( ( z C_ P /\ z =/= (/) /\ [C.] Or z ) -> U. z e. P ) )
25 24 alrimiv 
 |-  ( ph -> A. z ( ( z C_ P /\ z =/= (/) /\ [C.] Or z ) -> U. z e. P ) )
26 fvex 
 |-  ( LIdeal ` R ) e. _V
27 6 26 rabex2 
 |-  P e. _V
28 27 zornn0 
 |-  ( ( P =/= (/) /\ A. z ( ( z C_ P /\ z =/= (/) /\ [C.] Or z ) -> U. z e. P ) ) -> E. i e. P A. j e. P -. i C. j )
29 15 25 28 syl2anc 
 |-  ( ph -> E. i e. P A. j e. P -. i C. j )