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 31176
Description: The set 𝑃 used in the proof of ssmxidl 31177 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 3014 . . . 4 (𝑝 = 𝑍 → (𝑝𝐵 𝑍𝐵))
2 sseq2 3921 . . . 4 (𝑝 = 𝑍 → (𝐼𝑝𝐼 𝑍))
31, 2anbi12d 633 . . 3 (𝑝 = 𝑍 → ((𝑝𝐵𝐼𝑝) ↔ ( 𝑍𝐵𝐼 𝑍)))
4 ssmxidllem2.1 . . . . . . . . 9 (𝜑𝑍𝑃)
5 ssmxidllem.1 . . . . . . . . . 10 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ (𝑝𝐵𝐼𝑝)}
65ssrab3 3989 . . . . . . . . 9 𝑃 ⊆ (LIdeal‘𝑅)
74, 6sstrdi 3907 . . . . . . . 8 (𝜑𝑍 ⊆ (LIdeal‘𝑅))
87sselda 3895 . . . . . . 7 ((𝜑𝑗𝑍) → 𝑗 ∈ (LIdeal‘𝑅))
9 ssmxidl.1 . . . . . . . 8 𝐵 = (Base‘𝑅)
10 eqid 2759 . . . . . . . 8 (LIdeal‘𝑅) = (LIdeal‘𝑅)
119, 10lidlss 20066 . . . . . . 7 (𝑗 ∈ (LIdeal‘𝑅) → 𝑗𝐵)
128, 11syl 17 . . . . . 6 ((𝜑𝑗𝑍) → 𝑗𝐵)
1312ralrimiva 3114 . . . . 5 (𝜑 → ∀𝑗𝑍 𝑗𝐵)
14 unissb 4836 . . . . 5 ( 𝑍𝐵 ↔ ∀𝑗𝑍 𝑗𝐵)
1513, 14sylibr 237 . . . 4 (𝜑 𝑍𝐵)
16 ssmxidllem2.2 . . . . . . 7 (𝜑𝑍 ≠ ∅)
17 ssmxidllem.2 . . . . . . . . . . 11 (𝜑𝑅 ∈ Ring)
1817adantr 484 . . . . . . . . . 10 ((𝜑𝑗𝑍) → 𝑅 ∈ Ring)
19 eqid 2759 . . . . . . . . . . 11 (0g𝑅) = (0g𝑅)
2010, 19lidl0cl 20068 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅)) → (0g𝑅) ∈ 𝑗)
2118, 8, 20syl2anc 587 . . . . . . . . 9 ((𝜑𝑗𝑍) → (0g𝑅) ∈ 𝑗)
22 n0i 4235 . . . . . . . . 9 ((0g𝑅) ∈ 𝑗 → ¬ 𝑗 = ∅)
2321, 22syl 17 . . . . . . . 8 ((𝜑𝑗𝑍) → ¬ 𝑗 = ∅)
2423reximdva0 4253 . . . . . . 7 ((𝜑𝑍 ≠ ∅) → ∃𝑗𝑍 ¬ 𝑗 = ∅)
2516, 24mpdan 686 . . . . . 6 (𝜑 → ∃𝑗𝑍 ¬ 𝑗 = ∅)
26 rexnal 3166 . . . . . 6 (∃𝑗𝑍 ¬ 𝑗 = ∅ ↔ ¬ ∀𝑗𝑍 𝑗 = ∅)
2725, 26sylib 221 . . . . 5 (𝜑 → ¬ ∀𝑗𝑍 𝑗 = ∅)
28 uni0c 4831 . . . . . 6 ( 𝑍 = ∅ ↔ ∀𝑗𝑍 𝑗 = ∅)
2928necon3abii 2998 . . . . 5 ( 𝑍 ≠ ∅ ↔ ¬ ∀𝑗𝑍 𝑗 = ∅)
3027, 29sylibr 237 . . . 4 (𝜑 𝑍 ≠ ∅)
31 eluni2 4806 . . . . . . . 8 (𝑎 𝑍 ↔ ∃𝑖𝑍 𝑎𝑖)
32 eluni2 4806 . . . . . . . 8 (𝑏 𝑍 ↔ ∃𝑗𝑍 𝑏𝑗)
3331, 32anbi12i 629 . . . . . . 7 ((𝑎 𝑍𝑏 𝑍) ↔ (∃𝑖𝑍 𝑎𝑖 ∧ ∃𝑗𝑍 𝑏𝑗))
34 an32 645 . . . . . . . . . 10 ((((𝜑𝑥𝐵) ∧ ∃𝑖𝑍 𝑎𝑖) ∧ 𝑗𝑍) ↔ (((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ ∃𝑖𝑍 𝑎𝑖))
3517ad6antr 735 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑅 ∈ Ring)
367ad5antr 733 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → 𝑍 ⊆ (LIdeal‘𝑅))
37 simp-4r 783 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → 𝑗𝑍)
3836, 37sseldd 3896 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → 𝑗 ∈ (LIdeal‘𝑅))
3938adantr 484 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑗 ∈ (LIdeal‘𝑅))
40 simp-6r 787 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑥𝐵)
41 simpr 488 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑖𝑗)
42 simplr 768 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑎𝑖)
4341, 42sseldd 3896 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑎𝑗)
44 eqid 2759 . . . . . . . . . . . . . . . . 17 (.r𝑅) = (.r𝑅)
4510, 9, 44lidlmcl 20073 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅)) ∧ (𝑥𝐵𝑎𝑗)) → (𝑥(.r𝑅)𝑎) ∈ 𝑗)
4635, 39, 40, 43, 45syl22anc 837 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → (𝑥(.r𝑅)𝑎) ∈ 𝑗)
47 simp-4r 783 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑏𝑗)
48 eqid 2759 . . . . . . . . . . . . . . . 16 (+g𝑅) = (+g𝑅)
4910, 48lidlacl 20069 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅)) ∧ ((𝑥(.r𝑅)𝑎) ∈ 𝑗𝑏𝑗)) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑗)
5035, 39, 46, 47, 49syl22anc 837 . . . . . . . . . . . . . 14 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑗)
5137adantr 484 . . . . . . . . . . . . . 14 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑗𝑍)
52 elunii 4807 . . . . . . . . . . . . . 14 ((((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑗𝑗𝑍) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
5350, 51, 52syl2anc 587 . . . . . . . . . . . . 13 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
5417ad6antr 735 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑅 ∈ Ring)
5536adantr 484 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑍 ⊆ (LIdeal‘𝑅))
56 simplr 768 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → 𝑖𝑍)
5756adantr 484 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑖𝑍)
5855, 57sseldd 3896 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑖 ∈ (LIdeal‘𝑅))
59 simp-6r 787 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑥𝐵)
60 simplr 768 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑎𝑖)
6110, 9, 44lidlmcl 20073 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ (𝑥𝐵𝑎𝑖)) → (𝑥(.r𝑅)𝑎) ∈ 𝑖)
6254, 58, 59, 60, 61syl22anc 837 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → (𝑥(.r𝑅)𝑎) ∈ 𝑖)
63 simpr 488 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑗𝑖)
64 simp-4r 783 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑏𝑗)
6563, 64sseldd 3896 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑏𝑖)
6610, 48lidlacl 20069 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑥(.r𝑅)𝑎) ∈ 𝑖𝑏𝑖)) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑖)
6754, 58, 62, 65, 66syl22anc 837 . . . . . . . . . . . . . 14 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑖)
68 elunii 4807 . . . . . . . . . . . . . 14 ((((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑖𝑖𝑍) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
6967, 57, 68syl2anc 587 . . . . . . . . . . . . 13 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
70 ssmxidllem2.3 . . . . . . . . . . . . . . 15 (𝜑 → [] Or 𝑍)
7170ad5antr 733 . . . . . . . . . . . . . 14 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → [] Or 𝑍)
72 sorpssi 7460 . . . . . . . . . . . . . 14 (( [] Or 𝑍 ∧ (𝑖𝑍𝑗𝑍)) → (𝑖𝑗𝑗𝑖))
7371, 56, 37, 72syl12anc 835 . . . . . . . . . . . . 13 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → (𝑖𝑗𝑗𝑖))
7453, 69, 73mpjaodan 956 . . . . . . . . . . . 12 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7574r19.29an 3213 . . . . . . . . . . 11 (((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ ∃𝑖𝑍 𝑎𝑖) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7675an32s 651 . . . . . . . . . 10 (((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ ∃𝑖𝑍 𝑎𝑖) ∧ 𝑏𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7734, 76sylanb 584 . . . . . . . . 9 (((((𝜑𝑥𝐵) ∧ ∃𝑖𝑍 𝑎𝑖) ∧ 𝑗𝑍) ∧ 𝑏𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7877r19.29an 3213 . . . . . . . 8 ((((𝜑𝑥𝐵) ∧ ∃𝑖𝑍 𝑎𝑖) ∧ ∃𝑗𝑍 𝑏𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7978anasss 470 . . . . . . 7 (((𝜑𝑥𝐵) ∧ (∃𝑖𝑍 𝑎𝑖 ∧ ∃𝑗𝑍 𝑏𝑗)) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
8033, 79sylan2b 596 . . . . . 6 (((𝜑𝑥𝐵) ∧ (𝑎 𝑍𝑏 𝑍)) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
8180ralrimivva 3121 . . . . 5 ((𝜑𝑥𝐵) → ∀𝑎 𝑍𝑏 𝑍((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
8281ralrimiva 3114 . . . 4 (𝜑 → ∀𝑥𝐵𝑎 𝑍𝑏 𝑍((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
8310, 9, 48, 44islidl 20067 . . . 4 ( 𝑍 ∈ (LIdeal‘𝑅) ↔ ( 𝑍𝐵 𝑍 ≠ ∅ ∧ ∀𝑥𝐵𝑎 𝑍𝑏 𝑍((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍))
8415, 30, 82, 83syl3anbrc 1341 . . 3 (𝜑 𝑍 ∈ (LIdeal‘𝑅))
854sselda 3895 . . . . . . . . . 10 ((𝜑𝑗𝑍) → 𝑗𝑃)
86 neeq1 3014 . . . . . . . . . . . 12 (𝑝 = 𝑗 → (𝑝𝐵𝑗𝐵))
87 sseq2 3921 . . . . . . . . . . . 12 (𝑝 = 𝑗 → (𝐼𝑝𝐼𝑗))
8886, 87anbi12d 633 . . . . . . . . . . 11 (𝑝 = 𝑗 → ((𝑝𝐵𝐼𝑝) ↔ (𝑗𝐵𝐼𝑗)))
8988, 5elrab2 3608 . . . . . . . . . 10 (𝑗𝑃 ↔ (𝑗 ∈ (LIdeal‘𝑅) ∧ (𝑗𝐵𝐼𝑗)))
9085, 89sylib 221 . . . . . . . . 9 ((𝜑𝑗𝑍) → (𝑗 ∈ (LIdeal‘𝑅) ∧ (𝑗𝐵𝐼𝑗)))
9190simprld 771 . . . . . . . 8 ((𝜑𝑗𝑍) → 𝑗𝐵)
92 eqid 2759 . . . . . . . . 9 (1r𝑅) = (1r𝑅)
939, 92pridln1 31153 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅) ∧ 𝑗𝐵) → ¬ (1r𝑅) ∈ 𝑗)
9418, 8, 91, 93syl3anc 1369 . . . . . . 7 ((𝜑𝑗𝑍) → ¬ (1r𝑅) ∈ 𝑗)
9594nrexdv 3195 . . . . . 6 (𝜑 → ¬ ∃𝑗𝑍 (1r𝑅) ∈ 𝑗)
96 eluni2 4806 . . . . . 6 ((1r𝑅) ∈ 𝑍 ↔ ∃𝑗𝑍 (1r𝑅) ∈ 𝑗)
9795, 96sylnibr 332 . . . . 5 (𝜑 → ¬ (1r𝑅) ∈ 𝑍)
9810, 9, 92lidl1el 20074 . . . . . . 7 ((𝑅 ∈ Ring ∧ 𝑍 ∈ (LIdeal‘𝑅)) → ((1r𝑅) ∈ 𝑍 𝑍 = 𝐵))
9917, 84, 98syl2anc 587 . . . . . 6 (𝜑 → ((1r𝑅) ∈ 𝑍 𝑍 = 𝐵))
10099necon3bbid 2989 . . . . 5 (𝜑 → (¬ (1r𝑅) ∈ 𝑍 𝑍𝐵))
10197, 100mpbid 235 . . . 4 (𝜑 𝑍𝐵)
10290simprrd 773 . . . . . . 7 ((𝜑𝑗𝑍) → 𝐼𝑗)
103102ralrimiva 3114 . . . . . 6 (𝜑 → ∀𝑗𝑍 𝐼𝑗)
104 ssint 4858 . . . . . 6 (𝐼 𝑍 ↔ ∀𝑗𝑍 𝐼𝑗)
105103, 104sylibr 237 . . . . 5 (𝜑𝐼 𝑍)
106 intssuni 4864 . . . . . 6 (𝑍 ≠ ∅ → 𝑍 𝑍)
10716, 106syl 17 . . . . 5 (𝜑 𝑍 𝑍)
108105, 107sstrd 3905 . . . 4 (𝜑𝐼 𝑍)
109101, 108jca 515 . . 3 (𝜑 → ( 𝑍𝐵𝐼 𝑍))
1103, 84, 109elrabd 3607 . 2 (𝜑 𝑍 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ (𝑝𝐵𝐼𝑝)})
111110, 5eleqtrrdi 2864 1 (𝜑 𝑍𝑃)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844   = wceq 1539  wcel 2112  wne 2952  wral 3071  wrex 3072  {crab 3075  wss 3861  c0 4228   cuni 4802   cint 4842   Or wor 5447  cfv 6341  (class class class)co 7157   [] crpss 7453  Basecbs 16556  +gcplusg 16638  .rcmulr 16639  0gc0g 16786  1rcur 19334  Ringcrg 19380  LIdealclidl 20025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5161  ax-sep 5174  ax-nul 5181  ax-pow 5239  ax-pr 5303  ax-un 7466  ax-cnex 10645  ax-resscn 10646  ax-1cn 10647  ax-icn 10648  ax-addcl 10649  ax-addrcl 10650  ax-mulcl 10651  ax-mulrcl 10652  ax-mulcom 10653  ax-addass 10654  ax-mulass 10655  ax-distr 10656  ax-i2m1 10657  ax-1ne0 10658  ax-1rid 10659  ax-rnegex 10660  ax-rrecex 10661  ax-cnre 10662  ax-pre-lttri 10663  ax-pre-lttrn 10664  ax-pre-ltadd 10665  ax-pre-mulgt0 10666
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-pss 3880  df-nul 4229  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4803  df-int 4843  df-iun 4889  df-br 5038  df-opab 5100  df-mpt 5118  df-tr 5144  df-id 5435  df-eprel 5440  df-po 5448  df-so 5449  df-fr 5488  df-we 5490  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-pred 6132  df-ord 6178  df-on 6179  df-lim 6180  df-suc 6181  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-riota 7115  df-ov 7160  df-oprab 7161  df-mpo 7162  df-rpss 7454  df-om 7587  df-1st 7700  df-2nd 7701  df-wrecs 7964  df-recs 8025  df-rdg 8063  df-er 8306  df-en 8542  df-dom 8543  df-sdom 8544  df-pnf 10729  df-mnf 10730  df-xr 10731  df-ltxr 10732  df-le 10733  df-sub 10924  df-neg 10925  df-nn 11689  df-2 11751  df-3 11752  df-4 11753  df-5 11754  df-6 11755  df-7 11756  df-8 11757  df-ndx 16559  df-slot 16560  df-base 16562  df-sets 16563  df-ress 16564  df-plusg 16651  df-mulr 16652  df-sca 16654  df-vsca 16655  df-ip 16656  df-0g 16788  df-mgm 17933  df-sgrp 17982  df-mnd 17993  df-grp 18187  df-minusg 18188  df-sbg 18189  df-subg 18358  df-mgp 19323  df-ur 19335  df-ring 19382  df-subrg 19616  df-lmod 19719  df-lss 19787  df-sra 20027  df-rgmod 20028  df-lidl 20029
This theorem is referenced by:  ssmxidl  31177
  Copyright terms: Public domain W3C validator