This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssdifidllem

Description: Lemma for ssdifidl : The set P used in the proof of ssdifidl satisfies the condition of Zorn's Lemma. (Contributed by Thierry Arnoux, 3-Jun-2025)

Ref Expression
Hypotheses ssdifidl.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
ssdifidl.2 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
ssdifidl.3 ⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
ssdifidl.4 ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
ssdifidl.5 ⊢ ( 𝜑 → ( 𝑆 ∩ 𝐼 ) = ∅ )
ssdifidl.6 ⊢ 𝑃 = { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ 𝐼 ⊆ 𝑝 ) }
ssdifidllem.7 ⊢ ( 𝜑 → 𝑍 ⊆ 𝑃 )
ssdifidllem.8 ⊢ ( 𝜑 → 𝑍 ≠ ∅ )
ssdifidllem.9 ⊢ ( 𝜑 → [⊊] Or 𝑍 )
Assertion ssdifidllem ( 𝜑 → ∪ 𝑍 ∈ 𝑃 )

Proof

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