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 33466
Description: The set 𝑃 used in the proof of ssmxidl 33467 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 3009 . . . 4 (𝑝 = 𝑍 → (𝑝𝐵 𝑍𝐵))
2 sseq2 4035 . . . 4 (𝑝 = 𝑍 → (𝐼𝑝𝐼 𝑍))
31, 2anbi12d 631 . . 3 (𝑝 = 𝑍 → ((𝑝𝐵𝐼𝑝) ↔ ( 𝑍𝐵𝐼 𝑍)))
4 ssmxidllem2.1 . . . . . . . . 9 (𝜑𝑍𝑃)
5 ssmxidllem.1 . . . . . . . . . 10 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ (𝑝𝐵𝐼𝑝)}
65ssrab3 4105 . . . . . . . . 9 𝑃 ⊆ (LIdeal‘𝑅)
74, 6sstrdi 4021 . . . . . . . 8 (𝜑𝑍 ⊆ (LIdeal‘𝑅))
87sselda 4008 . . . . . . 7 ((𝜑𝑗𝑍) → 𝑗 ∈ (LIdeal‘𝑅))
9 ssmxidl.1 . . . . . . . 8 𝐵 = (Base‘𝑅)
10 eqid 2740 . . . . . . . 8 (LIdeal‘𝑅) = (LIdeal‘𝑅)
119, 10lidlss 21245 . . . . . . 7 (𝑗 ∈ (LIdeal‘𝑅) → 𝑗𝐵)
128, 11syl 17 . . . . . 6 ((𝜑𝑗𝑍) → 𝑗𝐵)
1312ralrimiva 3152 . . . . 5 (𝜑 → ∀𝑗𝑍 𝑗𝐵)
14 unissb 4963 . . . . 5 ( 𝑍𝐵 ↔ ∀𝑗𝑍 𝑗𝐵)
1513, 14sylibr 234 . . . 4 (𝜑 𝑍𝐵)
16 ssmxidllem2.2 . . . . . . 7 (𝜑𝑍 ≠ ∅)
17 ssmxidllem.2 . . . . . . . . . . 11 (𝜑𝑅 ∈ Ring)
1817adantr 480 . . . . . . . . . 10 ((𝜑𝑗𝑍) → 𝑅 ∈ Ring)
19 eqid 2740 . . . . . . . . . . 11 (0g𝑅) = (0g𝑅)
2010, 19lidl0cl 21253 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅)) → (0g𝑅) ∈ 𝑗)
2118, 8, 20syl2anc 583 . . . . . . . . 9 ((𝜑𝑗𝑍) → (0g𝑅) ∈ 𝑗)
22 n0i 4363 . . . . . . . . 9 ((0g𝑅) ∈ 𝑗 → ¬ 𝑗 = ∅)
2321, 22syl 17 . . . . . . . 8 ((𝜑𝑗𝑍) → ¬ 𝑗 = ∅)
2423reximdva0 4378 . . . . . . 7 ((𝜑𝑍 ≠ ∅) → ∃𝑗𝑍 ¬ 𝑗 = ∅)
2516, 24mpdan 686 . . . . . 6 (𝜑 → ∃𝑗𝑍 ¬ 𝑗 = ∅)
26 rexnal 3106 . . . . . 6 (∃𝑗𝑍 ¬ 𝑗 = ∅ ↔ ¬ ∀𝑗𝑍 𝑗 = ∅)
2725, 26sylib 218 . . . . 5 (𝜑 → ¬ ∀𝑗𝑍 𝑗 = ∅)
28 uni0c 4958 . . . . . 6 ( 𝑍 = ∅ ↔ ∀𝑗𝑍 𝑗 = ∅)
2928necon3abii 2993 . . . . 5 ( 𝑍 ≠ ∅ ↔ ¬ ∀𝑗𝑍 𝑗 = ∅)
3027, 29sylibr 234 . . . 4 (𝜑 𝑍 ≠ ∅)
31 eluni2 4935 . . . . . . . 8 (𝑎 𝑍 ↔ ∃𝑖𝑍 𝑎𝑖)
32 eluni2 4935 . . . . . . . 8 (𝑏 𝑍 ↔ ∃𝑗𝑍 𝑏𝑗)
3331, 32anbi12i 627 . . . . . . 7 ((𝑎 𝑍𝑏 𝑍) ↔ (∃𝑖𝑍 𝑎𝑖 ∧ ∃𝑗𝑍 𝑏𝑗))
34 an32 645 . . . . . . . . . 10 ((((𝜑𝑥𝐵) ∧ ∃𝑖𝑍 𝑎𝑖) ∧ 𝑗𝑍) ↔ (((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ ∃𝑖𝑍 𝑎𝑖))
3517ad6antr 735 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑅 ∈ Ring)
367ad5antr 733 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → 𝑍 ⊆ (LIdeal‘𝑅))
37 simp-4r 783 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → 𝑗𝑍)
3836, 37sseldd 4009 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → 𝑗 ∈ (LIdeal‘𝑅))
3938adantr 480 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑗 ∈ (LIdeal‘𝑅))
40 simp-6r 787 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑥𝐵)
41 simpr 484 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑖𝑗)
42 simplr 768 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑎𝑖)
4341, 42sseldd 4009 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑎𝑗)
44 eqid 2740 . . . . . . . . . . . . . . . . 17 (.r𝑅) = (.r𝑅)
4510, 9, 44lidlmcl 21258 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅)) ∧ (𝑥𝐵𝑎𝑗)) → (𝑥(.r𝑅)𝑎) ∈ 𝑗)
4635, 39, 40, 43, 45syl22anc 838 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → (𝑥(.r𝑅)𝑎) ∈ 𝑗)
47 simp-4r 783 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑏𝑗)
48 eqid 2740 . . . . . . . . . . . . . . . 16 (+g𝑅) = (+g𝑅)
4910, 48lidlacl 21254 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅)) ∧ ((𝑥(.r𝑅)𝑎) ∈ 𝑗𝑏𝑗)) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑗)
5035, 39, 46, 47, 49syl22anc 838 . . . . . . . . . . . . . 14 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑗)
5137adantr 480 . . . . . . . . . . . . . 14 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑗𝑍)
52 elunii 4936 . . . . . . . . . . . . . 14 ((((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑗𝑗𝑍) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
5350, 51, 52syl2anc 583 . . . . . . . . . . . . 13 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
5417ad6antr 735 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑅 ∈ Ring)
5536adantr 480 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑍 ⊆ (LIdeal‘𝑅))
56 simplr 768 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → 𝑖𝑍)
5756adantr 480 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑖𝑍)
5855, 57sseldd 4009 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑖 ∈ (LIdeal‘𝑅))
59 simp-6r 787 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑥𝐵)
60 simplr 768 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑎𝑖)
6110, 9, 44lidlmcl 21258 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ (𝑥𝐵𝑎𝑖)) → (𝑥(.r𝑅)𝑎) ∈ 𝑖)
6254, 58, 59, 60, 61syl22anc 838 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → (𝑥(.r𝑅)𝑎) ∈ 𝑖)
63 simpr 484 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑗𝑖)
64 simp-4r 783 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑏𝑗)
6563, 64sseldd 4009 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑏𝑖)
6610, 48lidlacl 21254 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑥(.r𝑅)𝑎) ∈ 𝑖𝑏𝑖)) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑖)
6754, 58, 62, 65, 66syl22anc 838 . . . . . . . . . . . . . 14 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑖)
68 elunii 4936 . . . . . . . . . . . . . 14 ((((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑖𝑖𝑍) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
6967, 57, 68syl2anc 583 . . . . . . . . . . . . 13 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
70 ssmxidllem2.3 . . . . . . . . . . . . . . 15 (𝜑 → [] Or 𝑍)
7170ad5antr 733 . . . . . . . . . . . . . 14 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → [] Or 𝑍)
72 sorpssi 7764 . . . . . . . . . . . . . 14 (( [] Or 𝑍 ∧ (𝑖𝑍𝑗𝑍)) → (𝑖𝑗𝑗𝑖))
7371, 56, 37, 72syl12anc 836 . . . . . . . . . . . . 13 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → (𝑖𝑗𝑗𝑖))
7453, 69, 73mpjaodan 959 . . . . . . . . . . . 12 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7574r19.29an 3164 . . . . . . . . . . 11 (((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ ∃𝑖𝑍 𝑎𝑖) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7675an32s 651 . . . . . . . . . 10 (((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ ∃𝑖𝑍 𝑎𝑖) ∧ 𝑏𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7734, 76sylanb 580 . . . . . . . . 9 (((((𝜑𝑥𝐵) ∧ ∃𝑖𝑍 𝑎𝑖) ∧ 𝑗𝑍) ∧ 𝑏𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7877r19.29an 3164 . . . . . . . 8 ((((𝜑𝑥𝐵) ∧ ∃𝑖𝑍 𝑎𝑖) ∧ ∃𝑗𝑍 𝑏𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7978anasss 466 . . . . . . 7 (((𝜑𝑥𝐵) ∧ (∃𝑖𝑍 𝑎𝑖 ∧ ∃𝑗𝑍 𝑏𝑗)) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
8033, 79sylan2b 593 . . . . . 6 (((𝜑𝑥𝐵) ∧ (𝑎 𝑍𝑏 𝑍)) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
8180ralrimivva 3208 . . . . 5 ((𝜑𝑥𝐵) → ∀𝑎 𝑍𝑏 𝑍((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
8281ralrimiva 3152 . . . 4 (𝜑 → ∀𝑥𝐵𝑎 𝑍𝑏 𝑍((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
8310, 9, 48, 44islidl 21248 . . . 4 ( 𝑍 ∈ (LIdeal‘𝑅) ↔ ( 𝑍𝐵 𝑍 ≠ ∅ ∧ ∀𝑥𝐵𝑎 𝑍𝑏 𝑍((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍))
8415, 30, 82, 83syl3anbrc 1343 . . 3 (𝜑 𝑍 ∈ (LIdeal‘𝑅))
854sselda 4008 . . . . . . . . . 10 ((𝜑𝑗𝑍) → 𝑗𝑃)
86 neeq1 3009 . . . . . . . . . . . 12 (𝑝 = 𝑗 → (𝑝𝐵𝑗𝐵))
87 sseq2 4035 . . . . . . . . . . . 12 (𝑝 = 𝑗 → (𝐼𝑝𝐼𝑗))
8886, 87anbi12d 631 . . . . . . . . . . 11 (𝑝 = 𝑗 → ((𝑝𝐵𝐼𝑝) ↔ (𝑗𝐵𝐼𝑗)))
8988, 5elrab2 3711 . . . . . . . . . 10 (𝑗𝑃 ↔ (𝑗 ∈ (LIdeal‘𝑅) ∧ (𝑗𝐵𝐼𝑗)))
9085, 89sylib 218 . . . . . . . . 9 ((𝜑𝑗𝑍) → (𝑗 ∈ (LIdeal‘𝑅) ∧ (𝑗𝐵𝐼𝑗)))
9190simprld 771 . . . . . . . 8 ((𝜑𝑗𝑍) → 𝑗𝐵)
92 eqid 2740 . . . . . . . . 9 (1r𝑅) = (1r𝑅)
939, 92pridln1 33436 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅) ∧ 𝑗𝐵) → ¬ (1r𝑅) ∈ 𝑗)
9418, 8, 91, 93syl3anc 1371 . . . . . . 7 ((𝜑𝑗𝑍) → ¬ (1r𝑅) ∈ 𝑗)
9594nrexdv 3155 . . . . . 6 (𝜑 → ¬ ∃𝑗𝑍 (1r𝑅) ∈ 𝑗)
96 eluni2 4935 . . . . . 6 ((1r𝑅) ∈ 𝑍 ↔ ∃𝑗𝑍 (1r𝑅) ∈ 𝑗)
9795, 96sylnibr 329 . . . . 5 (𝜑 → ¬ (1r𝑅) ∈ 𝑍)
9810, 9, 92lidl1el 21259 . . . . . . 7 ((𝑅 ∈ Ring ∧ 𝑍 ∈ (LIdeal‘𝑅)) → ((1r𝑅) ∈ 𝑍 𝑍 = 𝐵))
9917, 84, 98syl2anc 583 . . . . . 6 (𝜑 → ((1r𝑅) ∈ 𝑍 𝑍 = 𝐵))
10099necon3bbid 2984 . . . . 5 (𝜑 → (¬ (1r𝑅) ∈ 𝑍 𝑍𝐵))
10197, 100mpbid 232 . . . 4 (𝜑 𝑍𝐵)
10290simprrd 773 . . . . . . 7 ((𝜑𝑗𝑍) → 𝐼𝑗)
103102ralrimiva 3152 . . . . . 6 (𝜑 → ∀𝑗𝑍 𝐼𝑗)
104 ssint 4988 . . . . . 6 (𝐼 𝑍 ↔ ∀𝑗𝑍 𝐼𝑗)
105103, 104sylibr 234 . . . . 5 (𝜑𝐼 𝑍)
106 intssuni 4994 . . . . . 6 (𝑍 ≠ ∅ → 𝑍 𝑍)
10716, 106syl 17 . . . . 5 (𝜑 𝑍 𝑍)
108105, 107sstrd 4019 . . . 4 (𝜑𝐼 𝑍)
109101, 108jca 511 . . 3 (𝜑 → ( 𝑍𝐵𝐼 𝑍))
1103, 84, 109elrabd 3710 . 2 (𝜑 𝑍 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ (𝑝𝐵𝐼𝑝)})
111110, 5eleqtrrdi 2855 1 (𝜑 𝑍𝑃)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 846   = wceq 1537  wcel 2108  wne 2946  wral 3067  wrex 3076  {crab 3443  wss 3976  c0 4352   cuni 4931   cint 4970   Or wor 5606  cfv 6573  (class class class)co 7448   [] crpss 7757  Basecbs 17258  +gcplusg 17311  .rcmulr 17312  0gc0g 17499  1rcur 20208  Ringcrg 20260  LIdealclidl 21239
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-rpss 7758  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-nn 12294  df-2 12356  df-3 12357  df-4 12358  df-5 12359  df-6 12360  df-7 12361  df-8 12362  df-sets 17211  df-slot 17229  df-ndx 17241  df-base 17259  df-ress 17288  df-plusg 17324  df-mulr 17325  df-sca 17327  df-vsca 17328  df-ip 17329  df-0g 17501  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-grp 18976  df-minusg 18977  df-sbg 18978  df-subg 19163  df-cmn 19824  df-abl 19825  df-mgp 20162  df-rng 20180  df-ur 20209  df-ring 20262  df-subrg 20597  df-lmod 20882  df-lss 20953  df-sra 21195  df-rgmod 21196  df-lidl 21241
This theorem is referenced by:  ssmxidl  33467
  Copyright terms: Public domain W3C validator