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 
|- ( ( R e. Ring /\ ( C =/= (/) /\ C C_ ( LIdeal ` R ) /\ A. i e. C A. j e. C ( i C_ j \/ j C_ i ) ) ) -> U. C e. ( LIdeal ` R ) )

Proof

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