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

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 )