Metamath Proof Explorer


Theorem ssmxidllem

Description: The set P used in the proof of ssmxidl satisfies the condition of Zorn's Lemma. (Contributed by Thierry Arnoux, 10-Apr-2024)

Ref Expression
Hypotheses ssmxidl.1 𝐵 = ( Base ‘ 𝑅 )
ssmxidllem.1 𝑃 = { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝𝐵𝐼𝑝 ) }
ssmxidllem.2 ( 𝜑𝑅 ∈ Ring )
ssmxidllem.3 ( 𝜑𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
ssmxidllem.4 ( 𝜑𝐼𝐵 )
ssmxidllem2.1 ( 𝜑𝑍𝑃 )
ssmxidllem2.2 ( 𝜑𝑍 ≠ ∅ )
ssmxidllem2.3 ( 𝜑 → [] Or 𝑍 )
Assertion ssmxidllem ( 𝜑 𝑍𝑃 )

Proof

Step Hyp Ref Expression
1 ssmxidl.1 𝐵 = ( Base ‘ 𝑅 )
2 ssmxidllem.1 𝑃 = { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝𝐵𝐼𝑝 ) }
3 ssmxidllem.2 ( 𝜑𝑅 ∈ Ring )
4 ssmxidllem.3 ( 𝜑𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
5 ssmxidllem.4 ( 𝜑𝐼𝐵 )
6 ssmxidllem2.1 ( 𝜑𝑍𝑃 )
7 ssmxidllem2.2 ( 𝜑𝑍 ≠ ∅ )
8 ssmxidllem2.3 ( 𝜑 → [] Or 𝑍 )
9 neeq1 ( 𝑝 = 𝑍 → ( 𝑝𝐵 𝑍𝐵 ) )
10 sseq2 ( 𝑝 = 𝑍 → ( 𝐼𝑝𝐼 𝑍 ) )
11 9 10 anbi12d ( 𝑝 = 𝑍 → ( ( 𝑝𝐵𝐼𝑝 ) ↔ ( 𝑍𝐵𝐼 𝑍 ) ) )
12 2 ssrab3 𝑃 ⊆ ( LIdeal ‘ 𝑅 )
13 6 12 sstrdi ( 𝜑𝑍 ⊆ ( LIdeal ‘ 𝑅 ) )
14 13 sselda ( ( 𝜑𝑗𝑍 ) → 𝑗 ∈ ( LIdeal ‘ 𝑅 ) )
15 eqid ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
16 1 15 lidlss ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) → 𝑗𝐵 )
17 14 16 syl ( ( 𝜑𝑗𝑍 ) → 𝑗𝐵 )
18 17 ralrimiva ( 𝜑 → ∀ 𝑗𝑍 𝑗𝐵 )
19 unissb ( 𝑍𝐵 ↔ ∀ 𝑗𝑍 𝑗𝐵 )
20 18 19 sylibr ( 𝜑 𝑍𝐵 )
21 3 adantr ( ( 𝜑𝑗𝑍 ) → 𝑅 ∈ Ring )
22 eqid ( 0g𝑅 ) = ( 0g𝑅 )
23 15 22 lidl0cl ( ( 𝑅 ∈ Ring ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 0g𝑅 ) ∈ 𝑗 )
24 21 14 23 syl2anc ( ( 𝜑𝑗𝑍 ) → ( 0g𝑅 ) ∈ 𝑗 )
25 n0i ( ( 0g𝑅 ) ∈ 𝑗 → ¬ 𝑗 = ∅ )
26 24 25 syl ( ( 𝜑𝑗𝑍 ) → ¬ 𝑗 = ∅ )
27 26 reximdva0 ( ( 𝜑𝑍 ≠ ∅ ) → ∃ 𝑗𝑍 ¬ 𝑗 = ∅ )
28 7 27 mpdan ( 𝜑 → ∃ 𝑗𝑍 ¬ 𝑗 = ∅ )
29 rexnal ( ∃ 𝑗𝑍 ¬ 𝑗 = ∅ ↔ ¬ ∀ 𝑗𝑍 𝑗 = ∅ )
30 28 29 sylib ( 𝜑 → ¬ ∀ 𝑗𝑍 𝑗 = ∅ )
31 uni0c ( 𝑍 = ∅ ↔ ∀ 𝑗𝑍 𝑗 = ∅ )
32 31 necon3abii ( 𝑍 ≠ ∅ ↔ ¬ ∀ 𝑗𝑍 𝑗 = ∅ )
33 30 32 sylibr ( 𝜑 𝑍 ≠ ∅ )
34 eluni2 ( 𝑎 𝑍 ↔ ∃ 𝑖𝑍 𝑎𝑖 )
35 eluni2 ( 𝑏 𝑍 ↔ ∃ 𝑗𝑍 𝑏𝑗 )
36 34 35 anbi12i ( ( 𝑎 𝑍𝑏 𝑍 ) ↔ ( ∃ 𝑖𝑍 𝑎𝑖 ∧ ∃ 𝑗𝑍 𝑏𝑗 ) )
37 an32 ( ( ( ( 𝜑𝑥𝐵 ) ∧ ∃ 𝑖𝑍 𝑎𝑖 ) ∧ 𝑗𝑍 ) ↔ ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ ∃ 𝑖𝑍 𝑎𝑖 ) )
38 3 ad6antr ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑖𝑗 ) → 𝑅 ∈ Ring )
39 13 ad5antr ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) → 𝑍 ⊆ ( LIdeal ‘ 𝑅 ) )
40 simp-4r ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) → 𝑗𝑍 )
41 39 40 sseldd ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) → 𝑗 ∈ ( LIdeal ‘ 𝑅 ) )
42 41 adantr ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑖𝑗 ) → 𝑗 ∈ ( LIdeal ‘ 𝑅 ) )
43 simp-6r ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑖𝑗 ) → 𝑥𝐵 )
44 simpr ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑖𝑗 ) → 𝑖𝑗 )
45 simplr ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑖𝑗 ) → 𝑎𝑖 )
46 44 45 sseldd ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑖𝑗 ) → 𝑎𝑗 )
47 eqid ( .r𝑅 ) = ( .r𝑅 )
48 15 1 47 lidlmcl ( ( ( 𝑅 ∈ Ring ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑥𝐵𝑎𝑗 ) ) → ( 𝑥 ( .r𝑅 ) 𝑎 ) ∈ 𝑗 )
49 38 42 43 46 48 syl22anc ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑖𝑗 ) → ( 𝑥 ( .r𝑅 ) 𝑎 ) ∈ 𝑗 )
50 simp-4r ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑖𝑗 ) → 𝑏𝑗 )
51 eqid ( +g𝑅 ) = ( +g𝑅 )
52 15 51 lidlacl ( ( ( 𝑅 ∈ Ring ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r𝑅 ) 𝑎 ) ∈ 𝑗𝑏𝑗 ) ) → ( ( 𝑥 ( .r𝑅 ) 𝑎 ) ( +g𝑅 ) 𝑏 ) ∈ 𝑗 )
53 38 42 49 50 52 syl22anc ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑖𝑗 ) → ( ( 𝑥 ( .r𝑅 ) 𝑎 ) ( +g𝑅 ) 𝑏 ) ∈ 𝑗 )
54 40 adantr ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑖𝑗 ) → 𝑗𝑍 )
55 elunii ( ( ( ( 𝑥 ( .r𝑅 ) 𝑎 ) ( +g𝑅 ) 𝑏 ) ∈ 𝑗𝑗𝑍 ) → ( ( 𝑥 ( .r𝑅 ) 𝑎 ) ( +g𝑅 ) 𝑏 ) ∈ 𝑍 )
56 53 54 55 syl2anc ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑖𝑗 ) → ( ( 𝑥 ( .r𝑅 ) 𝑎 ) ( +g𝑅 ) 𝑏 ) ∈ 𝑍 )
57 3 ad6antr ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑗𝑖 ) → 𝑅 ∈ Ring )
58 39 adantr ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑗𝑖 ) → 𝑍 ⊆ ( LIdeal ‘ 𝑅 ) )
59 simplr ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) → 𝑖𝑍 )
60 59 adantr ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑗𝑖 ) → 𝑖𝑍 )
61 58 60 sseldd ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑗𝑖 ) → 𝑖 ∈ ( LIdeal ‘ 𝑅 ) )
62 simp-6r ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑗𝑖 ) → 𝑥𝐵 )
63 simplr ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑗𝑖 ) → 𝑎𝑖 )
64 15 1 47 lidlmcl ( ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑥𝐵𝑎𝑖 ) ) → ( 𝑥 ( .r𝑅 ) 𝑎 ) ∈ 𝑖 )
65 57 61 62 63 64 syl22anc ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑗𝑖 ) → ( 𝑥 ( .r𝑅 ) 𝑎 ) ∈ 𝑖 )
66 simpr ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑗𝑖 ) → 𝑗𝑖 )
67 simp-4r ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑗𝑖 ) → 𝑏𝑗 )
68 66 67 sseldd ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑗𝑖 ) → 𝑏𝑖 )
69 15 51 lidlacl ( ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r𝑅 ) 𝑎 ) ∈ 𝑖𝑏𝑖 ) ) → ( ( 𝑥 ( .r𝑅 ) 𝑎 ) ( +g𝑅 ) 𝑏 ) ∈ 𝑖 )
70 57 61 65 68 69 syl22anc ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑗𝑖 ) → ( ( 𝑥 ( .r𝑅 ) 𝑎 ) ( +g𝑅 ) 𝑏 ) ∈ 𝑖 )
71 elunii ( ( ( ( 𝑥 ( .r𝑅 ) 𝑎 ) ( +g𝑅 ) 𝑏 ) ∈ 𝑖𝑖𝑍 ) → ( ( 𝑥 ( .r𝑅 ) 𝑎 ) ( +g𝑅 ) 𝑏 ) ∈ 𝑍 )
72 70 60 71 syl2anc ( ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) ∧ 𝑗𝑖 ) → ( ( 𝑥 ( .r𝑅 ) 𝑎 ) ( +g𝑅 ) 𝑏 ) ∈ 𝑍 )
73 8 ad5antr ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) → [] Or 𝑍 )
74 sorpssi ( ( [] Or 𝑍 ∧ ( 𝑖𝑍𝑗𝑍 ) ) → ( 𝑖𝑗𝑗𝑖 ) )
75 73 59 40 74 syl12anc ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) → ( 𝑖𝑗𝑗𝑖 ) )
76 56 72 75 mpjaodan ( ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ 𝑖𝑍 ) ∧ 𝑎𝑖 ) → ( ( 𝑥 ( .r𝑅 ) 𝑎 ) ( +g𝑅 ) 𝑏 ) ∈ 𝑍 )
77 76 r19.29an ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) ∧ ∃ 𝑖𝑍 𝑎𝑖 ) → ( ( 𝑥 ( .r𝑅 ) 𝑎 ) ( +g𝑅 ) 𝑏 ) ∈ 𝑍 )
78 77 an32s ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑗𝑍 ) ∧ ∃ 𝑖𝑍 𝑎𝑖 ) ∧ 𝑏𝑗 ) → ( ( 𝑥 ( .r𝑅 ) 𝑎 ) ( +g𝑅 ) 𝑏 ) ∈ 𝑍 )
79 37 78 sylanb ( ( ( ( ( 𝜑𝑥𝐵 ) ∧ ∃ 𝑖𝑍 𝑎𝑖 ) ∧ 𝑗𝑍 ) ∧ 𝑏𝑗 ) → ( ( 𝑥 ( .r𝑅 ) 𝑎 ) ( +g𝑅 ) 𝑏 ) ∈ 𝑍 )
80 79 r19.29an ( ( ( ( 𝜑𝑥𝐵 ) ∧ ∃ 𝑖𝑍 𝑎𝑖 ) ∧ ∃ 𝑗𝑍 𝑏𝑗 ) → ( ( 𝑥 ( .r𝑅 ) 𝑎 ) ( +g𝑅 ) 𝑏 ) ∈ 𝑍 )
81 80 anasss ( ( ( 𝜑𝑥𝐵 ) ∧ ( ∃ 𝑖𝑍 𝑎𝑖 ∧ ∃ 𝑗𝑍 𝑏𝑗 ) ) → ( ( 𝑥 ( .r𝑅 ) 𝑎 ) ( +g𝑅 ) 𝑏 ) ∈ 𝑍 )
82 36 81 sylan2b ( ( ( 𝜑𝑥𝐵 ) ∧ ( 𝑎 𝑍𝑏 𝑍 ) ) → ( ( 𝑥 ( .r𝑅 ) 𝑎 ) ( +g𝑅 ) 𝑏 ) ∈ 𝑍 )
83 82 ralrimivva ( ( 𝜑𝑥𝐵 ) → ∀ 𝑎 𝑍𝑏 𝑍 ( ( 𝑥 ( .r𝑅 ) 𝑎 ) ( +g𝑅 ) 𝑏 ) ∈ 𝑍 )
84 83 ralrimiva ( 𝜑 → ∀ 𝑥𝐵𝑎 𝑍𝑏 𝑍 ( ( 𝑥 ( .r𝑅 ) 𝑎 ) ( +g𝑅 ) 𝑏 ) ∈ 𝑍 )
85 15 1 51 47 islidl ( 𝑍 ∈ ( LIdeal ‘ 𝑅 ) ↔ ( 𝑍𝐵 𝑍 ≠ ∅ ∧ ∀ 𝑥𝐵𝑎 𝑍𝑏 𝑍 ( ( 𝑥 ( .r𝑅 ) 𝑎 ) ( +g𝑅 ) 𝑏 ) ∈ 𝑍 ) )
86 20 33 84 85 syl3anbrc ( 𝜑 𝑍 ∈ ( LIdeal ‘ 𝑅 ) )
87 6 sselda ( ( 𝜑𝑗𝑍 ) → 𝑗𝑃 )
88 neeq1 ( 𝑝 = 𝑗 → ( 𝑝𝐵𝑗𝐵 ) )
89 sseq2 ( 𝑝 = 𝑗 → ( 𝐼𝑝𝐼𝑗 ) )
90 88 89 anbi12d ( 𝑝 = 𝑗 → ( ( 𝑝𝐵𝐼𝑝 ) ↔ ( 𝑗𝐵𝐼𝑗 ) ) )
91 90 2 elrab2 ( 𝑗𝑃 ↔ ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑗𝐵𝐼𝑗 ) ) )
92 87 91 sylib ( ( 𝜑𝑗𝑍 ) → ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝑗𝐵𝐼𝑗 ) ) )
93 92 simprld ( ( 𝜑𝑗𝑍 ) → 𝑗𝐵 )
94 eqid ( 1r𝑅 ) = ( 1r𝑅 )
95 1 94 pridln1 ( ( 𝑅 ∈ Ring ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑗𝐵 ) → ¬ ( 1r𝑅 ) ∈ 𝑗 )
96 21 14 93 95 syl3anc ( ( 𝜑𝑗𝑍 ) → ¬ ( 1r𝑅 ) ∈ 𝑗 )
97 96 nrexdv ( 𝜑 → ¬ ∃ 𝑗𝑍 ( 1r𝑅 ) ∈ 𝑗 )
98 eluni2 ( ( 1r𝑅 ) ∈ 𝑍 ↔ ∃ 𝑗𝑍 ( 1r𝑅 ) ∈ 𝑗 )
99 97 98 sylnibr ( 𝜑 → ¬ ( 1r𝑅 ) ∈ 𝑍 )
100 15 1 94 lidl1el ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ ( LIdeal ‘ 𝑅 ) ) → ( ( 1r𝑅 ) ∈ 𝑍 𝑍 = 𝐵 ) )
101 3 86 100 syl2anc ( 𝜑 → ( ( 1r𝑅 ) ∈ 𝑍 𝑍 = 𝐵 ) )
102 101 necon3bbid ( 𝜑 → ( ¬ ( 1r𝑅 ) ∈ 𝑍 𝑍𝐵 ) )
103 99 102 mpbid ( 𝜑 𝑍𝐵 )
104 92 simprrd ( ( 𝜑𝑗𝑍 ) → 𝐼𝑗 )
105 104 ralrimiva ( 𝜑 → ∀ 𝑗𝑍 𝐼𝑗 )
106 ssint ( 𝐼 𝑍 ↔ ∀ 𝑗𝑍 𝐼𝑗 )
107 105 106 sylibr ( 𝜑𝐼 𝑍 )
108 intssuni ( 𝑍 ≠ ∅ → 𝑍 𝑍 )
109 7 108 syl ( 𝜑 𝑍 𝑍 )
110 107 109 sstrd ( 𝜑𝐼 𝑍 )
111 103 110 jca ( 𝜑 → ( 𝑍𝐵𝐼 𝑍 ) )
112 11 86 111 elrabd ( 𝜑 𝑍 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑝𝐵𝐼𝑝 ) } )
113 112 2 eleqtrrdi ( 𝜑 𝑍𝑃 )