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 ⊢ ( 𝜑 → ∪ 𝑍 ∈ 𝑃 )