Metamath Proof Explorer

Theorem ssdifidllem

Description: Lemma for ssdifidl : The set P used in the proof of ssdifidl satisfies the condition of Zorn's Lemma. (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 ) }
ssdifidllem.7 
|- ( ph -> Z C_ P )
ssdifidllem.8 
|- ( ph -> Z =/= (/) )
ssdifidllem.9 
|- ( ph -> [C.] Or Z )
Assertion ssdifidllem 
|- ( ph -> U. Z e. P )

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 ssdifidllem.7 
 |-  ( ph -> Z C_ P )
8 ssdifidllem.8 
 |-  ( ph -> Z =/= (/) )
9 ssdifidllem.9 
 |-  ( ph -> [C.] Or Z )
10 ineq2 
 |-  ( p = U. Z -> ( S i^i p ) = ( S i^i U. Z ) )
11 10 eqeq1d 
 |-  ( p = U. Z -> ( ( S i^i p ) = (/) <-> ( S i^i U. Z ) = (/) ) )
12 sseq2 
 |-  ( p = U. Z -> ( I C_ p <-> I C_ U. Z ) )
13 11 12 anbi12d 
 |-  ( p = U. Z -> ( ( ( S i^i p ) = (/) /\ I C_ p ) <-> ( ( S i^i U. Z ) = (/) /\ I C_ U. Z ) ) )
14 6 ssrab3 
 |-  P C_ ( LIdeal ` R )
15 7 14 sstrdi 
 |-  ( ph -> Z C_ ( LIdeal ` R ) )
16 15 sselda 
 |-  ( ( ph /\ j e. Z ) -> j e. ( LIdeal ` R ) )
17 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
18 1 17 lidlss 
 |-  ( j e. ( LIdeal ` R ) -> j C_ B )
19 16 18 syl 
 |-  ( ( ph /\ j e. Z ) -> j C_ B )
20 19 ralrimiva 
 |-  ( ph -> A. j e. Z j C_ B )
21 unissb 
 |-  ( U. Z C_ B <-> A. j e. Z j C_ B )
22 20 21 sylibr 
 |-  ( ph -> U. Z C_ B )
23 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
24 17 23 lidl0cl 
 |-  ( ( R e. Ring /\ j e. ( LIdeal ` R ) ) -> ( 0g ` R ) e. j )
25 2 16 24 syl2an2r 
 |-  ( ( ph /\ j e. Z ) -> ( 0g ` R ) e. j )
26 n0i 
 |-  ( ( 0g ` R ) e. j -> -. j = (/) )
27 25 26 syl 
 |-  ( ( ph /\ j e. Z ) -> -. j = (/) )
28 27 reximdva0 
 |-  ( ( ph /\ Z =/= (/) ) -> E. j e. Z -. j = (/) )
29 8 28 mpdan 
 |-  ( ph -> E. j e. Z -. j = (/) )
30 rexnal 
 |-  ( E. j e. Z -. j = (/) <-> -. A. j e. Z j = (/) )
31 29 30 sylib 
 |-  ( ph -> -. A. j e. Z j = (/) )
32 uni0c 
 |-  ( U. Z = (/) <-> A. j e. Z j = (/) )
33 32 necon3abii 
 |-  ( U. Z =/= (/) <-> -. A. j e. Z j = (/) )
34 31 33 sylibr 
 |-  ( ph -> U. Z =/= (/) )
35 eluni2 
 |-  ( a e. U. Z <-> E. i e. Z a e. i )
36 eluni2 
 |-  ( b e. U. Z <-> E. j e. Z b e. j )
37 35 36 anbi12i 
 |-  ( ( a e. U. Z /\ b e. U. Z ) <-> ( E. i e. Z a e. i /\ E. j e. Z b e. j ) )
38 an32 
 |-  ( ( ( ( ph /\ x e. B ) /\ E. i e. Z a e. i ) /\ j e. Z ) <-> ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ E. i e. Z a e. i ) )
