Metamath Proof Explorer


Theorem ssmxidllem

Description: The set P used in the proof of ssmxidl satisfies the condition of Zorn's Lemma. (Contributed by Thierry Arnoux, 10-Apr-2024)

Ref Expression
Hypotheses ssmxidl.1
|- B = ( Base ` R )
ssmxidllem.1
|- P = { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) }
ssmxidllem.2
|- ( ph -> R e. Ring )
ssmxidllem.3
|- ( ph -> I e. ( LIdeal ` R ) )
ssmxidllem.4
|- ( ph -> I =/= B )
ssmxidllem2.1
|- ( ph -> Z C_ P )
ssmxidllem2.2
|- ( ph -> Z =/= (/) )
ssmxidllem2.3
|- ( ph -> [C.] Or Z )
Assertion ssmxidllem
|- ( ph -> U. Z e. P )

Proof

Step Hyp Ref Expression
1 ssmxidl.1
 |-  B = ( Base ` R )
2 ssmxidllem.1
 |-  P = { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) }
3 ssmxidllem.2
 |-  ( ph -> R e. Ring )
4 ssmxidllem.3
 |-  ( ph -> I e. ( LIdeal ` R ) )
5 ssmxidllem.4
 |-  ( ph -> I =/= B )
6 ssmxidllem2.1
 |-  ( ph -> Z C_ P )
7 ssmxidllem2.2
 |-  ( ph -> Z =/= (/) )
8 ssmxidllem2.3
 |-  ( ph -> [C.] Or Z )
9 neeq1
 |-  ( p = U. Z -> ( p =/= B <-> U. Z =/= B ) )
10 sseq2
 |-  ( p = U. Z -> ( I C_ p <-> I C_ U. Z ) )
11 9 10 anbi12d
 |-  ( p = U. Z -> ( ( p =/= B /\ I C_ p ) <-> ( U. Z =/= B /\ I C_ U. Z ) ) )
12 2 ssrab3
 |-  P C_ ( LIdeal ` R )
13 6 12 sstrdi
 |-  ( ph -> Z C_ ( LIdeal ` R ) )
14 13 sselda
 |-  ( ( ph /\ j e. Z ) -> j e. ( LIdeal ` R ) )
15 eqid
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
16 1 15 lidlss
 |-  ( j e. ( LIdeal ` R ) -> j C_ B )
17 14 16 syl
 |-  ( ( ph /\ j e. Z ) -> j C_ B )
18 17 ralrimiva
 |-  ( ph -> A. j e. Z j C_ B )
19 unissb
 |-  ( U. Z C_ B <-> A. j e. Z j C_ B )
20 18 19 sylibr
 |-  ( ph -> U. Z C_ B )
21 3 adantr
 |-  ( ( ph /\ j e. Z ) -> R e. Ring )
22 eqid
 |-  ( 0g ` R ) = ( 0g ` R )
23 15 22 lidl0cl
 |-  ( ( R e. Ring /\ j e. ( LIdeal ` R ) ) -> ( 0g ` R ) e. j )
24 21 14 23 syl2anc
 |-  ( ( ph /\ j e. Z ) -> ( 0g ` R ) e. j )
25 n0i
 |-  ( ( 0g ` R ) e. j -> -. j = (/) )
26 24 25 syl
 |-  ( ( ph /\ j e. Z ) -> -. j = (/) )
27 26 reximdva0
 |-  ( ( ph /\ Z =/= (/) ) -> E. j e. Z -. j = (/) )
28 7 27 mpdan
 |-  ( ph -> E. j e. Z -. j = (/) )
29 rexnal
 |-  ( E. j e. Z -. j = (/) <-> -. A. j e. Z j = (/) )
30 28 29 sylib
 |-  ( ph -> -. A. j e. Z j = (/) )
31 uni0c
 |-  ( U. Z = (/) <-> A. j e. Z j = (/) )
32 31 necon3abii
 |-  ( U. Z =/= (/) <-> -. A. j e. Z j = (/) )
33 30 32 sylibr
 |-  ( ph -> U. Z =/= (/) )
34 eluni2
 |-  ( a e. U. Z <-> E. i e. Z a e. i )
35 eluni2
 |-  ( b e. U. Z <-> E. j e. Z b e. j )
36 34 35 anbi12i
 |-  ( ( a e. U. Z /\ b e. U. Z ) <-> ( E. i e. Z a e. i /\ E. j e. Z b e. j ) )
37 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 ) )
38 3 ad6antr
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> R e. Ring )
39 13 ad5antr
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) -> Z C_ ( LIdeal ` R ) )
40 simp-4r
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) -> j e. Z )
41 39 40 sseldd
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) -> j e. ( LIdeal ` R ) )
42 41 adantr
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> j e. ( LIdeal ` R ) )
43 simp-6r
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> x e. B )
44 simpr
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> i C_ j )
45 simplr
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> a e. i )
46 44 45 sseldd
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> a e. j )
47 eqid
 |-  ( .r ` R ) = ( .r ` R )
48 15 1 47 lidlmcl
 |-  ( ( ( R e. Ring /\ j e. ( LIdeal ` R ) ) /\ ( x e. B /\ a e. j ) ) -> ( x ( .r ` R ) a ) e. j )
49 38 42 43 46 48 syl22anc
 |-  ( ( ( ( ( ( ( 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 )
50 simp-4r
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> b e. j )
51 eqid
 |-  ( +g ` R ) = ( +g ` R )
52 15 51 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 )
53 38 42 49 50 52 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 )
54 40 adantr
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> j e. Z )
55 elunii
 |-  ( ( ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. j /\ j e. Z ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z )
56 53 54 55 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 )
57 3 ad6antr
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> R e. Ring )
58 39 adantr
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> Z C_ ( LIdeal ` R ) )
59 simplr
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) -> i e. Z )
60 59 adantr
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> i e. Z )
61 58 60 sseldd
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> i e. ( LIdeal ` R ) )
62 simp-6r
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> x e. B )
63 simplr
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> a e. i )
64 15 1 47 lidlmcl
 |-  ( ( ( R e. Ring /\ i e. ( LIdeal ` R ) ) /\ ( x e. B /\ a e. i ) ) -> ( x ( .r ` R ) a ) e. i )
65 57 61 62 63 64 syl22anc
 |-  ( ( ( ( ( ( ( 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 )
66 simpr
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> j C_ i )
67 simp-4r
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> b e. j )
68 66 67 sseldd
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> b e. i )
69 15 51 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 )
70 57 61 65 68 69 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 )
71 elunii
 |-  ( ( ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. i /\ i e. Z ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z )
72 70 60 71 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 )
73 8 ad5antr
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) -> [C.] Or Z )
74 sorpssi
 |-  ( ( [C.] Or Z /\ ( i e. Z /\ j e. Z ) ) -> ( i C_ j \/ j C_ i ) )
75 73 59 40 74 syl12anc
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) -> ( i C_ j \/ j C_ i ) )
76 56 72 75 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 )
77 76 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 )
78 77 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 )
79 37 78 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 )
80 79 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 )
81 80 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 )
82 36 81 sylan2b
 |-  ( ( ( ph /\ x e. B ) /\ ( a e. U. Z /\ b e. U. Z ) ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z )
83 82 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 )
84 83 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 )
85 15 1 51 47 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 ) )
86 20 33 84 85 syl3anbrc
 |-  ( ph -> U. Z e. ( LIdeal ` R ) )
