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

Theorem ssmxidllem 30999
 Description: The set 𝑃 used in the proof of ssmxidl 31000 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 3075 . . . 4 (𝑝 = 𝑍 → (𝑝𝐵 𝑍𝐵))
2 sseq2 3977 . . . 4 (𝑝 = 𝑍 → (𝐼𝑝𝐼 𝑍))
31, 2anbi12d 633 . . 3 (𝑝 = 𝑍 → ((𝑝𝐵𝐼𝑝) ↔ ( 𝑍𝐵𝐼 𝑍)))
4 ssmxidllem2.1 . . . . . . . . 9 (𝜑𝑍𝑃)
5 ssmxidllem.1 . . . . . . . . . 10 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ (𝑝𝐵𝐼𝑝)}
65ssrab3 4041 . . . . . . . . 9 𝑃 ⊆ (LIdeal‘𝑅)
74, 6sstrdi 3963 . . . . . . . 8 (𝜑𝑍 ⊆ (LIdeal‘𝑅))
87sselda 3951 . . . . . . 7 ((𝜑𝑗𝑍) → 𝑗 ∈ (LIdeal‘𝑅))
9 ssmxidl.1 . . . . . . . 8 𝐵 = (Base‘𝑅)
10 eqid 2824 . . . . . . . 8 (LIdeal‘𝑅) = (LIdeal‘𝑅)
119, 10lidlss 19969 . . . . . . 7 (𝑗 ∈ (LIdeal‘𝑅) → 𝑗𝐵)
128, 11syl 17 . . . . . 6 ((𝜑𝑗𝑍) → 𝑗𝐵)
1312ralrimiva 3176 . . . . 5 (𝜑 → ∀𝑗𝑍 𝑗𝐵)
14 unissb 4851 . . . . 5 ( 𝑍𝐵 ↔ ∀𝑗𝑍 𝑗𝐵)
1513, 14sylibr 237 . . . 4 (𝜑 𝑍𝐵)
16 ssmxidllem2.2 . . . . . . 7 (𝜑𝑍 ≠ ∅)
17 ssmxidllem.2 . . . . . . . . . . 11 (𝜑𝑅 ∈ Ring)
1817adantr 484 . . . . . . . . . 10 ((𝜑𝑗𝑍) → 𝑅 ∈ Ring)
19 eqid 2824 . . . . . . . . . . 11 (0g𝑅) = (0g𝑅)
2010, 19lidl0cl 19971 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅)) → (0g𝑅) ∈ 𝑗)
2118, 8, 20syl2anc 587 . . . . . . . . 9 ((𝜑𝑗𝑍) → (0g𝑅) ∈ 𝑗)
22 n0i 4280 . . . . . . . . 9 ((0g𝑅) ∈ 𝑗 → ¬ 𝑗 = ∅)
2321, 22syl 17 . . . . . . . 8 ((𝜑𝑗𝑍) → ¬ 𝑗 = ∅)
2423reximdva0 4293 . . . . . . 7 ((𝜑𝑍 ≠ ∅) → ∃𝑗𝑍 ¬ 𝑗 = ∅)
2516, 24mpdan 686 . . . . . 6 (𝜑 → ∃𝑗𝑍 ¬ 𝑗 = ∅)
26 rexnal 3232 . . . . . 6 (∃𝑗𝑍 ¬ 𝑗 = ∅ ↔ ¬ ∀𝑗𝑍 𝑗 = ∅)
2725, 26sylib 221 . . . . 5 (𝜑 → ¬ ∀𝑗𝑍 𝑗 = ∅)
28 uni0c 4846 . . . . . 6 ( 𝑍 = ∅ ↔ ∀𝑗𝑍 𝑗 = ∅)
2928necon3abii 3059 . . . . 5 ( 𝑍 ≠ ∅ ↔ ¬ ∀𝑗𝑍 𝑗 = ∅)
3027, 29sylibr 237 . . . 4 (𝜑 𝑍 ≠ ∅)
31 eluni2 4823 . . . . . . . 8 (𝑎 𝑍 ↔ ∃𝑖𝑍 𝑎𝑖)
32 eluni2 4823 . . . . . . . 8 (𝑏 𝑍 ↔ ∃𝑗𝑍 𝑏𝑗)
3331, 32anbi12i 629 . . . . . . 7 ((𝑎 𝑍𝑏 𝑍) ↔ (∃𝑖𝑍 𝑎𝑖 ∧ ∃𝑗𝑍 𝑏𝑗))
34 an32 645 . . . . . . . . . 10 ((((𝜑𝑥𝐵) ∧ ∃𝑖𝑍 𝑎𝑖) ∧ 𝑗𝑍) ↔ (((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ ∃𝑖𝑍 𝑎𝑖))
3517ad6antr 735 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑅 ∈ Ring)
367ad5antr 733 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → 𝑍 ⊆ (LIdeal‘𝑅))
37 simp-4r 783 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → 𝑗𝑍)
3836, 37sseldd 3952 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → 𝑗 ∈ (LIdeal‘𝑅))
3938adantr 484 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑗 ∈ (LIdeal‘𝑅))
40 simp-6r 787 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑥𝐵)
41 simpr 488 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑖𝑗)
42 simplr 768 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑎𝑖)
4341, 42sseldd 3952 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑎𝑗)
44 eqid 2824 . . . . . . . . . . . . . . . . 17 (.r𝑅) = (.r𝑅)
4510, 9, 44lidlmcl 19976 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅)) ∧ (𝑥𝐵𝑎𝑗)) → (𝑥(.r𝑅)𝑎) ∈ 𝑗)
4635, 39, 40, 43, 45syl22anc 837 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → (𝑥(.r𝑅)𝑎) ∈ 𝑗)
47 simp-4r 783 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑏𝑗)
48 eqid 2824 . . . . . . . . . . . . . . . 16 (+g𝑅) = (+g𝑅)
4910, 48lidlacl 19972 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅)) ∧ ((𝑥(.r𝑅)𝑎) ∈ 𝑗𝑏𝑗)) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑗)
5035, 39, 46, 47, 49syl22anc 837 . . . . . . . . . . . . . 14 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑗)
5137adantr 484 . . . . . . . . . . . . . 14 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑖𝑗) → 𝑗𝑍)
52 elunii 4824 . . . . . . . . . . . . . 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 3952 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑖 ∈ (LIdeal‘𝑅))
59 simp-6r 787 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑥𝐵)
60 simplr 768 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑎𝑖)
6110, 9, 44lidlmcl 19976 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ (𝑥𝐵𝑎𝑖)) → (𝑥(.r𝑅)𝑎) ∈ 𝑖)
6254, 58, 59, 60, 61syl22anc 837 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → (𝑥(.r𝑅)𝑎) ∈ 𝑖)
63 simpr 488 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑗𝑖)
64 simp-4r 783 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑏𝑗)
6563, 64sseldd 3952 . . . . . . . . . . . . . . 15 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → 𝑏𝑖)
6610, 48lidlacl 19972 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑥(.r𝑅)𝑎) ∈ 𝑖𝑏𝑖)) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑖)
6754, 58, 62, 65, 66syl22anc 837 . . . . . . . . . . . . . 14 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑖)
68 elunii 4824 . . . . . . . . . . . . . 14 ((((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑖𝑖𝑍) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
6967, 57, 68syl2anc 587 . . . . . . . . . . . . 13 (((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) ∧ 𝑗𝑖) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
70 ssmxidllem2.3 . . . . . . . . . . . . . . 15 (𝜑 → [] Or 𝑍)
7170ad5antr 733 . . . . . . . . . . . . . 14 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → [] Or 𝑍)
72 sorpssi 7438 . . . . . . . . . . . . . 14 (( [] Or 𝑍 ∧ (𝑖𝑍𝑗𝑍)) → (𝑖𝑗𝑗𝑖))
7371, 56, 37, 72syl12anc 835 . . . . . . . . . . . . 13 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → (𝑖𝑗𝑗𝑖))
7453, 69, 73mpjaodan 956 . . . . . . . . . . . 12 ((((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ 𝑖𝑍) ∧ 𝑎𝑖) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7574r19.29an 3280 . . . . . . . . . . 11 (((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ 𝑏𝑗) ∧ ∃𝑖𝑍 𝑎𝑖) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7675an32s 651 . . . . . . . . . 10 (((((𝜑𝑥𝐵) ∧ 𝑗𝑍) ∧ ∃𝑖𝑍 𝑎𝑖) ∧ 𝑏𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7734, 76sylanb 584 . . . . . . . . 9 (((((𝜑𝑥𝐵) ∧ ∃𝑖𝑍 𝑎𝑖) ∧ 𝑗𝑍) ∧ 𝑏𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7877r19.29an 3280 . . . . . . . 8 ((((𝜑𝑥𝐵) ∧ ∃𝑖𝑍 𝑎𝑖) ∧ ∃𝑗𝑍 𝑏𝑗) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
7978anasss 470 . . . . . . 7 (((𝜑𝑥𝐵) ∧ (∃𝑖𝑍 𝑎𝑖 ∧ ∃𝑗𝑍 𝑏𝑗)) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
8033, 79sylan2b 596 . . . . . 6 (((𝜑𝑥𝐵) ∧ (𝑎 𝑍𝑏 𝑍)) → ((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
8180ralrimivva 3185 . . . . 5 ((𝜑𝑥𝐵) → ∀𝑎 𝑍𝑏 𝑍((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
8281ralrimiva 3176 . . . 4 (𝜑 → ∀𝑥𝐵𝑎 𝑍𝑏 𝑍((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍)
8310, 9, 48, 44islidl 19970 . . . 4 ( 𝑍 ∈ (LIdeal‘𝑅) ↔ ( 𝑍𝐵 𝑍 ≠ ∅ ∧ ∀𝑥𝐵𝑎 𝑍𝑏 𝑍((𝑥(.r𝑅)𝑎)(+g𝑅)𝑏) ∈ 𝑍))
8415, 30, 82, 83syl3anbrc 1340 . . 3 (𝜑 𝑍 ∈ (LIdeal‘𝑅))
854sselda 3951 . . . . . . . . . 10 ((𝜑𝑗𝑍) → 𝑗𝑃)
86 neeq1 3075 . . . . . . . . . . . 12 (𝑝 = 𝑗 → (𝑝𝐵𝑗𝐵))
87 sseq2 3977 . . . . . . . . . . . 12 (𝑝 = 𝑗 → (𝐼𝑝𝐼𝑗))
8886, 87anbi12d 633 . . . . . . . . . . 11 (𝑝 = 𝑗 → ((𝑝𝐵𝐼𝑝) ↔ (𝑗𝐵𝐼𝑗)))
8988, 5elrab2 3668 . . . . . . . . . 10 (𝑗𝑃 ↔ (𝑗 ∈ (LIdeal‘𝑅) ∧ (𝑗𝐵𝐼𝑗)))
9085, 89sylib 221 . . . . . . . . 9 ((𝜑𝑗𝑍) → (𝑗 ∈ (LIdeal‘𝑅) ∧ (𝑗𝐵𝐼𝑗)))
9190simprld 771 . . . . . . . 8 ((𝜑𝑗𝑍) → 𝑗𝐵)
92 eqid 2824 . . . . . . . . 9 (1r𝑅) = (1r𝑅)
939, 92pridln1 30980 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝑗 ∈ (LIdeal‘𝑅) ∧ 𝑗𝐵) → ¬ (1r𝑅) ∈ 𝑗)
9418, 8, 91, 93syl3anc 1368 . . . . . . 7 ((𝜑𝑗𝑍) → ¬ (1r𝑅) ∈ 𝑗)
9594nrexdv 3262 . . . . . 6 (𝜑 → ¬ ∃𝑗𝑍 (1r𝑅) ∈ 𝑗)
96 eluni2 4823 . . . . . 6 ((1r𝑅) ∈ 𝑍 ↔ ∃𝑗𝑍 (1r𝑅) ∈ 𝑗)
9795, 96sylnibr 332 . . . . 5 (𝜑 → ¬ (1r𝑅) ∈ 𝑍)
9810, 9, 92lidl1el 19977 . . . . . . 7 ((𝑅 ∈ Ring ∧ 𝑍 ∈ (LIdeal‘𝑅)) → ((1r𝑅) ∈ 𝑍 𝑍 = 𝐵))
9917, 84, 98syl2anc 587 . . . . . 6 (𝜑 → ((1r𝑅) ∈ 𝑍 𝑍 = 𝐵))
10099necon3bbid 3050 . . . . 5 (𝜑 → (¬ (1r𝑅) ∈ 𝑍 𝑍𝐵))
10197, 100mpbid 235 . . . 4 (𝜑 𝑍𝐵)
10290simprrd 773 . . . . . . 7 ((𝜑𝑗𝑍) → 𝐼𝑗)
103102ralrimiva 3176 . . . . . 6 (𝜑 → ∀𝑗𝑍 𝐼𝑗)
104 ssint 4873 . . . . . 6 (𝐼 𝑍 ↔ ∀𝑗𝑍 𝐼𝑗)
105103, 104sylibr 237 . . . . 5 (𝜑𝐼 𝑍)
106 intssuni 4879 . . . . . 6 (𝑍 ≠ ∅ → 𝑍 𝑍)
10716, 106syl 17 . . . . 5 (𝜑 𝑍 𝑍)
108105, 107sstrd 3961 . . . 4 (𝜑𝐼 𝑍)
109101, 108jca 515 . . 3 (𝜑 → ( 𝑍𝐵𝐼 𝑍))
1103, 84, 109elrabd 3667 . 2 (𝜑 𝑍 ∈ {𝑝 ∈ (LIdeal‘𝑅) ∣ (𝑝𝐵𝐼𝑝)})
111110, 5eleqtrrdi 2927 1 (𝜑 𝑍𝑃)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2115   ≠ wne 3013  ∀wral 3132  ∃wrex 3133  {crab 3136   ⊆ wss 3918  ∅c0 4274  ∪ cuni 4819  ∩ cint 4857   Or wor 5454  ‘cfv 6336  (class class class)co 7138   [⊊] crpss 7431  Basecbs 16472  +gcplusg 16554  .rcmulr 16555  0gc0g 16702  1rcur 19240  Ringcrg 19286  LIdealclidl 19928 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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5171  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311  ax-un 7444  ax-cnex 10578  ax-resscn 10579  ax-1cn 10580  ax-icn 10581  ax-addcl 10582  ax-addrcl 10583  ax-mulcl 10584  ax-mulrcl 10585  ax-mulcom 10586  ax-addass 10587  ax-mulass 10588  ax-distr 10589  ax-i2m1 10590  ax-1ne0 10591  ax-1rid 10592  ax-rnegex 10593  ax-rrecex 10594  ax-cnre 10595  ax-pre-lttri 10596  ax-pre-lttrn 10597  ax-pre-ltadd 10598  ax-pre-mulgt0 10599 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3014  df-nel 3118  df-ral 3137  df-rex 3138  df-reu 3139  df-rmo 3140  df-rab 3141  df-v 3481  df-sbc 3758  df-csb 3866  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-pss 3937  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-tp 4553  df-op 4555  df-uni 4820  df-int 4858  df-iun 4902  df-br 5048  df-opab 5110  df-mpt 5128  df-tr 5154  df-id 5441  df-eprel 5446  df-po 5455  df-so 5456  df-fr 5495  df-we 5497  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7096  df-ov 7141  df-oprab 7142  df-mpo 7143  df-rpss 7432  df-om 7564  df-1st 7672  df-2nd 7673  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10662  df-mnf 10663  df-xr 10664  df-ltxr 10665  df-le 10666  df-sub 10857  df-neg 10858  df-nn 11624  df-2 11686  df-3 11687  df-4 11688  df-5 11689  df-6 11690  df-7 11691  df-8 11692  df-ndx 16475  df-slot 16476  df-base 16478  df-sets 16479  df-ress 16480  df-plusg 16567  df-mulr 16568  df-sca 16570  df-vsca 16571  df-ip 16572  df-0g 16704  df-mgm 17841  df-sgrp 17890  df-mnd 17901  df-grp 18095  df-minusg 18096  df-sbg 18097  df-subg 18265  df-mgp 19229  df-ur 19241  df-ring 19288  df-subrg 19519  df-lmod 19622  df-lss 19690  df-sra 19930  df-rgmod 19931  df-lidl 19932 This theorem is referenced by:  ssmxidl  31000
 Copyright terms: Public domain W3C validator