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 33480
Description: The set 𝑃 used in the proof of ssmxidl 33481 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 3000 . . . 4 (𝑝 = 𝑍 → (𝑝𝐵 𝑍𝐵))
2 sseq2 4021 . . . 4 (𝑝 = 𝑍 → (𝐼𝑝𝐼 𝑍))
31, 2anbi12d 632 . . 3 (𝑝 = 𝑍 → ((𝑝𝐵𝐼𝑝) ↔ ( 𝑍𝐵𝐼 𝑍)))
4 ssmxidllem2.1 . . . . . . . . 9 (𝜑𝑍𝑃)
5 ssmxidllem.1 . . . . . . . . . 10 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ (𝑝𝐵𝐼𝑝)}
65ssrab3 4091 . . . . . . . . 9 𝑃 ⊆ (LIdeal‘𝑅)
74, 6sstrdi 4007 . . . . . . . 8 (𝜑𝑍 ⊆ (LIdeal‘𝑅))
87sselda 3994 . . . . . . 7 ((𝜑𝑗𝑍) → 𝑗 ∈ (LIdeal‘𝑅))
9 ssmxidl.1 . . . . . . . 8 𝐵 = (Base‘𝑅)
10 eqid 2734 . . . . . . . 8 (LIdeal‘𝑅) = (LIdeal‘𝑅)
119, 10lidlss 21239 . . . . . . 7 (𝑗 ∈ (LIdeal‘𝑅) → 𝑗𝐵)
128, 11syl 17 . . . . . 6 ((𝜑𝑗𝑍) → 𝑗𝐵)
1312ralrimiva 3143 . . . . 5 (𝜑 → ∀𝑗𝑍 𝑗𝐵)
14 unissb 4943 . . . . 5 ( 𝑍𝐵 ↔ ∀𝑗𝑍 𝑗𝐵)
1513, 14sylibr 234 . . . 4 (𝜑 𝑍𝐵)
16 ssmxidllem2.2 . . . . . . 7 (𝜑𝑍 ≠ ∅)
17 ssmxidllem.2 . . . . . . . . . . 11 (𝜑𝑅 ∈ Ring)
1817adantr 480 . . . . . . . . . 10 ((𝜑𝑗𝑍) → 𝑅 ∈ Ring)
19 eqid 2734 . . . . . . . . . . 11 (0g𝑅) = (0g𝑅)
2010, 19lidl0cl 21247 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅)) → (0g𝑅) ∈ 𝑗)
2118, 8, 20syl2anc 584 . . . . . . . . 9 ((𝜑𝑗𝑍) → (0g𝑅) ∈ 𝑗)
22 n0i 4345 . . . . . . . . 9 ((0g𝑅) ∈ 𝑗 → ¬ 𝑗 = ∅)
2321, 22syl 17 . . . . . . . 8 ((𝜑𝑗𝑍) → ¬ 𝑗 = ∅)
2423reximdva0 4360 . . . . . . 7 ((𝜑𝑍 ≠ ∅) → ∃𝑗𝑍 ¬ 𝑗 = ∅)
2516, 24mpdan 687 . . . . . 6 (𝜑 → ∃𝑗𝑍 ¬ 𝑗 = ∅)
26 rexnal 3097 . . . . . 6 (∃𝑗𝑍 ¬ 𝑗 = ∅ ↔ ¬ ∀𝑗𝑍 𝑗 = ∅)
2725, 26sylib 218 . . . . 5 (𝜑 → ¬ ∀𝑗𝑍 𝑗 = ∅)
28 uni0c 4938 . . . . . 6 ( 𝑍 = ∅ ↔ ∀𝑗𝑍 𝑗 = ∅)
2928necon3abii 2984 . . . . 5 ( 𝑍 ≠ ∅ ↔ ¬ ∀𝑗𝑍 𝑗 = ∅)
3027, 29sylibr 234 . . . 4 (𝜑 𝑍 ≠ ∅)
31 eluni2 4915 . . . . . . . 8 (𝑎 𝑍 ↔ ∃𝑖𝑍 𝑎𝑖)
32 eluni2 4915 . . . . . . . 8 (𝑏 𝑍 ↔ ∃𝑗𝑍 𝑏𝑗)
3331, 32anbi12i 628 . . . . . . 7 ((𝑎 𝑍𝑏 𝑍) ↔ (∃𝑖𝑍 𝑎𝑖 ∧ ∃𝑗𝑍 𝑏𝑗))
34 an32 646 . . . . . . . . . 10 ((((𝜑𝑥𝐵) ∧ ∃𝑖𝑍 𝑎𝑖) ∧ 𝑗𝑍) ↔ (((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ ∃𝑖𝑍 𝑎𝑖))
3517ad6antr 736 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑅 ∈ Ring)
367ad5antr 734 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → 𝑍 ⊆ (LIdeal‘𝑅))
37 simp-4r 784 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → 𝑗𝑍)
3836, 37sseldd 3995 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → 𝑗 ∈ (LIdeal‘𝑅))
3938adantr 480 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑗 ∈ (LIdeal‘𝑅))
40 simp-6r 788 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑥𝐵)
41 simpr 484 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑖𝑗)
42 simplr 769 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑎𝑖)
4341, 42sseldd 3995 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑎𝑗)
44 eqid 2734 . . . . . . . . . . . . . . . . 17 (.r𝑅) = (.r𝑅)
4510, 9, 44lidlmcl 21252 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅)) ∧ (𝑥𝐵𝑎𝑗)) → (𝑥(.r𝑅)𝑎) ∈ 𝑗)
4635, 39, 40, 43, 45syl22anc 839 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → (𝑥(.r𝑅)𝑎) ∈ 𝑗)
47 simp-4r 784 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑏𝑗)
48 eqid 2734 . . . . . . . . . . . . . . . 16 (+g𝑅) = (+g𝑅)
4910, 48lidlacl 21248 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅)) ∧ ((𝑥(.r𝑅)𝑎) ∈ 𝑗𝑏𝑗)) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑗)
5035, 39, 46, 47, 49syl22anc 839 . . . . . . . . . . . . . 14 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑗)
5137adantr 480 . . . . . . . . . . . . . 14 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑗𝑍)
52 elunii 4916 . . . . . . . . . . . . . 14 ((((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑗𝑗𝑍) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
5350, 51, 52syl2anc 584 . . . . . . . . . . . . 13 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
5417ad6antr 736 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑅 ∈ Ring)
5536adantr 480 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑍 ⊆ (LIdeal‘𝑅))
56 simplr 769 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → 𝑖𝑍)
5756adantr 480 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑖𝑍)
5855, 57sseldd 3995 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑖 ∈ (LIdeal‘𝑅))
59 simp-6r 788 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑥𝐵)
60 simplr 769 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑎𝑖)
6110, 9, 44lidlmcl 21252 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ (𝑥𝐵𝑎𝑖)) → (𝑥(.r𝑅)𝑎) ∈ 𝑖)
6254, 58, 59, 60, 61syl22anc 839 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → (𝑥(.r𝑅)𝑎) ∈ 𝑖)
63 simpr 484 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑗𝑖)
64 simp-4r 784 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑏𝑗)
6563, 64sseldd 3995 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑏𝑖)
6610, 48lidlacl 21248 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑥(.r𝑅)𝑎) ∈ 𝑖𝑏𝑖)) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑖)
6754, 58, 62, 65, 66syl22anc 839 . . . . . . . . . . . . . 14 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑖)
68 elunii 4916 . . . . . . . . . . . . . 14 ((((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑖𝑖𝑍) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
6967, 57, 68syl2anc 584 . . . . . . . . . . . . 13 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
70 ssmxidllem2.3 . . . . . . . . . . . . . . 15 (𝜑 → [] Or 𝑍)
7170ad5antr 734 . . . . . . . . . . . . . 14 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → [] Or 𝑍)
72 sorpssi 7747 . . . . . . . . . . . . . 14 (( [] Or 𝑍 ∧ (𝑖𝑍𝑗𝑍)) → (𝑖𝑗𝑗𝑖))
7371, 56, 37, 72syl12anc 837 . . . . . . . . . . . . 13 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → (𝑖𝑗𝑗𝑖))
7453, 69, 73mpjaodan 960 . . . . . . . . . . . 12 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7574r19.29an 3155 . . . . . . . . . . 11 (((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ ∃𝑖𝑍 𝑎𝑖) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7675an32s 652 . . . . . . . . . 10 (((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ ∃𝑖𝑍 𝑎𝑖) ∧ 𝑏𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7734, 76sylanb 581 . . . . . . . . 9 (((((𝜑𝑥𝐵) ∧ ∃𝑖𝑍 𝑎𝑖) ∧ 𝑗𝑍) ∧ 𝑏𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7877r19.29an 3155 . . . . . . . 8 ((((𝜑𝑥𝐵) ∧ ∃𝑖𝑍 𝑎𝑖) ∧ ∃𝑗𝑍 𝑏𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7978anasss 466 . . . . . . 7 (((𝜑𝑥𝐵) ∧ (∃𝑖𝑍 𝑎𝑖 ∧ ∃𝑗𝑍 𝑏𝑗)) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
8033, 79sylan2b 594 . . . . . 6 (((𝜑𝑥𝐵) ∧ (𝑎 𝑍𝑏 𝑍)) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
8180ralrimivva 3199 . . . . 5 ((𝜑𝑥𝐵) → ∀𝑎 𝑍𝑏 𝑍((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
8281ralrimiva 3143 . . . 4 (𝜑 → ∀𝑥𝐵𝑎 𝑍𝑏 𝑍((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
8310, 9, 48, 44islidl 21242 . . . 4 ( 𝑍 ∈ (LIdeal‘𝑅) ↔ ( 𝑍𝐵 𝑍 ≠ ∅ ∧ ∀𝑥𝐵𝑎 𝑍𝑏 𝑍((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍))
8415, 30, 82, 83syl3anbrc 1342 . . 3 (𝜑 𝑍 ∈ (LIdeal‘𝑅))
854sselda 3994 . . . . . . . . . 10 ((𝜑𝑗𝑍) → 𝑗𝑃)
86 neeq1 3000 . . . . . . . . . . . 12 (𝑝 = 𝑗 → (𝑝𝐵𝑗𝐵))
87 sseq2 4021 . . . . . . . . . . . 12 (𝑝 = 𝑗 → (𝐼𝑝𝐼𝑗))
8886, 87anbi12d 632 . . . . . . . . . . 11 (𝑝 = 𝑗 → ((𝑝𝐵𝐼𝑝) ↔ (𝑗𝐵𝐼𝑗)))
8988, 5elrab2 3697 . . . . . . . . . 10 (𝑗𝑃 ↔ (𝑗 ∈ (LIdeal‘𝑅) ∧ (𝑗𝐵𝐼𝑗)))
9085, 89sylib 218 . . . . . . . . 9 ((𝜑𝑗𝑍) → (𝑗 ∈ (LIdeal‘𝑅) ∧ (𝑗𝐵𝐼𝑗)))
9190simprld 772 . . . . . . . 8 ((𝜑𝑗𝑍) → 𝑗𝐵)
92 eqid 2734 . . . . . . . . 9 (1r𝑅) = (1r𝑅)
939, 92pridln1 33450 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅) ∧ 𝑗𝐵) → ¬ (1r𝑅) ∈ 𝑗)
9418, 8, 91, 93syl3anc 1370 . . . . . . 7 ((𝜑𝑗𝑍) → ¬ (1r𝑅) ∈ 𝑗)
9594nrexdv 3146 . . . . . 6 (𝜑 → ¬ ∃𝑗𝑍 (1r𝑅) ∈ 𝑗)
96 eluni2 4915 . . . . . 6 ((1r𝑅) ∈ 𝑍 ↔ ∃𝑗𝑍 (1r𝑅) ∈ 𝑗)
9795, 96sylnibr 329 . . . . 5 (𝜑 → ¬ (1r𝑅) ∈ 𝑍)
9810, 9, 92lidl1el 21253 . . . . . . 7 ((𝑅 ∈ Ring ∧ 𝑍 ∈ (LIdeal‘𝑅)) → ((1r𝑅) ∈ 𝑍 𝑍 = 𝐵))
9917, 84, 98syl2anc 584 . . . . . 6 (𝜑 → ((1r𝑅) ∈ 𝑍 𝑍 = 𝐵))
10099necon3bbid 2975 . . . . 5 (𝜑 → (¬ (1r𝑅) ∈ 𝑍 𝑍𝐵))
10197, 100mpbid 232 . . . 4 (𝜑 𝑍𝐵)
10290simprrd 774 . . . . . . 7 ((𝜑𝑗𝑍) → 𝐼𝑗)
103102ralrimiva 3143 . . . . . 6 (𝜑 → ∀𝑗𝑍 𝐼𝑗)
104 ssint 4968 . . . . . 6 (𝐼 𝑍 ↔ ∀𝑗𝑍 𝐼𝑗)
105103, 104sylibr 234 . . . . 5 (𝜑𝐼 𝑍)
106 intssuni 4974 . . . . . 6 (𝑍 ≠ ∅ → 𝑍 𝑍)
10716, 106syl 17 . . . . 5 (𝜑 𝑍 𝑍)
108105, 107sstrd 4005 . . . 4 (𝜑𝐼 𝑍)
109101, 108jca 511 . . 3 (𝜑 → ( 𝑍𝐵𝐼 𝑍))
1103, 84, 109elrabd 3696 . 2 (𝜑 𝑍 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ (𝑝𝐵𝐼𝑝)})
111110, 5eleqtrrdi 2849 1 (𝜑 𝑍𝑃)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847   = wceq 1536  wcel 2105  wne 2937  wral 3058  wrex 3067  {crab 3432  wss 3962  c0 4338   cuni 4911   cint 4950   Or wor 5595  cfv 6562  (class class class)co 7430   [] crpss 7740  Basecbs 17244  +gcplusg 17297  .rcmulr 17298  0gc0g 17485  1rcur 20198  Ringcrg 20250  LIdealclidl 21233
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-rpss 7741  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-mulr 17311  df-sca 17313  df-vsca 17314  df-ip 17315  df-0g 17487  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-grp 18966  df-minusg 18967  df-sbg 18968  df-subg 19153  df-cmn 19814  df-abl 19815  df-mgp 20152  df-rng 20170  df-ur 20199  df-ring 20252  df-subrg 20586  df-lmod 20876  df-lss 20947  df-sra 21189  df-rgmod 21190  df-lidl 21235
This theorem is referenced by:  ssmxidl  33481
  Copyright terms: Public domain W3C validator