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 LIdeal R | p B I p
ssmxidllem.2 φ R Ring
ssmxidllem.3 φ I LIdeal R
ssmxidllem.4 φ I B
ssmxidllem2.1 φ Z P
ssmxidllem2.2 φ Z
ssmxidllem2.3 φ [⊂] Or Z
Assertion ssmxidllem φ Z P

Proof

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