39 2 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> R e. Ring )
40 15 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> Z C_ ( LIdeal ` R ) )
41 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> j e. Z )
42 40 41 sseldd 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> j e. ( LIdeal ` R ) )
43 eqid 
 |-  ( .r ` R ) = ( .r ` R )
44 simp-6r 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> x e. B )
45 simpr 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> i C_ j )
46 simplr 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> a e. i )
47 45 46 sseldd 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> a e. j )
48 17 1 43 39 42 44 47 lidlmcld 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> ( x ( .r ` R ) a ) e. j )
49 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> b e. j )
50 eqid 
 |-  ( +g ` R ) = ( +g ` R )
51 17 50 lidlacl 
 |-  ( ( ( R e. Ring /\ j e. ( LIdeal ` R ) ) /\ ( ( x ( .r ` R ) a ) e. j /\ b e. j ) ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. j )
52 39 42 48 49 51 syl22anc 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. j )
53 elunii 
 |-  ( ( ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. j /\ j e. Z ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z )
54 52 41 53 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z )
55 2 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> R e. Ring )
56 15 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> Z C_ ( LIdeal ` R ) )
57 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> i e. Z )
58 56 57 sseldd 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> i e. ( LIdeal ` R ) )
59 simp-6r 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> x e. B )
60 simplr 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> a e. i )
61 17 1 43 55 58 59 60 lidlmcld 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> ( x ( .r ` R ) a ) e. i )
62 simpr 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> j C_ i )
63 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> b e. j )
64 62 63 sseldd 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> b e. i )
65 17 50 lidlacl 
 |-  ( ( ( R e. Ring /\ i e. ( LIdeal ` R ) ) /\ ( ( x ( .r ` R ) a ) e. i /\ b e. i ) ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. i )
66 55 58 61 64 65 syl22anc 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. i )
67 elunii 
 |-  ( ( ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. i /\ i e. Z ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z )
68 66 57 67 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z )
69 9 ad5antr 
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) -> [C.] Or Z )
70 simplr 
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) -> i e. Z )
71 simp-4r 
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) -> j e. Z )
72 sorpssi 
 |-  ( ( [C.] Or Z /\ ( i e. Z /\ j e. Z ) ) -> ( i C_ j \/ j C_ i ) )
