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

Metamath Proof Explorer

Theorem unichnidl

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

Ref Expression
Assertion unichnidl ( ( 𝑅 ∈ RingOps ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) → ∪ 𝐶 ∈ ( Idl ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 dfss3 ⊢ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ↔ ∀ 𝑖 ∈ 𝐶 𝑖 ∈ ( Idl ‘ 𝑅 ) )
2 eqid ⊢ ( 1st ‘ 𝑅 ) = ( 1st ‘ 𝑅 )
3 eqid ⊢ ran ( 1st ‘ 𝑅 ) = ran ( 1st ‘ 𝑅 )
4 2 3 idlss ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) → 𝑖 ⊆ ran ( 1st ‘ 𝑅 ) )
5 4 ex ⊢ ( 𝑅 ∈ RingOps → ( 𝑖 ∈ ( Idl ‘ 𝑅 ) → 𝑖 ⊆ ran ( 1st ‘ 𝑅 ) ) )
6 5 ralimdv ⊢ ( 𝑅 ∈ RingOps → ( ∀ 𝑖 ∈ 𝐶 𝑖 ∈ ( Idl ‘ 𝑅 ) → ∀ 𝑖 ∈ 𝐶 𝑖 ⊆ ran ( 1st ‘ 𝑅 ) ) )
7 6 imp ⊢ ( ( 𝑅 ∈ RingOps ∧ ∀ 𝑖 ∈ 𝐶 𝑖 ∈ ( Idl ‘ 𝑅 ) ) → ∀ 𝑖 ∈ 𝐶 𝑖 ⊆ ran ( 1st ‘ 𝑅 ) )
8 1 7 sylan2b ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ∀ 𝑖 ∈ 𝐶 𝑖 ⊆ ran ( 1st ‘ 𝑅 ) )
9 unissb ⊢ ( ∪ 𝐶 ⊆ ran ( 1st ‘ 𝑅 ) ↔ ∀ 𝑖 ∈ 𝐶 𝑖 ⊆ ran ( 1st ‘ 𝑅 ) )
10 8 9 sylibr ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ∪ 𝐶 ⊆ ran ( 1st ‘ 𝑅 ) )
11 10 3ad2antr2 ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) → ∪ 𝐶 ⊆ ran ( 1st ‘ 𝑅 ) )
12 eqid ⊢ ( GId ‘ ( 1st ‘ 𝑅 ) ) = ( GId ‘ ( 1st ‘ 𝑅 ) )
13 2 12 idl0cl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) → ( GId ‘ ( 1st ‘ 𝑅 ) ) ∈ 𝑖 )
14 13 ex ⊢ ( 𝑅 ∈ RingOps → ( 𝑖 ∈ ( Idl ‘ 𝑅 ) → ( GId ‘ ( 1st ‘ 𝑅 ) ) ∈ 𝑖 ) )
15 14 ralimdv ⊢ ( 𝑅 ∈ RingOps → ( ∀ 𝑖 ∈ 𝐶 𝑖 ∈ ( Idl ‘ 𝑅 ) → ∀ 𝑖 ∈ 𝐶 ( GId ‘ ( 1st ‘ 𝑅 ) ) ∈ 𝑖 ) )
16 15 imp ⊢ ( ( 𝑅 ∈ RingOps ∧ ∀ 𝑖 ∈ 𝐶 𝑖 ∈ ( Idl ‘ 𝑅 ) ) → ∀ 𝑖 ∈ 𝐶 ( GId ‘ ( 1st ‘ 𝑅 ) ) ∈ 𝑖 )
17 1 16 sylan2b ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ∀ 𝑖 ∈ 𝐶 ( GId ‘ ( 1st ‘ 𝑅 ) ) ∈ 𝑖 )
18 r19.2z ⊢ ( ( 𝐶 ≠ ∅ ∧ ∀ 𝑖 ∈ 𝐶 ( GId ‘ ( 1st ‘ 𝑅 ) ) ∈ 𝑖 ) → ∃ 𝑖 ∈ 𝐶 ( GId ‘ ( 1st ‘ 𝑅 ) ) ∈ 𝑖 )
19 17 18 sylan2 ⊢ ( ( 𝐶 ≠ ∅ ∧ ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ) → ∃ 𝑖 ∈ 𝐶 ( GId ‘ ( 1st ‘ 𝑅 ) ) ∈ 𝑖 )
20 19 an12s ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ) → ∃ 𝑖 ∈ 𝐶 ( GId ‘ ( 1st ‘ 𝑅 ) ) ∈ 𝑖 )
21 eluni2 ⊢ ( ( GId ‘ ( 1st ‘ 𝑅 ) ) ∈ ∪ 𝐶 ↔ ∃ 𝑖 ∈ 𝐶 ( GId ‘ ( 1st ‘ 𝑅 ) ) ∈ 𝑖 )
22 20 21 sylibr ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ) → ( GId ‘ ( 1st ‘ 𝑅 ) ) ∈ ∪ 𝐶 )
23 22 3adantr3 ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) → ( GId ‘ ( 1st ‘ 𝑅 ) ) ∈ ∪ 𝐶 )
24 eluni2 ⊢ ( 𝑥 ∈ ∪ 𝐶 ↔ ∃ 𝑘 ∈ 𝐶 𝑥 ∈ 𝑘 )
25 sseq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 ⊆ 𝑗 ↔ 𝑘 ⊆ 𝑗 ) )
26 sseq2 ⊢ ( 𝑖 = 𝑘 → ( 𝑗 ⊆ 𝑖 ↔ 𝑗 ⊆ 𝑘 ) )
27 25 26 orbi12d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ↔ ( 𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘 ) ) )
28 27 ralbidv ⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ↔ ∀ 𝑗 ∈ 𝐶 ( 𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘 ) ) )
29 28 rspcv ⊢ ( 𝑘 ∈ 𝐶 → ( ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) → ∀ 𝑗 ∈ 𝐶 ( 𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘 ) ) )
30 29 adantr ⊢ ( ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) → ( ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) → ∀ 𝑗 ∈ 𝐶 ( 𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘 ) ) )
31 30 ad2antlr ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ( ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) → ∀ 𝑗 ∈ 𝐶 ( 𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘 ) ) )
32 31 imp ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) → ∀ 𝑗 ∈ 𝐶 ( 𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘 ) )
33 eluni2 ⊢ ( 𝑦 ∈ ∪ 𝐶 ↔ ∃ 𝑖 ∈ 𝐶 𝑦 ∈ 𝑖 )
34 sseq2 ⊢ ( 𝑗 = 𝑖 → ( 𝑘 ⊆ 𝑗 ↔ 𝑘 ⊆ 𝑖 ) )
35 sseq1 ⊢ ( 𝑗 = 𝑖 → ( 𝑗 ⊆ 𝑘 ↔ 𝑖 ⊆ 𝑘 ) )
36 34 35 orbi12d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘 ) ↔ ( 𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘 ) ) )
37 36 rspcv ⊢ ( 𝑖 ∈ 𝐶 → ( ∀ 𝑗 ∈ 𝐶 ( 𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘 ) → ( 𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘 ) ) )
38 37 ad2antrl ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖 ) ) → ( ∀ 𝑗 ∈ 𝐶 ( 𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘 ) → ( 𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘 ) ) )
39 38 imp ⊢ ( ( ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖 ) ) ∧ ∀ 𝑗 ∈ 𝐶 ( 𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘 ) ) → ( 𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘 ) )
40 ssel2 ⊢ ( ( 𝑘 ⊆ 𝑖 ∧ 𝑥 ∈ 𝑘 ) → 𝑥 ∈ 𝑖 )
41 40 ancoms ⊢ ( ( 𝑥 ∈ 𝑘 ∧ 𝑘 ⊆ 𝑖 ) → 𝑥 ∈ 𝑖 )
42 41 adantll ⊢ ( ( ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ 𝑘 ⊆ 𝑖 ) → 𝑥 ∈ 𝑖 )
43 ssel2 ⊢ ( ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ 𝑖 ∈ 𝐶 ) → 𝑖 ∈ ( Idl ‘ 𝑅 ) )
44 2 idladdcl ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖 ) ) → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ 𝑖 )
45 44 ancom2s ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑦 ∈ 𝑖 ∧ 𝑥 ∈ 𝑖 ) ) → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ 𝑖 )
46 45 expr ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝑦 ∈ 𝑖 ) → ( 𝑥 ∈ 𝑖 → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ 𝑖 ) )
47 46 an32s ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑖 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝑥 ∈ 𝑖 → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ 𝑖 ) )
48 43 47 sylan2 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑦 ∈ 𝑖 ) ∧ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ 𝑖 ∈ 𝐶 ) ) → ( 𝑥 ∈ 𝑖 → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ 𝑖 ) )
49 48 an42s ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖 ) ) → ( 𝑥 ∈ 𝑖 → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ 𝑖 ) )
50 49 anasss ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ ( 𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖 ) ) ) → ( 𝑥 ∈ 𝑖 → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ 𝑖 ) )
51 50 imp ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ ( 𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖 ) ) ) ∧ 𝑥 ∈ 𝑖 ) → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ 𝑖 )
52 simprl ⊢ ( ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ ( 𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖 ) ) → 𝑖 ∈ 𝐶 )
53 52 ad2antlr ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ ( 𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖 ) ) ) ∧ 𝑥 ∈ 𝑖 ) → 𝑖 ∈ 𝐶 )
54 elunii ⊢ ( ( ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ 𝑖 ∧ 𝑖 ∈ 𝐶 ) → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
55 51 53 54 syl2anc ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ ( 𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖 ) ) ) ∧ 𝑥 ∈ 𝑖 ) → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
56 42 55 sylan2 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ ( 𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖 ) ) ) ∧ ( ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ∧ 𝑘 ⊆ 𝑖 ) ) → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
57 56 expr ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ ( 𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖 ) ) ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) → ( 𝑘 ⊆ 𝑖 → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ) )
58 57 an32s ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ ( 𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖 ) ) ) → ( 𝑘 ⊆ 𝑖 → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ) )
59 58 anassrs ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖 ) ) → ( 𝑘 ⊆ 𝑖 → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ) )
60 59 imp ⊢ ( ( ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖 ) ) ∧ 𝑘 ⊆ 𝑖 ) → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
61 ssel2 ⊢ ( ( 𝑖 ⊆ 𝑘 ∧ 𝑦 ∈ 𝑖 ) → 𝑦 ∈ 𝑘 )
62 61 ancoms ⊢ ( ( 𝑦 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑘 ) → 𝑦 ∈ 𝑘 )
63 62 adantll ⊢ ( ( ( 𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑖 ⊆ 𝑘 ) → 𝑦 ∈ 𝑘 )
64 ssel2 ⊢ ( ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ 𝑘 ∈ 𝐶 ) → 𝑘 ∈ ( Idl ‘ 𝑅 ) )
65 2 idladdcl ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑘 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑘 ) ) → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ 𝑘 )
66 65 expr ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑘 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝑘 ) → ( 𝑦 ∈ 𝑘 → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ 𝑘 ) )
67 66 an32s ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘 ) ∧ 𝑘 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝑦 ∈ 𝑘 → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ 𝑘 ) )
68 64 67 sylan2 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ 𝑘 ∈ 𝐶 ) ) → ( 𝑦 ∈ 𝑘 → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ 𝑘 ) )
69 68 an42s ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) → ( 𝑦 ∈ 𝑘 → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ 𝑘 ) )
70 69 an32s ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ( 𝑦 ∈ 𝑘 → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ 𝑘 ) )
71 70 imp ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ 𝑦 ∈ 𝑘 ) → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ 𝑘 )
72 simprl ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) → 𝑘 ∈ 𝐶 )
73 72 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ 𝑦 ∈ 𝑘 ) → 𝑘 ∈ 𝐶 )
74 elunii ⊢ ( ( ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ 𝑘 ∧ 𝑘 ∈ 𝐶 ) → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
75 71 73 74 syl2anc ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ 𝑦 ∈ 𝑘 ) → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
76 63 75 sylan2 ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ( ( 𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑖 ⊆ 𝑘 ) ) → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
77 76 anassrs ⊢ ( ( ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖 ) ) ∧ 𝑖 ⊆ 𝑘 ) → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
78 60 77 jaodan ⊢ ( ( ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖 ) ) ∧ ( 𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘 ) ) → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
79 39 78 syldan ⊢ ( ( ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖 ) ) ∧ ∀ 𝑗 ∈ 𝐶 ( 𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘 ) ) → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
80 79 an32s ⊢ ( ( ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ∀ 𝑗 ∈ 𝐶 ( 𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘 ) ) ∧ ( 𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖 ) ) → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
81 80 rexlimdvaa ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ∀ 𝑗 ∈ 𝐶 ( 𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘 ) ) → ( ∃ 𝑖 ∈ 𝐶 𝑦 ∈ 𝑖 → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ) )
82 33 81 biimtrid ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ∀ 𝑗 ∈ 𝐶 ( 𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘 ) ) → ( 𝑦 ∈ ∪ 𝐶 → ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ) )
83 82 ralrimiv ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ∀ 𝑗 ∈ 𝐶 ( 𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘 ) ) → ∀ 𝑦 ∈ ∪ 𝐶 ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
84 32 83 syldan ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) → ∀ 𝑦 ∈ ∪ 𝐶 ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
85 84 anasss ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) → ∀ 𝑦 ∈ ∪ 𝐶 ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
86 85 3adantr1 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) → ∀ 𝑦 ∈ ∪ 𝐶 ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
87 86 an32s ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) → ∀ 𝑦 ∈ ∪ 𝐶 ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 )
88 eqid ⊢ ( 2nd ‘ 𝑅 ) = ( 2nd ‘ 𝑅 )
89 2 88 3 idllmulcl ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑘 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑧 ∈ ran ( 1st ‘ 𝑅 ) ) ) → ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 )
90 89 exp43 ⊢ ( 𝑅 ∈ RingOps → ( 𝑘 ∈ ( Idl ‘ 𝑅 ) → ( 𝑥 ∈ 𝑘 → ( 𝑧 ∈ ran ( 1st ‘ 𝑅 ) → ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ) ) ) )
91 90 com23 ⊢ ( 𝑅 ∈ RingOps → ( 𝑥 ∈ 𝑘 → ( 𝑘 ∈ ( Idl ‘ 𝑅 ) → ( 𝑧 ∈ ran ( 1st ‘ 𝑅 ) → ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ) ) ) )
92 91 imp41 ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘 ) ∧ 𝑘 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝑧 ∈ ran ( 1st ‘ 𝑅 ) ) → ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 )
93 64 92 sylanl2 ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ 𝑘 ∈ 𝐶 ) ) ∧ 𝑧 ∈ ran ( 1st ‘ 𝑅 ) ) → ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 )
94 simplrr ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ 𝑘 ∈ 𝐶 ) ) ∧ 𝑧 ∈ ran ( 1st ‘ 𝑅 ) ) → 𝑘 ∈ 𝐶 )
95 elunii ⊢ ( ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑘 ∧ 𝑘 ∈ 𝐶 ) → ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ ∪ 𝐶 )
96 93 94 95 syl2anc ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ 𝑘 ∈ 𝐶 ) ) ∧ 𝑧 ∈ ran ( 1st ‘ 𝑅 ) ) → ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ ∪ 𝐶 )
97 2 88 3 idlrmulcl ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑘 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝑘 ∧ 𝑧 ∈ ran ( 1st ‘ 𝑅 ) ) ) → ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑘 )
98 97 exp43 ⊢ ( 𝑅 ∈ RingOps → ( 𝑘 ∈ ( Idl ‘ 𝑅 ) → ( 𝑥 ∈ 𝑘 → ( 𝑧 ∈ ran ( 1st ‘ 𝑅 ) → ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑘 ) ) ) )
99 98 com23 ⊢ ( 𝑅 ∈ RingOps → ( 𝑥 ∈ 𝑘 → ( 𝑘 ∈ ( Idl ‘ 𝑅 ) → ( 𝑧 ∈ ran ( 1st ‘ 𝑅 ) → ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑘 ) ) ) )
100 99 imp41 ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘 ) ∧ 𝑘 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝑧 ∈ ran ( 1st ‘ 𝑅 ) ) → ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑘 )
101 64 100 sylanl2 ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ 𝑘 ∈ 𝐶 ) ) ∧ 𝑧 ∈ ran ( 1st ‘ 𝑅 ) ) → ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑘 )
102 elunii ⊢ ( ( ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑘 ∧ 𝑘 ∈ 𝐶 ) → ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ ∪ 𝐶 )
103 101 94 102 syl2anc ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ 𝑘 ∈ 𝐶 ) ) ∧ 𝑧 ∈ ran ( 1st ‘ 𝑅 ) ) → ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ ∪ 𝐶 )
104 96 103 jca ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ 𝑘 ∈ 𝐶 ) ) ∧ 𝑧 ∈ ran ( 1st ‘ 𝑅 ) ) → ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ ∪ 𝐶 ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ ∪ 𝐶 ) )
105 104 ralrimiva ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘 ) ∧ ( 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ 𝑘 ∈ 𝐶 ) ) → ∀ 𝑧 ∈ ran ( 1st ‘ 𝑅 ) ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ ∪ 𝐶 ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ ∪ 𝐶 ) )
106 105 an42s ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) → ∀ 𝑧 ∈ ran ( 1st ‘ 𝑅 ) ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ ∪ 𝐶 ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ ∪ 𝐶 ) )
107 106 an32s ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ) → ∀ 𝑧 ∈ ran ( 1st ‘ 𝑅 ) ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ ∪ 𝐶 ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ ∪ 𝐶 ) )
108 107 3ad2antr2 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) → ∀ 𝑧 ∈ ran ( 1st ‘ 𝑅 ) ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ ∪ 𝐶 ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ ∪ 𝐶 ) )
109 108 an32s ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) → ∀ 𝑧 ∈ ran ( 1st ‘ 𝑅 ) ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ ∪ 𝐶 ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ ∪ 𝐶 ) )
110 87 109 jca ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘 ) ) → ( ∀ 𝑦 ∈ ∪ 𝐶 ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ∧ ∀ 𝑧 ∈ ran ( 1st ‘ 𝑅 ) ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ ∪ 𝐶 ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ ∪ 𝐶 ) ) )
111 110 rexlimdvaa ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) → ( ∃ 𝑘 ∈ 𝐶 𝑥 ∈ 𝑘 → ( ∀ 𝑦 ∈ ∪ 𝐶 ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ∧ ∀ 𝑧 ∈ ran ( 1st ‘ 𝑅 ) ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ ∪ 𝐶 ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ ∪ 𝐶 ) ) ) )
112 24 111 biimtrid ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) → ( 𝑥 ∈ ∪ 𝐶 → ( ∀ 𝑦 ∈ ∪ 𝐶 ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ∧ ∀ 𝑧 ∈ ran ( 1st ‘ 𝑅 ) ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ ∪ 𝐶 ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ ∪ 𝐶 ) ) ) )
113 112 ralrimiv ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) → ∀ 𝑥 ∈ ∪ 𝐶 ( ∀ 𝑦 ∈ ∪ 𝐶 ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ∧ ∀ 𝑧 ∈ ran ( 1st ‘ 𝑅 ) ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ ∪ 𝐶 ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ ∪ 𝐶 ) ) )
114 2 88 3 12 isidl ⊢ ( 𝑅 ∈ RingOps → ( ∪ 𝐶 ∈ ( Idl ‘ 𝑅 ) ↔ ( ∪ 𝐶 ⊆ ran ( 1st ‘ 𝑅 ) ∧ ( GId ‘ ( 1st ‘ 𝑅 ) ) ∈ ∪ 𝐶 ∧ ∀ 𝑥 ∈ ∪ 𝐶 ( ∀ 𝑦 ∈ ∪ 𝐶 ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ∧ ∀ 𝑧 ∈ ran ( 1st ‘ 𝑅 ) ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ ∪ 𝐶 ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ ∪ 𝐶 ) ) ) ) )
115 114 adantr ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) → ( ∪ 𝐶 ∈ ( Idl ‘ 𝑅 ) ↔ ( ∪ 𝐶 ⊆ ran ( 1st ‘ 𝑅 ) ∧ ( GId ‘ ( 1st ‘ 𝑅 ) ) ∈ ∪ 𝐶 ∧ ∀ 𝑥 ∈ ∪ 𝐶 ( ∀ 𝑦 ∈ ∪ 𝐶 ( 𝑥 ( 1st ‘ 𝑅 ) 𝑦 ) ∈ ∪ 𝐶 ∧ ∀ 𝑧 ∈ ran ( 1st ‘ 𝑅 ) ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ ∪ 𝐶 ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ ∪ 𝐶 ) ) ) ) )
116 11 23 113 115 mpbir3and ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( Idl ‘ 𝑅 ) ∧ ∀ 𝑖 ∈ 𝐶 ∀ 𝑗 ∈ 𝐶 ( 𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖 ) ) ) → ∪ 𝐶 ∈ ( Idl ‘ 𝑅 ) )