Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ssmxidllem Structured version   Visualization version   GIF version

Theorem ssmxidllem 32584
Description: The set 𝑃 used in the proof of ssmxidl 32585 satisfies the condition of Zorn's Lemma. (Contributed by Thierry Arnoux, 10-Apr-2024.)
Hypotheses
Ref Expression
ssmxidl.1 𝐡 = (Baseβ€˜π‘…)
ssmxidllem.1 𝑃 = {𝑝 ∈ (LIdealβ€˜π‘…) ∣ (𝑝 β‰  𝐡 ∧ 𝐼 βŠ† 𝑝)}
ssmxidllem.2 (πœ‘ β†’ 𝑅 ∈ Ring)
ssmxidllem.3 (πœ‘ β†’ 𝐼 ∈ (LIdealβ€˜π‘…))
ssmxidllem.4 (πœ‘ β†’ 𝐼 β‰  𝐡)
ssmxidllem2.1 (πœ‘ β†’ 𝑍 βŠ† 𝑃)
ssmxidllem2.2 (πœ‘ β†’ 𝑍 β‰  βˆ…)
ssmxidllem2.3 (πœ‘ β†’ [⊊] Or 𝑍)
Assertion
Ref Expression
ssmxidllem (πœ‘ β†’ βˆͺ 𝑍 ∈ 𝑃)
Distinct variable groups:   𝐡,𝑝   𝐼,𝑝   𝑅,𝑝   𝑍,𝑝
Allowed substitution hints:   πœ‘(𝑝)   𝑃(𝑝)