73 69 70 71 72 syl12anc 
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) -> ( i C_ j \/ j C_ i ) )
74 54 68 73 mpjaodan 
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z )
75 74 r19.29an 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ E. i e. Z a e. i ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z )
76 75 an32s 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ E. i e. Z a e. i ) /\ b e. j ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z )
77 38 76 sylanb 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ E. i e. Z a e. i ) /\ j e. Z ) /\ b e. j ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z )
78 77 r19.29an 
 |-  ( ( ( ( ph /\ x e. B ) /\ E. i e. Z a e. i ) /\ E. j e. Z b e. j ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z )
79 78 anasss 
 |-  ( ( ( ph /\ x e. B ) /\ ( E. i e. Z a e. i /\ E. j e. Z b e. j ) ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z )
80 37 79 sylan2b 
 |-  ( ( ( ph /\ x e. B ) /\ ( a e. U. Z /\ b e. U. Z ) ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z )
81 80 ralrimivva 
 |-  ( ( ph /\ x e. B ) -> A. a e. U. Z A. b e. U. Z ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z )
82 81 ralrimiva 
 |-  ( ph -> A. x e. B A. a e. U. Z A. b e. U. Z ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z )
83 17 1 50 43 islidl 
 |-  ( U. Z e. ( LIdeal ` R ) <-> ( U. Z C_ B /\ U. Z =/= (/) /\ A. x e. B A. a e. U. Z A. b e. U. Z ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z ) )
84 22 34 82 83 syl3anbrc 
 |-  ( ph -> U. Z e. ( LIdeal ` R ) )
85 iunss1 
 |-  ( Z C_ P -> U_ j e. Z ( S i^i j ) C_ U_ j e. P ( S i^i j ) )
86 7 85 syl 
 |-  ( ph -> U_ j e. Z ( S i^i j ) C_ U_ j e. P ( S i^i j ) )
87 uniin2 
 |-  U_ j e. Z ( S i^i j ) = ( S i^i U. Z )
88 87 a1i 
 |-  ( ph -> U_ j e. Z ( S i^i j ) = ( S i^i U. Z ) )
89 14 a1i 
 |-  ( ph -> P C_ ( LIdeal ` R ) )
90 89 sselda 
 |-  ( ( ph /\ j e. P ) -> j e. ( LIdeal ` R ) )
91 simpr 
 |-  ( ( ph /\ j e. P ) -> j e. P )
92 91 6 eleqtrdi 
 |-  ( ( ph /\ j e. P ) -> j e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ I C_ p ) } )
93 ineq2 
 |-  ( p = j -> ( S i^i p ) = ( S i^i j ) )
94 93 eqeq1d 
 |-  ( p = j -> ( ( S i^i p ) = (/) <-> ( S i^i j ) = (/) ) )
95 sseq2 
 |-  ( p = j -> ( I C_ p <-> I C_ j ) )
96 94 95 anbi12d 
 |-  ( p = j -> ( ( ( S i^i p ) = (/) /\ I C_ p ) <-> ( ( S i^i j ) = (/) /\ I C_ j ) ) )
97 96 elrab3 
 |-  ( j e. ( LIdeal ` R ) -> ( j e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ I C_ p ) } <-> ( ( S i^i j ) = (/) /\ I C_ j ) ) )
98 97 simprbda 
 |-  ( ( j e. ( LIdeal ` R ) /\ j e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ I C_ p ) } ) -> ( S i^i j ) = (/) )
99 90 92 98 syl2anc 
 |-  ( ( ph /\ j e. P ) -> ( S i^i j ) = (/) )
100 99 iuneq2dv 
 |-  ( ph -> U_ j e. P ( S i^i j ) = U_ j e. P (/) )
101 iun0 
 |-  U_ j e. P (/) = (/)
102 100 101 eqtrdi 
 |-  ( ph -> U_ j e. P ( S i^i j ) = (/) )
103 86 88 102 3sstr3d 
 |-  ( ph -> ( S i^i U. Z ) C_ (/) )
104 ss0 
 |-  ( ( S i^i U. Z ) C_ (/) -> ( S i^i U. Z ) = (/) )
105 103 104 syl 
 |-  ( ph -> ( S i^i U. Z ) = (/) )
106 7 sselda 
 |-  ( ( ph /\ j e. Z ) -> j e. P )
107 96 6 elrab2 
 |-  ( j e. P <-> ( j e. ( LIdeal ` R ) /\ ( ( S i^i j ) = (/) /\ I C_ j ) ) )
108 106 107 sylib 
 |-  ( ( ph /\ j e. Z ) -> ( j e. ( LIdeal ` R ) /\ ( ( S i^i j ) = (/) /\ I C_ j ) ) )
109 108 simprrd 
 |-  ( ( ph /\ j e. Z ) -> I C_ j )
110 109 ralrimiva 
 |-  ( ph -> A. j e. Z I C_ j )
111 ssint 
 |-  ( I C_ |^| Z <-> A. j e. Z I C_ j )
112 110 111 sylibr 
 |-  ( ph -> I C_ |^| Z )
113 intssuni 
 |-  ( Z =/= (/) -> |^| Z C_ U. Z )
114 8 113 syl 
 |-  ( ph -> |^| Z C_ U. Z )
115 112 114 sstrd 
 |-  ( ph -> I C_ U. Z )
116 105 115 jca 
 |-  ( ph -> ( ( S i^i U. Z ) = (/) /\ I C_ U. Z ) )
117 13 84 116 elrabd 
 |-  ( ph -> U. Z e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ I C_ p ) } )
118 117 6 eleqtrrdi 
 |-  ( ph -> U. Z e. P )