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

Proof

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