Metamath Proof Explorer

Theorem unichnlidl

Description: The union of a nonempty chain of ideals is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011) (Revised by AV, 28-Jun-2026)

Ref Expression
Assertion unichnlidl ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) → ∪ 𝐶 ∈ ( LIdeal ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 dfss3 ⊢ ( 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ↔ ∀ 𝑖 ∈ 𝐶 𝑖 ∈ ( LIdeal ‘ 𝑅 ) )
2 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
4 2 3 lidlss ⊢ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) → 𝑖 ⊆ ( Base ‘ 𝑅 ) )
5 4 a1i ⊢ ( 𝑅 ∈ Ring → ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) → 𝑖 ⊆ ( Base ‘ 𝑅 ) ) )
6 5 ralimdv ⊢ ( 𝑅 ∈ Ring → ( ∀ 𝑖 ∈ 𝐶 𝑖 ∈ ( LIdeal ‘ 𝑅 ) → ∀ 𝑖 ∈ 𝐶 𝑖 ⊆ ( Base ‘ 𝑅 ) ) )
7 6 imp ⊢ ( ( 𝑅 ∈ Ring ∧ ∀ 𝑖 ∈ 𝐶 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) → ∀ 𝑖 ∈ 𝐶 𝑖 ⊆ ( Base ‘ 𝑅 ) )
8 1 7 sylan2b ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ∀ 𝑖 ∈ 𝐶 𝑖 ⊆ ( Base ‘ 𝑅 ) )
9 unissb ⊢ ( ∪ 𝐶 ⊆ ( Base ‘ 𝑅 ) ↔ ∀ 𝑖 ∈ 𝐶 𝑖 ⊆ ( Base ‘ 𝑅 ) )
10 8 9 sylibr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ∪ 𝐶 ⊆ ( Base ‘ 𝑅 ) )
11 10 3ad2antr2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) → ∪ 𝐶 ⊆ ( Base ‘ 𝑅 ) )
12 lidlunin0 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ∪ 𝐶 ≠ ∅ )
13 12 3adant3r3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) → ∪ 𝐶 ≠ ∅ )
14 eluni2 ⊢ ( 𝑥 ∈ ∪ 𝐶 ↔ ∃ 𝑘 ∈ 𝐶 𝑥 ∈ 𝑘 )
15 eluni2 ⊢ ( 𝑦 ∈ ∪ 𝐶 ↔ ∃ 𝑙 ∈ 𝐶 𝑦 ∈ 𝑙 )
16 simpl ⊢ ( ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) → 𝑘 ∈ 𝐶 )
17 simpl ⊢ ( ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) → 𝑙 ∈ 𝐶 )
18 16 17 anim12i ⊢ ( ( ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) → ( 𝑘 ∈ 𝐶 ∧ 𝑙 ∈ 𝐶 ) )
19 18 3adant1 ⊢ ( ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) → ( 𝑘 ∈ 𝐶 ∧ 𝑙 ∈ 𝐶 ) )
20 19 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) → ( 𝑘 ∈ 𝐶 ∧ 𝑙 ∈ 𝐶 ) )
21 sseq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 ⊆ 𝑗 ↔ 𝑘 ⊆ 𝑗 ) )
22 sseq2 ⊢ ( 𝑖 = 𝑘 → ( 𝑗 ⊆ 𝑖 ↔ 𝑗 ⊆ 𝑘 ) )
23 21 22 orbi12d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ↔ ( 𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘 ) ) )
24 sseq2 ⊢ ( 𝑗 = 𝑙 → ( 𝑘 ⊆ 𝑗 ↔ 𝑘 ⊆ 𝑙 ) )
25 sseq1 ⊢ ( 𝑗 = 𝑙 → ( 𝑗 ⊆ 𝑘 ↔ 𝑙 ⊆ 𝑘 ) )
26 24 25 orbi12d ⊢ ( 𝑗 = 𝑙 → ( ( 𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘 ) ↔ ( 𝑘 ⊆ 𝑙 ∨ 𝑙 ⊆ 𝑘 ) ) )
27 23 26 rspc2v ⊢ ( ( 𝑘 ∈ 𝐶 ∧ 𝑙 ∈ 𝐶 ) → ( ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) → ( 𝑘 ⊆ 𝑙 ∨ 𝑙 ⊆ 𝑘 ) ) )
28 20 27 syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) → ( ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) → ( 𝑘 ⊆ 𝑙 ∨ 𝑙 ⊆ 𝑘 ) ) )
29 simpl1 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) → 𝑅 ∈ Ring )
30 ssel ⊢ ( 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) → ( 𝑘 ∈ 𝐶 → 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) )
31 30 com12 ⊢ ( 𝑘 ∈ 𝐶 → ( 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) → 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) )
32 31 adantr ⊢ ( ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) → ( 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) → 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) )
33 32 3ad2ant2 ⊢ ( ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) → ( 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) → 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) )
34 33 com12 ⊢ ( 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) → ( ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) → 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) )
35 34 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ( ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) → 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) )
36 35 imp ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) → 𝑘 ∈ ( LIdeal ‘ 𝑅 ) )
37 29 36 jca ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) → ( 𝑅 ∈ Ring ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) )
38 simpr ⊢ ( ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) → 𝑥 ∈ 𝑘 )
39 38 anim2i ⊢ ( ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) → ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑘 ) )
40 39 3adant3 ⊢ ( ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) → ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑘 ) )
41 40 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) → ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑘 ) )
42 37 41 jca ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) → ( ( 𝑅 ∈ Ring ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑘 ) ) )
43 42 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑘 ⊆ 𝑙 ∨ 𝑙 ⊆ 𝑘 ) ) → ( ( 𝑅 ∈ Ring ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑘 ) ) )
44 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
45 3 2 44 lidlmcl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑘 ) ) → ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 )
46 43 45 syl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑘 ⊆ 𝑙 ∨ 𝑙 ⊆ 𝑘 ) ) → ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 )
47 ssel ⊢ ( 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) → ( 𝑙 ∈ 𝐶 → 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ) )
48 47 com12 ⊢ ( 𝑙 ∈ 𝐶 → ( 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) → 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ) )
49 48 adantr ⊢ ( ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) → ( 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) → 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ) )
50 49 3ad2ant3 ⊢ ( ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) → ( 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) → 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ) )
51 50 com12 ⊢ ( 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) → ( ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) → 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ) )
52 51 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ( ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) → 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ) )
53 52 imp ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) → 𝑙 ∈ ( LIdeal ‘ 𝑅 ) )
54 29 53 jca ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) → ( 𝑅 ∈ Ring ∧ 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ) )
55 54 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ) → ( 𝑅 ∈ Ring ∧ 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ) )
56 55 adantr ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ) ∧ 𝑘 ⊆ 𝑙 ) → ( 𝑅 ∈ Ring ∧ 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ) )
57 ssel ⊢ ( 𝑘 ⊆ 𝑙 → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 → ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑙 ) )
58 57 com12 ⊢ ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 → ( 𝑘 ⊆ 𝑙 → ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑙 ) )
59 58 adantl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ) → ( 𝑘 ⊆ 𝑙 → ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑙 ) )
60 59 imp ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ) ∧ 𝑘 ⊆ 𝑙 ) → ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑙 )
61 simpr ⊢ ( ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) → 𝑦 ∈ 𝑙 )
62 61 3ad2ant3 ⊢ ( ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) → 𝑦 ∈ 𝑙 )
63 62 ad3antlr ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ) ∧ 𝑘 ⊆ 𝑙 ) → 𝑦 ∈ 𝑙 )
64 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
65 3 64 lidlacl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑙 ∧ 𝑦 ∈ 𝑙 ) ) → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝑙 )
66 56 60 63 65 syl12anc ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ) ∧ 𝑘 ⊆ 𝑙 ) → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝑙 )
67 17 3ad2ant3 ⊢ ( ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) → 𝑙 ∈ 𝐶 )
68 67 ad3antlr ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ) ∧ 𝑘 ⊆ 𝑙 ) → 𝑙 ∈ 𝐶 )
69 elunii ⊢ ( ( ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝑙 ∧ 𝑙 ∈ 𝐶 ) → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
70 66 68 69 syl2anc ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ) ∧ 𝑘 ⊆ 𝑙 ) → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
71 70 ex ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ) → ( 𝑘 ⊆ 𝑙 → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ) )
72 37 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ) → ( 𝑅 ∈ Ring ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) )
73 72 adantr ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ) ∧ 𝑙 ⊆ 𝑘 ) → ( 𝑅 ∈ Ring ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) )
74 simpr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ) → ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 )
75 74 adantr ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ) ∧ 𝑙 ⊆ 𝑘 ) → ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 )
76 ssel ⊢ ( 𝑙 ⊆ 𝑘 → ( 𝑦 ∈ 𝑙 → 𝑦 ∈ 𝑘 ) )
77 76 com12 ⊢ ( 𝑦 ∈ 𝑙 → ( 𝑙 ⊆ 𝑘 → 𝑦 ∈ 𝑘 ) )
78 77 adantl ⊢ ( ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) → ( 𝑙 ⊆ 𝑘 → 𝑦 ∈ 𝑘 ) )
79 78 3ad2ant3 ⊢ ( ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) → ( 𝑙 ⊆ 𝑘 → 𝑦 ∈ 𝑘 ) )
80 79 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) → ( 𝑙 ⊆ 𝑘 → 𝑦 ∈ 𝑘 ) )
81 80 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ) → ( 𝑙 ⊆ 𝑘 → 𝑦 ∈ 𝑘 ) )
82 81 imp ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ) ∧ 𝑙 ⊆ 𝑘 ) → 𝑦 ∈ 𝑘 )
83 3 64 lidlacl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ∧ 𝑦 ∈ 𝑘 ) ) → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝑘 )
84 73 75 82 83 syl12anc ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ) ∧ 𝑙 ⊆ 𝑘 ) → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝑘 )
85 16 3ad2ant2 ⊢ ( ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) → 𝑘 ∈ 𝐶 )
86 85 ad3antlr ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ) ∧ 𝑙 ⊆ 𝑘 ) → 𝑘 ∈ 𝐶 )
87 elunii ⊢ ( ( ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝑘 ∧ 𝑘 ∈ 𝐶 ) → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
88 84 86 87 syl2anc ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ) ∧ 𝑙 ⊆ 𝑘 ) → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
89 88 ex ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ) → ( 𝑙 ⊆ 𝑘 → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ) )
90 71 89 jaod ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ) → ( ( 𝑘 ⊆ 𝑙 ∨ 𝑙 ⊆ 𝑘 ) → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ) )
91 90 impancom ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑘 ⊆ 𝑙 ∨ 𝑙 ⊆ 𝑘 ) ) → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ) )
92 46 91 mpd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) ∧ ( 𝑘 ⊆ 𝑙 ∨ 𝑙 ⊆ 𝑘 ) ) → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
93 92 ex ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) → ( ( 𝑘 ⊆ 𝑙 ∨ 𝑙 ⊆ 𝑘 ) → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ) )
94 28 93 syld ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) ) → ( ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ) )
95 94 ex ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ( ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) → ( ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ) ) )
96 95 com23 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ( ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) → ( ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ) ) )
97 96 3exp ⊢ ( 𝑅 ∈ Ring → ( 𝐶 ≠ ∅ → ( 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) → ( ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) → ( ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ) ) ) ) )
98 97 3imp2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) → ( ( 𝑏 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ) )
99 98 3expd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) → ( 𝑏 ∈ ( Base ‘ 𝑅 ) → ( ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) → ( ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ) ) ) )
100 99 imp41 ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ ( 𝑙 ∈ 𝐶 ∧ 𝑦 ∈ 𝑙 ) ) → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
101 100 rexlimdvaa ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) → ( ∃ 𝑙 ∈ 𝐶 𝑦 ∈ 𝑙 → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ) )
102 15 101 biimtrid ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) → ( 𝑦 ∈ ∪ 𝐶 → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ) )
103 102 ralrimiv ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) → ∀ 𝑦 ∈ ∪ 𝐶 ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
104 103 rexlimdvaa ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) → ( ∃ 𝑘 ∈ 𝐶 𝑥 ∈ 𝑘 → ∀ 𝑦 ∈ ∪ 𝐶 ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ) )
105 14 104 biimtrid ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ∈ ∪ 𝐶 → ∀ 𝑦 ∈ ∪ 𝐶 ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ) )
106 105 ralrimiv ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) → ∀ 𝑥 ∈ ∪ 𝐶 ∀ 𝑦 ∈ ∪ 𝐶 ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
107 106 ralrimiva ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) → ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ∀ 𝑥 ∈ ∪ 𝐶 ∀ 𝑦 ∈ ∪ 𝐶 ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
108 3 2 64 44 islidl ⊢ ( ∪ 𝐶 ∈ ( LIdeal ‘ 𝑅 ) ↔ ( ∪ 𝐶 ⊆ ( Base ‘ 𝑅 ) ∧ ∪ 𝐶 ≠ ∅ ∧ ∀ 𝑏 ∈ ( Base ‘ 𝑅 ) ∀ 𝑥 ∈ ∪ 𝐶 ∀ 𝑦 ∈ ∪ 𝐶 ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ) )
109 11 13 107 108 syl3anbrc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) → ∪ 𝐶 ∈ ( LIdeal ‘ 𝑅 ) )