87 6 sselda
 |-  ( ( ph /\ j e. Z ) -> j e. P )
88 neeq1
 |-  ( p = j -> ( p =/= B <-> j =/= B ) )
89 sseq2
 |-  ( p = j -> ( I C_ p <-> I C_ j ) )
90 88 89 anbi12d
 |-  ( p = j -> ( ( p =/= B /\ I C_ p ) <-> ( j =/= B /\ I C_ j ) ) )
91 90 2 elrab2
 |-  ( j e. P <-> ( j e. ( LIdeal ` R ) /\ ( j =/= B /\ I C_ j ) ) )
92 87 91 sylib
 |-  ( ( ph /\ j e. Z ) -> ( j e. ( LIdeal ` R ) /\ ( j =/= B /\ I C_ j ) ) )
93 92 simprld
 |-  ( ( ph /\ j e. Z ) -> j =/= B )
94 eqid
 |-  ( 1r ` R ) = ( 1r ` R )
95 1 94 pridln1
 |-  ( ( R e. Ring /\ j e. ( LIdeal ` R ) /\ j =/= B ) -> -. ( 1r ` R ) e. j )
96 21 14 93 95 syl3anc
 |-  ( ( ph /\ j e. Z ) -> -. ( 1r ` R ) e. j )
97 96 nrexdv
 |-  ( ph -> -. E. j e. Z ( 1r ` R ) e. j )
98 eluni2
 |-  ( ( 1r ` R ) e. U. Z <-> E. j e. Z ( 1r ` R ) e. j )
99 97 98 sylnibr
 |-  ( ph -> -. ( 1r ` R ) e. U. Z )
100 15 1 94 lidl1el
 |-  ( ( R e. Ring /\ U. Z e. ( LIdeal ` R ) ) -> ( ( 1r ` R ) e. U. Z <-> U. Z = B ) )
101 3 86 100 syl2anc
 |-  ( ph -> ( ( 1r ` R ) e. U. Z <-> U. Z = B ) )
102 101 necon3bbid
 |-  ( ph -> ( -. ( 1r ` R ) e. U. Z <-> U. Z =/= B ) )
103 99 102 mpbid
 |-  ( ph -> U. Z =/= B )
104 92 simprrd
 |-  ( ( ph /\ j e. Z ) -> I C_ j )
105 104 ralrimiva
 |-  ( ph -> A. j e. Z I C_ j )
106 ssint
 |-  ( I C_ |^| Z <-> A. j e. Z I C_ j )
107 105 106 sylibr
 |-  ( ph -> I C_ |^| Z )
108 intssuni
 |-  ( Z =/= (/) -> |^| Z C_ U. Z )
109 7 108 syl
 |-  ( ph -> |^| Z C_ U. Z )
110 107 109 sstrd
 |-  ( ph -> I C_ U. Z )
111 103 110 jca
 |-  ( ph -> ( U. Z =/= B /\ I C_ U. Z ) )
112 11 86 111 elrabd
 |-  ( ph -> U. Z e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } )
113 112 2 eleqtrrdi
 |-  ( ph -> U. Z e. P )