Proof of Theorem ssmxidllem
Dummy variables π‘Ž 𝑏 𝑖 π‘₯ 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 neeq1 3003 . . . 4 (𝑝 = βˆͺ 𝑍 β†’ (𝑝 β‰  𝐡 ↔ βˆͺ 𝑍 β‰  𝐡))
2 sseq2 4008 . . . 4 (𝑝 = βˆͺ 𝑍 β†’ (𝐼 βŠ† 𝑝 ↔ 𝐼 βŠ† βˆͺ 𝑍))
31, 2anbi12d 631 . . 3 (𝑝 = βˆͺ 𝑍 β†’ ((𝑝 β‰  𝐡 ∧ 𝐼 βŠ† 𝑝) ↔ (βˆͺ 𝑍 β‰  𝐡 ∧ 𝐼 βŠ† βˆͺ 𝑍)))
4 ssmxidllem2.1 . . . . . . . . 9 (πœ‘ β†’ 𝑍 βŠ† 𝑃)
5 ssmxidllem.1 . . . . . . . . . 10 𝑃 = {𝑝 ∈ (LIdealβ€˜π‘…) ∣ (𝑝 β‰  𝐡 ∧ 𝐼 βŠ† 𝑝)}
65ssrab3 4080 . . . . . . . . 9 𝑃 βŠ† (LIdealβ€˜π‘…)
74, 6sstrdi 3994 . . . . . . . 8 (πœ‘ β†’ 𝑍 βŠ† (LIdealβ€˜π‘…))
87sselda 3982 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ 𝑍) β†’ 𝑗 ∈ (LIdealβ€˜π‘…))
9 ssmxidl.1 . . . . . . . 8 𝐡 = (Baseβ€˜π‘…)
10 eqid 2732 . . . . . . . 8 (LIdealβ€˜π‘…) = (LIdealβ€˜π‘…)
119, 10lidlss 20832 . . . . . . 7 (𝑗 ∈ (LIdealβ€˜π‘…) β†’ 𝑗 βŠ† 𝐡)
128, 11syl 17 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ 𝑍) β†’ 𝑗 βŠ† 𝐡)
1312ralrimiva 3146 . . . . 5 (πœ‘ β†’ βˆ€π‘— ∈ 𝑍 𝑗 βŠ† 𝐡)
14 unissb 4943 . . . . 5 (βˆͺ 𝑍 βŠ† 𝐡 ↔ βˆ€π‘— ∈ 𝑍 𝑗 βŠ† 𝐡)
1513, 14sylibr 233 . . . 4 (πœ‘ β†’ βˆͺ 𝑍 βŠ† 𝐡)
16 ssmxidllem2.2 . . . . . . 7 (πœ‘ β†’ 𝑍 β‰  βˆ…)
17 ssmxidllem.2 . . . . . . . . . . 11 (πœ‘ β†’ 𝑅 ∈ Ring)
1817adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ 𝑍) β†’ 𝑅 ∈ Ring)
19 eqid 2732 . . . . . . . . . . 11 (0gβ€˜π‘…) = (0gβ€˜π‘…)
2010, 19lidl0cl 20834 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdealβ€˜π‘…)) β†’ (0gβ€˜π‘…) ∈ 𝑗)
2118, 8, 20syl2anc 584 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ 𝑍) β†’ (0gβ€˜π‘…) ∈ 𝑗)
22 n0i 4333 . . . . . . . . 9 ((0gβ€˜π‘…) ∈ 𝑗 β†’ Β¬ 𝑗 = βˆ…)
2321, 22syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ 𝑍) β†’ Β¬ 𝑗 = βˆ…)
2423reximdva0 4351 . . . . . . 7 ((πœ‘ ∧ 𝑍 β‰  βˆ…) β†’ βˆƒπ‘— ∈ 𝑍 Β¬ 𝑗 = βˆ…)
2516, 24mpdan 685 . . . . . 6 (πœ‘ β†’ βˆƒπ‘— ∈ 𝑍 Β¬ 𝑗 = βˆ…)
26 rexnal 3100 . . . . . 6 (βˆƒπ‘— ∈ 𝑍 Β¬ 𝑗 = βˆ… ↔ Β¬ βˆ€π‘— ∈ 𝑍 𝑗 = βˆ…)
2725, 26sylib 217 . . . . 5 (πœ‘ β†’ Β¬ βˆ€π‘— ∈ 𝑍 𝑗 = βˆ…)
28 uni0c 4938 . . . . . 6 (βˆͺ 𝑍 = βˆ… ↔ βˆ€π‘— ∈ 𝑍 𝑗 = βˆ…)
2928necon3abii 2987 . . . . 5 (βˆͺ 𝑍 β‰  βˆ… ↔ Β¬ βˆ€π‘— ∈ 𝑍 𝑗 = βˆ…)
3027, 29sylibr 233 . . . 4 (πœ‘ β†’ βˆͺ 𝑍 β‰  βˆ…)
31 eluni2 4912 . . . . . . . 8 (π‘Ž ∈ βˆͺ 𝑍 ↔ βˆƒπ‘– ∈ 𝑍 π‘Ž ∈ 𝑖)
32 eluni2 4912 . . . . . . . 8 (𝑏 ∈ βˆͺ 𝑍 ↔ βˆƒπ‘— ∈ 𝑍 𝑏 ∈ 𝑗)
3331, 32anbi12i 627 . . . . . . 7 ((π‘Ž ∈ βˆͺ 𝑍 ∧ 𝑏 ∈ βˆͺ 𝑍) ↔ (βˆƒπ‘– ∈ 𝑍 π‘Ž ∈ 𝑖 ∧ βˆƒπ‘— ∈ 𝑍 𝑏 ∈ 𝑗))
34 an32 644 . . . . . . . . . 10 ((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ βˆƒπ‘– ∈ 𝑍 π‘Ž ∈ 𝑖) ∧ 𝑗 ∈ 𝑍) ↔ (((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ βˆƒπ‘– ∈ 𝑍 π‘Ž ∈ 𝑖))
3517ad6antr 734 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑖 βŠ† 𝑗) β†’ 𝑅 ∈ Ring)
367ad5antr 732 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) β†’ 𝑍 βŠ† (LIdealβ€˜π‘…))
37 simp-4r 782 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) β†’ 𝑗 ∈ 𝑍)
3836, 37sseldd 3983 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) β†’ 𝑗 ∈ (LIdealβ€˜π‘…))
3938adantr 481 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑖 βŠ† 𝑗) β†’ 𝑗 ∈ (LIdealβ€˜π‘…))
40 simp-6r 786 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑖 βŠ† 𝑗) β†’ π‘₯ ∈ 𝐡)
41 simpr 485 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑖 βŠ† 𝑗) β†’ 𝑖 βŠ† 𝑗)
42 simplr 767 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑖 βŠ† 𝑗) β†’ π‘Ž ∈ 𝑖)
4341, 42sseldd 3983 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑖 βŠ† 𝑗) β†’ π‘Ž ∈ 𝑗)
44 eqid 2732 . . . . . . . . . . . . . . . . 17 (.rβ€˜π‘…) = (.rβ€˜π‘…)
4510, 9, 44lidlmcl 20839 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdealβ€˜π‘…)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘Ž ∈ 𝑗)) β†’ (π‘₯(.rβ€˜π‘…)π‘Ž) ∈ 𝑗)
4635, 39, 40, 43, 45syl22anc 837 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑖 βŠ† 𝑗) β†’ (π‘₯(.rβ€˜π‘…)π‘Ž) ∈ 𝑗)
47 simp-4r 782 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑖 βŠ† 𝑗) β†’ 𝑏 ∈ 𝑗)
48 eqid 2732 . . . . . . . . . . . . . . . 16 (+gβ€˜π‘…) = (+gβ€˜π‘…)
4910, 48lidlacl 20835 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdealβ€˜π‘…)) ∧ ((π‘₯(.rβ€˜π‘…)π‘Ž) ∈ 𝑗 ∧ 𝑏 ∈ 𝑗)) β†’ ((π‘₯(.rβ€˜π‘…)π‘Ž)(+gβ€˜π‘…)𝑏) ∈ 𝑗)
5035, 39, 46, 47, 49syl22anc 837 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑖 βŠ† 𝑗) β†’ ((π‘₯(.rβ€˜π‘…)π‘Ž)(+gβ€˜π‘…)𝑏) ∈ 𝑗)
5137adantr 481 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑖 βŠ† 𝑗) β†’ 𝑗 ∈ 𝑍)
52 elunii 4913 . . . . . . . . . . . . . 14 ((((π‘₯(.rβ€˜π‘…)π‘Ž)(+gβ€˜π‘…)𝑏) ∈ 𝑗 ∧ 𝑗 ∈ 𝑍) β†’ ((π‘₯(.rβ€˜π‘…)π‘Ž)(+gβ€˜π‘…)𝑏) ∈ βˆͺ 𝑍)
5350, 51, 52syl2anc 584 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑖 βŠ† 𝑗) β†’ ((π‘₯(.rβ€˜π‘…)π‘Ž)(+gβ€˜π‘…)𝑏) ∈ βˆͺ 𝑍)
5417ad6antr 734 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑗 βŠ† 𝑖) β†’ 𝑅 ∈ Ring)
5536adantr 481 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑗 βŠ† 𝑖) β†’ 𝑍 βŠ† (LIdealβ€˜π‘…))
56 simplr 767 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) β†’ 𝑖 ∈ 𝑍)
5756adantr 481 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑗 βŠ† 𝑖) β†’ 𝑖 ∈ 𝑍)
5855, 57sseldd 3983 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑗 βŠ† 𝑖) β†’ 𝑖 ∈ (LIdealβ€˜π‘…))
59 simp-6r 786 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑗 βŠ† 𝑖) β†’ π‘₯ ∈ 𝐡)
60 simplr 767 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑗 βŠ† 𝑖) β†’ π‘Ž ∈ 𝑖)
6110, 9, 44lidlmcl 20839 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdealβ€˜π‘…)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘Ž ∈ 𝑖)) β†’ (π‘₯(.rβ€˜π‘…)π‘Ž) ∈ 𝑖)
6254, 58, 59, 60, 61syl22anc 837 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑗 βŠ† 𝑖) β†’ (π‘₯(.rβ€˜π‘…)π‘Ž) ∈ 𝑖)
63 simpr 485 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑗 βŠ† 𝑖) β†’ 𝑗 βŠ† 𝑖)
64 simp-4r 782 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑗 βŠ† 𝑖) β†’ 𝑏 ∈ 𝑗)
6563, 64sseldd 3983 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑗 βŠ† 𝑖) β†’ 𝑏 ∈ 𝑖)
6610, 48lidlacl 20835 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdealβ€˜π‘…)) ∧ ((π‘₯(.rβ€˜π‘…)π‘Ž) ∈ 𝑖 ∧ 𝑏 ∈ 𝑖)) β†’ ((π‘₯(.rβ€˜π‘…)π‘Ž)(+gβ€˜π‘…)𝑏) ∈ 𝑖)
6754, 58, 62, 65, 66syl22anc 837 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑗 βŠ† 𝑖) β†’ ((π‘₯(.rβ€˜π‘…)π‘Ž)(+gβ€˜π‘…)𝑏) ∈ 𝑖)
68 elunii 4913 . . . . . . . . . . . . . 14 ((((π‘₯(.rβ€˜π‘…)π‘Ž)(+gβ€˜π‘…)𝑏) ∈ 𝑖 ∧ 𝑖 ∈ 𝑍) β†’ ((π‘₯(.rβ€˜π‘…)π‘Ž)(+gβ€˜π‘…)𝑏) ∈ βˆͺ 𝑍)
6967, 57, 68syl2anc 584 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) ∧ 𝑗 βŠ† 𝑖) β†’ ((π‘₯(.rβ€˜π‘…)π‘Ž)(+gβ€˜π‘…)𝑏) ∈ βˆͺ 𝑍)
70 ssmxidllem2.3 . . . . . . . . . . . . . . 15 (πœ‘ β†’ [⊊] Or 𝑍)
7170ad5antr 732 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) β†’ [⊊] Or 𝑍)
72 sorpssi 7718 . . . . . . . . . . . . . 14 (( [⊊] Or 𝑍 ∧ (𝑖 ∈ 𝑍 ∧ 𝑗 ∈ 𝑍)) β†’ (𝑖 βŠ† 𝑗 ∨ 𝑗 βŠ† 𝑖))
7371, 56, 37, 72syl12anc 835 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) β†’ (𝑖 βŠ† 𝑗 ∨ 𝑗 βŠ† 𝑖))
7453, 69, 73mpjaodan 957 . . . . . . . . . . . 12 ((((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ 𝑖 ∈ 𝑍) ∧ π‘Ž ∈ 𝑖) β†’ ((π‘₯(.rβ€˜π‘…)π‘Ž)(+gβ€˜π‘…)𝑏) ∈ βˆͺ 𝑍)
7574r19.29an 3158 . . . . . . . . . . 11 (((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) ∧ βˆƒπ‘– ∈ 𝑍 π‘Ž ∈ 𝑖) β†’ ((π‘₯(.rβ€˜π‘…)π‘Ž)(+gβ€˜π‘…)𝑏) ∈ βˆͺ 𝑍)
7675an32s 650 . . . . . . . . . 10 (((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ 𝑗 ∈ 𝑍) ∧ βˆƒπ‘– ∈ 𝑍 π‘Ž ∈ 𝑖) ∧ 𝑏 ∈ 𝑗) β†’ ((π‘₯(.rβ€˜π‘…)π‘Ž)(+gβ€˜π‘…)𝑏) ∈ βˆͺ 𝑍)
7734, 76sylanb 581 . . . . . . . . 9 (((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ βˆƒπ‘– ∈ 𝑍 π‘Ž ∈ 𝑖) ∧ 𝑗 ∈ 𝑍) ∧ 𝑏 ∈ 𝑗) β†’ ((π‘₯(.rβ€˜π‘…)π‘Ž)(+gβ€˜π‘…)𝑏) ∈ βˆͺ 𝑍)
7877r19.29an 3158 . . . . . . . 8 ((((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ βˆƒπ‘– ∈ 𝑍 π‘Ž ∈ 𝑖) ∧ βˆƒπ‘— ∈ 𝑍 𝑏 ∈ 𝑗) β†’ ((π‘₯(.rβ€˜π‘…)π‘Ž)(+gβ€˜π‘…)𝑏) ∈ βˆͺ 𝑍)
7978anasss 467 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ (βˆƒπ‘– ∈ 𝑍 π‘Ž ∈ 𝑖 ∧ βˆƒπ‘— ∈ 𝑍 𝑏 ∈ 𝑗)) β†’ ((π‘₯(.rβ€˜π‘…)π‘Ž)(+gβ€˜π‘…)𝑏) ∈ βˆͺ 𝑍)
8033, 79sylan2b 594 . . . . . 6 (((πœ‘ ∧ π‘₯ ∈ 𝐡) ∧ (π‘Ž ∈ βˆͺ 𝑍 ∧ 𝑏 ∈ βˆͺ 𝑍)) β†’ ((π‘₯(.rβ€˜π‘…)π‘Ž)(+gβ€˜π‘…)𝑏) ∈ βˆͺ 𝑍)
8180ralrimivva 3200 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ 𝐡) β†’ βˆ€π‘Ž ∈ βˆͺ π‘βˆ€π‘ ∈ βˆͺ 𝑍((π‘₯(.rβ€˜π‘…)π‘Ž)(+gβ€˜π‘…)𝑏) ∈ βˆͺ 𝑍)
8281ralrimiva 3146 . . . 4 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘Ž ∈ βˆͺ π‘βˆ€π‘ ∈ βˆͺ 𝑍((π‘₯(.rβ€˜π‘…)π‘Ž)(+gβ€˜π‘…)𝑏) ∈ βˆͺ 𝑍)
8310, 9, 48, 44islidl 20833 . . . 4 (βˆͺ 𝑍 ∈ (LIdealβ€˜π‘…) ↔ (βˆͺ 𝑍 βŠ† 𝐡 ∧ βˆͺ 𝑍 β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘Ž ∈ βˆͺ π‘βˆ€π‘ ∈ βˆͺ 𝑍((π‘₯(.rβ€˜π‘…)π‘Ž)(+gβ€˜π‘…)𝑏) ∈ βˆͺ 𝑍))
8415, 30, 82, 83syl3anbrc 1343 . . 3 (πœ‘ β†’ βˆͺ 𝑍 ∈ (LIdealβ€˜π‘…))
854sselda 3982 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ 𝑍) β†’ 𝑗 ∈ 𝑃)
86 neeq1 3003 . . . . . . . . . . . 12 (𝑝 = 𝑗 β†’ (𝑝 β‰  𝐡 ↔ 𝑗 β‰  𝐡))
87 sseq2 4008 . . . . . . . . . . . 12 (𝑝 = 𝑗 β†’ (𝐼 βŠ† 𝑝 ↔ 𝐼 βŠ† 𝑗))
8886, 87anbi12d 631 . . . . . . . . . . 11 (𝑝 = 𝑗 β†’ ((𝑝 β‰  𝐡 ∧ 𝐼 βŠ† 𝑝) ↔ (𝑗 β‰  𝐡 ∧ 𝐼 βŠ† 𝑗)))
8988, 5elrab2 3686 . . . . . . . . . 10 (𝑗 ∈ 𝑃 ↔ (𝑗 ∈ (LIdealβ€˜π‘…) ∧ (𝑗 β‰  𝐡 ∧ 𝐼 βŠ† 𝑗)))
9085, 89sylib 217 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ 𝑍) β†’ (𝑗 ∈ (LIdealβ€˜π‘…) ∧ (𝑗 β‰  𝐡 ∧ 𝐼 βŠ† 𝑗)))
9190simprld 770 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ 𝑍) β†’ 𝑗 β‰  𝐡)
92 eqid 2732 . . . . . . . . 9 (1rβ€˜π‘…) = (1rβ€˜π‘…)
939, 92pridln1 32556 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdealβ€˜π‘…) ∧ 𝑗 β‰  𝐡) β†’ Β¬ (1rβ€˜π‘…) ∈ 𝑗)
9418, 8, 91, 93syl3anc 1371 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ 𝑍) β†’ Β¬ (1rβ€˜π‘…) ∈ 𝑗)
9594nrexdv 3149 . . . . . 6 (πœ‘ β†’ Β¬ βˆƒπ‘— ∈ 𝑍 (1rβ€˜π‘…) ∈ 𝑗)
96 eluni2 4912 . . . . . 6 ((1rβ€˜π‘…) ∈ βˆͺ 𝑍 ↔ βˆƒπ‘— ∈ 𝑍 (1rβ€˜π‘…) ∈ 𝑗)
9795, 96sylnibr 328 . . . . 5 (πœ‘ β†’ Β¬ (1rβ€˜π‘…) ∈ βˆͺ 𝑍)
9810, 9, 92lidl1el 20840 . . . . . . 7 ((𝑅 ∈ Ring ∧ βˆͺ 𝑍 ∈ (LIdealβ€˜π‘…)) β†’ ((1rβ€˜π‘…) ∈ βˆͺ 𝑍 ↔ βˆͺ 𝑍 = 𝐡))
9917, 84, 98syl2anc 584 . . . . . 6 (πœ‘ β†’ ((1rβ€˜π‘…) ∈ βˆͺ 𝑍 ↔ βˆͺ 𝑍 = 𝐡))
10099necon3bbid 2978 . . . . 5 (πœ‘ β†’ (Β¬ (1rβ€˜π‘…) ∈ βˆͺ 𝑍 ↔ βˆͺ 𝑍 β‰  𝐡))
10197, 100mpbid 231 . . . 4 (πœ‘ β†’ βˆͺ 𝑍 β‰  𝐡)
10290simprrd 772 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ 𝑍) β†’ 𝐼 βŠ† 𝑗)
103102ralrimiva 3146 . . . . . 6 (πœ‘ β†’ βˆ€π‘— ∈ 𝑍 𝐼 βŠ† 𝑗)
104 ssint 4968 . . . . . 6 (𝐼 βŠ† ∩ 𝑍 ↔ βˆ€π‘— ∈ 𝑍 𝐼 βŠ† 𝑗)
105103, 104sylibr 233 . . . . 5 (πœ‘ β†’ 𝐼 βŠ† ∩ 𝑍)
106 intssuni 4974 . . . . . 6 (𝑍 β‰  βˆ… β†’ ∩ 𝑍 βŠ† βˆͺ 𝑍)
10716, 106syl 17 . . . . 5 (πœ‘ β†’ ∩ 𝑍 βŠ† βˆͺ 𝑍)
108105, 107sstrd 3992 . . . 4 (πœ‘ β†’ 𝐼 βŠ† βˆͺ 𝑍)
109101, 108jca 512 . . 3 (πœ‘ β†’ (βˆͺ 𝑍 β‰  𝐡 ∧ 𝐼 βŠ† βˆͺ 𝑍))
1103, 84, 109elrabd 3685 . 2 (πœ‘ β†’ βˆͺ 𝑍 ∈ {𝑝 ∈ (LIdealβ€˜π‘…) ∣ (𝑝 β‰  𝐡 ∧ 𝐼 βŠ† 𝑝)})
111110, 5eleqtrrdi 2844 1 (πœ‘ β†’ βˆͺ 𝑍 ∈ 𝑃)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  {crab 3432   βŠ† wss 3948  βˆ…c0 4322  βˆͺ cuni 4908  βˆ© cint 4950   Or wor 5587  β€˜cfv 6543  (class class class)co 7408   [⊊] crpss 7711  Basecbs 17143  +gcplusg 17196  .rcmulr 17197  0gc0g 17384  1rcur 20003  Ringcrg 20055  LIdealclidl 20782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-rpss 7712  df-om 7855  df-1st 7974  df-2nd 7975  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-er 8702  df-en 8939  df-dom 8940  df-sdom 8941  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-nn 12212  df-2 12274  df-3 12275  df-4 12276  df-5 12277  df-6 12278  df-7 12279  df-8 12280  df-sets 17096  df-slot 17114  df-ndx 17126  df-base 17144  df-ress 17173  df-plusg 17209  df-mulr 17210  df-sca 17212  df-vsca 17213  df-ip 17214  df-0g 17386  df-mgm 18560  df-sgrp 18609  df-mnd 18625  df-grp 18821  df-minusg 18822  df-sbg 18823  df-subg 19002  df-mgp 19987  df-ur 20004  df-ring 20057  df-subrg 20316  df-lmod 20472  df-lss 20542  df-sra 20784  df-rgmod 20785  df-lidl 20786
This theorem is referenced by:  ssmxidl  32585
  Copyright terms: Public domain W3C validator