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 31002
Description: The set 𝑃 used in the proof of ssmxidl 31003 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 3077 . . . 4 (𝑝 = 𝑍 → (𝑝𝐵 𝑍𝐵))
2 sseq2 3986 . . . 4 (𝑝 = 𝑍 → (𝐼𝑝𝐼 𝑍))
31, 2anbi12d 632 . . 3 (𝑝 = 𝑍 → ((𝑝𝐵𝐼𝑝) ↔ ( 𝑍𝐵𝐼 𝑍)))
4 ssmxidllem2.1 . . . . . . . . 9 (𝜑𝑍𝑃)
5 ssmxidllem.1 . . . . . . . . . 10 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ (𝑝𝐵𝐼𝑝)}
65ssrab3 4050 . . . . . . . . 9 𝑃 ⊆ (LIdeal‘𝑅)
74, 6sstrdi 3972 . . . . . . . 8 (𝜑𝑍 ⊆ (LIdeal‘𝑅))
87sselda 3960 . . . . . . 7 ((𝜑𝑗𝑍) → 𝑗 ∈ (LIdeal‘𝑅))
9 ssmxidl.1 . . . . . . . 8 𝐵 = (Base‘𝑅)
10 eqid 2820 . . . . . . . 8 (LIdeal‘𝑅) = (LIdeal‘𝑅)
119, 10lidlss 19978 . . . . . . 7 (𝑗 ∈ (LIdeal‘𝑅) → 𝑗𝐵)
128, 11syl 17 . . . . . 6 ((𝜑𝑗𝑍) → 𝑗𝐵)
1312ralrimiva 3181 . . . . 5 (𝜑 → ∀𝑗𝑍 𝑗𝐵)
14 unissb 4863 . . . . 5 ( 𝑍𝐵 ↔ ∀𝑗𝑍 𝑗𝐵)
1513, 14sylibr 236 . . . 4 (𝜑 𝑍𝐵)
16 ssmxidllem2.2 . . . . . . 7 (𝜑𝑍 ≠ ∅)
17 ssmxidllem.2 . . . . . . . . . . 11 (𝜑𝑅 ∈ Ring)
1817adantr 483 . . . . . . . . . 10 ((𝜑𝑗𝑍) → 𝑅 ∈ Ring)
19 eqid 2820 . . . . . . . . . . 11 (0g𝑅) = (0g𝑅)
2010, 19lidl0cl 19980 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅)) → (0g𝑅) ∈ 𝑗)
2118, 8, 20syl2anc 586 . . . . . . . . 9 ((𝜑𝑗𝑍) → (0g𝑅) ∈ 𝑗)
22 n0i 4292 . . . . . . . . 9 ((0g𝑅) ∈ 𝑗 → ¬ 𝑗 = ∅)
2321, 22syl 17 . . . . . . . 8 ((𝜑𝑗𝑍) → ¬ 𝑗 = ∅)
2423reximdva0 4305 . . . . . . 7 ((𝜑𝑍 ≠ ∅) → ∃𝑗𝑍 ¬ 𝑗 = ∅)
2516, 24mpdan 685 . . . . . 6 (𝜑 → ∃𝑗𝑍 ¬ 𝑗 = ∅)
26 rexnal 3237 . . . . . 6 (∃𝑗𝑍 ¬ 𝑗 = ∅ ↔ ¬ ∀𝑗𝑍 𝑗 = ∅)
2725, 26sylib 220 . . . . 5 (𝜑 → ¬ ∀𝑗𝑍 𝑗 = ∅)
28 uni0c 4858 . . . . . 6 ( 𝑍 = ∅ ↔ ∀𝑗𝑍 𝑗 = ∅)
2928necon3abii 3061 . . . . 5 ( 𝑍 ≠ ∅ ↔ ¬ ∀𝑗𝑍 𝑗 = ∅)
3027, 29sylibr 236 . . . 4 (𝜑 𝑍 ≠ ∅)
31 eluni2 4835 . . . . . . . 8 (𝑎 𝑍 ↔ ∃𝑖𝑍 𝑎𝑖)
32 eluni2 4835 . . . . . . . 8 (𝑏 𝑍 ↔ ∃𝑗𝑍 𝑏𝑗)
3331, 32anbi12i 628 . . . . . . 7 ((𝑎 𝑍𝑏 𝑍) ↔ (∃𝑖𝑍 𝑎𝑖 ∧ ∃𝑗𝑍 𝑏𝑗))
34 an32 644 . . . . . . . . . 10 ((((𝜑𝑥𝐵) ∧ ∃𝑖𝑍 𝑎𝑖) ∧ 𝑗𝑍) ↔ (((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ ∃𝑖𝑍 𝑎𝑖))
3517ad6antr 734 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑅 ∈ Ring)
367ad5antr 732 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → 𝑍 ⊆ (LIdeal‘𝑅))
37 simp-4r 782 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → 𝑗𝑍)
3836, 37sseldd 3961 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → 𝑗 ∈ (LIdeal‘𝑅))
3938adantr 483 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑗 ∈ (LIdeal‘𝑅))
40 simp-6r 786 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑥𝐵)
41 simpr 487 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑖𝑗)
42 simplr 767 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑎𝑖)
4341, 42sseldd 3961 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑎𝑗)
44 eqid 2820 . . . . . . . . . . . . . . . . 17 (.r𝑅) = (.r𝑅)
4510, 9, 44lidlmcl 19985 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅)) ∧ (𝑥𝐵𝑎𝑗)) → (𝑥(.r𝑅)𝑎) ∈ 𝑗)
4635, 39, 40, 43, 45syl22anc 836 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → (𝑥(.r𝑅)𝑎) ∈ 𝑗)
47 simp-4r 782 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑏𝑗)
48 eqid 2820 . . . . . . . . . . . . . . . 16 (+g𝑅) = (+g𝑅)
4910, 48lidlacl 19981 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅)) ∧ ((𝑥(.r𝑅)𝑎) ∈ 𝑗𝑏𝑗)) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑗)
5035, 39, 46, 47, 49syl22anc 836 . . . . . . . . . . . . . 14 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑗)
5137adantr 483 . . . . . . . . . . . . . 14 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑗𝑍)
52 elunii 4836 . . . . . . . . . . . . . 14 ((((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑗𝑗𝑍) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
5350, 51, 52syl2anc 586 . . . . . . . . . . . . 13 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
5417ad6antr 734 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑅 ∈ Ring)
5536adantr 483 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑍 ⊆ (LIdeal‘𝑅))
56 simplr 767 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → 𝑖𝑍)
5756adantr 483 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑖𝑍)
5855, 57sseldd 3961 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑖 ∈ (LIdeal‘𝑅))
59 simp-6r 786 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑥𝐵)
60 simplr 767 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑎𝑖)
6110, 9, 44lidlmcl 19985 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ (𝑥𝐵𝑎𝑖)) → (𝑥(.r𝑅)𝑎) ∈ 𝑖)
6254, 58, 59, 60, 61syl22anc 836 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → (𝑥(.r𝑅)𝑎) ∈ 𝑖)
63 simpr 487 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑗𝑖)
64 simp-4r 782 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑏𝑗)
6563, 64sseldd 3961 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑏𝑖)
6610, 48lidlacl 19981 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑥(.r𝑅)𝑎) ∈ 𝑖𝑏𝑖)) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑖)
6754, 58, 62, 65, 66syl22anc 836 . . . . . . . . . . . . . 14 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑖)
68 elunii 4836 . . . . . . . . . . . . . 14 ((((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑖𝑖𝑍) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
6967, 57, 68syl2anc 586 . . . . . . . . . . . . 13 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
70 ssmxidllem2.3 . . . . . . . . . . . . . . 15 (𝜑 → [] Or 𝑍)
7170ad5antr 732 . . . . . . . . . . . . . 14 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → [] Or 𝑍)
72 sorpssi 7448 . . . . . . . . . . . . . 14 (( [] Or 𝑍 ∧ (𝑖𝑍𝑗𝑍)) → (𝑖𝑗𝑗𝑖))
7371, 56, 37, 72syl12anc 834 . . . . . . . . . . . . 13 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → (𝑖𝑗𝑗𝑖))
7453, 69, 73mpjaodan 955 . . . . . . . . . . . 12 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7574r19.29an 3287 . . . . . . . . . . 11 (((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ ∃𝑖𝑍 𝑎𝑖) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7675an32s 650 . . . . . . . . . 10 (((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ ∃𝑖𝑍 𝑎𝑖) ∧ 𝑏𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7734, 76sylanb 583 . . . . . . . . 9 (((((𝜑𝑥𝐵) ∧ ∃𝑖𝑍 𝑎𝑖) ∧ 𝑗𝑍) ∧ 𝑏𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7877r19.29an 3287 . . . . . . . 8 ((((𝜑𝑥𝐵) ∧ ∃𝑖𝑍 𝑎𝑖) ∧ ∃𝑗𝑍 𝑏𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7978anasss 469 . . . . . . 7 (((𝜑𝑥𝐵) ∧ (∃𝑖𝑍 𝑎𝑖 ∧ ∃𝑗𝑍 𝑏𝑗)) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
8033, 79sylan2b 595 . . . . . 6 (((𝜑𝑥𝐵) ∧ (𝑎 𝑍𝑏 𝑍)) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
8180ralrimivva 3190 . . . . 5 ((𝜑𝑥𝐵) → ∀𝑎 𝑍𝑏 𝑍((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
8281ralrimiva 3181 . . . 4 (𝜑 → ∀𝑥𝐵𝑎 𝑍𝑏 𝑍((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
8310, 9, 48, 44islidl 19979 . . . 4 ( 𝑍 ∈ (LIdeal‘𝑅) ↔ ( 𝑍𝐵 𝑍 ≠ ∅ ∧ ∀𝑥𝐵𝑎 𝑍𝑏 𝑍((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍))
8415, 30, 82, 83syl3anbrc 1338 . . 3 (𝜑 𝑍 ∈ (LIdeal‘𝑅))
854sselda 3960 . . . . . . . . . 10 ((𝜑𝑗𝑍) → 𝑗𝑃)
86 neeq1 3077 . . . . . . . . . . . 12 (𝑝 = 𝑗 → (𝑝𝐵𝑗𝐵))
87 sseq2 3986 . . . . . . . . . . . 12 (𝑝 = 𝑗 → (𝐼𝑝𝐼𝑗))
8886, 87anbi12d 632 . . . . . . . . . . 11 (𝑝 = 𝑗 → ((𝑝𝐵𝐼𝑝) ↔ (𝑗𝐵𝐼𝑗)))
8988, 5elrab2 3679 . . . . . . . . . 10 (𝑗𝑃 ↔ (𝑗 ∈ (LIdeal‘𝑅) ∧ (𝑗𝐵𝐼𝑗)))
9085, 89sylib 220 . . . . . . . . 9 ((𝜑𝑗𝑍) → (𝑗 ∈ (LIdeal‘𝑅) ∧ (𝑗𝐵𝐼𝑗)))
9190simprld 770 . . . . . . . 8 ((𝜑𝑗𝑍) → 𝑗𝐵)
92 eqid 2820 . . . . . . . . 9 (1r𝑅) = (1r𝑅)
939, 92pridln1 30983 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅) ∧ 𝑗𝐵) → ¬ (1r𝑅) ∈ 𝑗)
9418, 8, 91, 93syl3anc 1366 . . . . . . 7 ((𝜑𝑗𝑍) → ¬ (1r𝑅) ∈ 𝑗)
9594nrexdv 3269 . . . . . 6 (𝜑 → ¬ ∃𝑗𝑍 (1r𝑅) ∈ 𝑗)
96 eluni2 4835 . . . . . 6 ((1r𝑅) ∈ 𝑍 ↔ ∃𝑗𝑍 (1r𝑅) ∈ 𝑗)
9795, 96sylnibr 331 . . . . 5 (𝜑 → ¬ (1r𝑅) ∈ 𝑍)
9810, 9, 92lidl1el 19986 . . . . . . 7 ((𝑅 ∈ Ring ∧ 𝑍 ∈ (LIdeal‘𝑅)) → ((1r𝑅) ∈ 𝑍 𝑍 = 𝐵))
9917, 84, 98syl2anc 586 . . . . . 6 (𝜑 → ((1r𝑅) ∈ 𝑍 𝑍 = 𝐵))
10099necon3bbid 3052 . . . . 5 (𝜑 → (¬ (1r𝑅) ∈ 𝑍 𝑍𝐵))
10197, 100mpbid 234 . . . 4 (𝜑 𝑍𝐵)
10290simprrd 772 . . . . . . 7 ((𝜑𝑗𝑍) → 𝐼𝑗)
103102ralrimiva 3181 . . . . . 6 (𝜑 → ∀𝑗𝑍 𝐼𝑗)
104 ssint 4885 . . . . . 6 (𝐼 𝑍 ↔ ∀𝑗𝑍 𝐼𝑗)
105103, 104sylibr 236 . . . . 5 (𝜑𝐼 𝑍)
106 intssuni 4891 . . . . . 6 (𝑍 ≠ ∅ → 𝑍 𝑍)
10716, 106syl 17 . . . . 5 (𝜑 𝑍 𝑍)
108105, 107sstrd 3970 . . . 4 (𝜑𝐼 𝑍)
109101, 108jca 514 . . 3 (𝜑 → ( 𝑍𝐵𝐼 𝑍))
1103, 84, 109elrabd 3678 . 2 (𝜑 𝑍 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ (𝑝𝐵𝐼𝑝)})
111110, 5eleqtrrdi 2923 1 (𝜑 𝑍𝑃)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wo 843   = wceq 1536  wcel 2113  wne 3015  wral 3137  wrex 3138  {crab 3141  wss 3929  c0 4284   cuni 4831   cint 4869   Or wor 5466  cfv 6348  (class class class)co 7149   [] crpss 7441  Basecbs 16478  +gcplusg 16560  .rcmulr 16561  0gc0g 16708  1rcur 19246  Ringcrg 19292  LIdealclidl 19937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792  ax-rep 5183  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5323  ax-un 7454  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-ne 3016  df-nel 3123  df-ral 3142  df-rex 3143  df-reu 3144  df-rmo 3145  df-rab 3146  df-v 3493  df-sbc 3769  df-csb 3877  df-dif 3932  df-un 3934  df-in 3936  df-ss 3945  df-pss 3947  df-nul 4285  df-if 4461  df-pw 4534  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-int 4870  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-tr 5166  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-rpss 7442  df-om 7574  df-1st 7682  df-2nd 7683  df-wrecs 7940  df-recs 8001  df-rdg 8039  df-er 8282  df-en 8503  df-dom 8504  df-sdom 8505  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-nn 11632  df-2 11694  df-3 11695  df-4 11696  df-5 11697  df-6 11698  df-7 11699  df-8 11700  df-ndx 16481  df-slot 16482  df-base 16484  df-sets 16485  df-ress 16486  df-plusg 16573  df-mulr 16574  df-sca 16576  df-vsca 16577  df-ip 16578  df-0g 16710  df-mgm 17847  df-sgrp 17896  df-mnd 17907  df-grp 18101  df-minusg 18102  df-sbg 18103  df-subg 18271  df-mgp 19235  df-ur 19247  df-ring 19294  df-subrg 19528  df-lmod 19631  df-lss 19699  df-sra 19939  df-rgmod 19940  df-lidl 19941
This theorem is referenced by:  ssmxidl  31003
  Copyright terms: Public domain W3C validator