Metamath Proof Explorer

Theorem intidl

Description: The intersection of a nonempty collection of ideals is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Assertion intidl 
|- ( ( R e. RingOps /\ C =/= (/) /\ C C_ ( Idl ` R ) ) -> |^| C e. ( Idl ` R ) )

Proof

Step Hyp Ref Expression
1 intssuni 
 |-  ( C =/= (/) -> |^| C C_ U. C )
2 1 3ad2ant2 
 |-  ( ( R e. RingOps /\ C =/= (/) /\ C C_ ( Idl ` R ) ) -> |^| C C_ U. C )
3 ssel2 
 |-  ( ( C C_ ( Idl ` R ) /\ i e. C ) -> i e. ( Idl ` R ) )
4 eqid 
 |-  ( 1st ` R ) = ( 1st ` R )
5 eqid 
 |-  ran ( 1st ` R ) = ran ( 1st ` R )
6 4 5 idlss 
 |-  ( ( R e. RingOps /\ i e. ( Idl ` R ) ) -> i C_ ran ( 1st ` R ) )
7 3 6 sylan2 
 |-  ( ( R e. RingOps /\ ( C C_ ( Idl ` R ) /\ i e. C ) ) -> i C_ ran ( 1st ` R ) )
8 7 anassrs 
 |-  ( ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) /\ i e. C ) -> i C_ ran ( 1st ` R ) )
9 8 ralrimiva 
 |-  ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) -> A. i e. C i C_ ran ( 1st ` R ) )
10 9 3adant2 
 |-  ( ( R e. RingOps /\ C =/= (/) /\ C C_ ( Idl ` R ) ) -> A. i e. C i C_ ran ( 1st ` R ) )
11 unissb 
 |-  ( U. C C_ ran ( 1st ` R ) <-> A. i e. C i C_ ran ( 1st ` R ) )
12 10 11 sylibr 
 |-  ( ( R e. RingOps /\ C =/= (/) /\ C C_ ( Idl ` R ) ) -> U. C C_ ran ( 1st ` R ) )
13 2 12 sstrd 
 |-  ( ( R e. RingOps /\ C =/= (/) /\ C C_ ( Idl ` R ) ) -> |^| C C_ ran ( 1st ` R ) )
14 eqid 
 |-  ( GId ` ( 1st ` R ) ) = ( GId ` ( 1st ` R ) )
15 4 14 idl0cl 
 |-  ( ( R e. RingOps /\ i e. ( Idl ` R ) ) -> ( GId ` ( 1st ` R ) ) e. i )
16 3 15 sylan2 
 |-  ( ( R e. RingOps /\ ( C C_ ( Idl ` R ) /\ i e. C ) ) -> ( GId ` ( 1st ` R ) ) e. i )
17 16 anassrs 
 |-  ( ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) /\ i e. C ) -> ( GId ` ( 1st ` R ) ) e. i )
18 17 ralrimiva 
 |-  ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) -> A. i e. C ( GId ` ( 1st ` R ) ) e. i )
19 fvex 
 |-  ( GId ` ( 1st ` R ) ) e. _V
20 19 elint2 
 |-  ( ( GId ` ( 1st ` R ) ) e. |^| C <-> A. i e. C ( GId ` ( 1st ` R ) ) e. i )
21 18 20 sylibr 
 |-  ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) -> ( GId ` ( 1st ` R ) ) e. |^| C )
22 21 3adant2 
 |-  ( ( R e. RingOps /\ C =/= (/) /\ C C_ ( Idl ` R ) ) -> ( GId ` ( 1st ` R ) ) e. |^| C )
23 vex 
 |-  x e. _V
24 23 elint2 
 |-  ( x e. |^| C <-> A. i e. C x e. i )
25 vex 
 |-  y e. _V
26 25 elint2 
 |-  ( y e. |^| C <-> A. i e. C y e. i )
27 r19.26 
 |-  ( A. i e. C ( x e. i /\ y e. i ) <-> ( A. i e. C x e. i /\ A. i e. C y e. i ) )
28 4 idladdcl 
 |-  ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ ( x e. i /\ y e. i ) ) -> ( x ( 1st ` R ) y ) e. i )
29 28 ex 
 |-  ( ( R e. RingOps /\ i e. ( Idl ` R ) ) -> ( ( x e. i /\ y e. i ) -> ( x ( 1st ` R ) y ) e. i ) )
30 3 29 sylan2 
 |-  ( ( R e. RingOps /\ ( C C_ ( Idl ` R ) /\ i e. C ) ) -> ( ( x e. i /\ y e. i ) -> ( x ( 1st ` R ) y ) e. i ) )
31 30 anassrs 
 |-  ( ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) /\ i e. C ) -> ( ( x e. i /\ y e. i ) -> ( x ( 1st ` R ) y ) e. i ) )
32 31 ralimdva 
 |-  ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) -> ( A. i e. C ( x e. i /\ y e. i ) -> A. i e. C ( x ( 1st ` R ) y ) e. i ) )
33 ovex 
 |-  ( x ( 1st ` R ) y ) e. _V
34 33 elint2 
 |-  ( ( x ( 1st ` R ) y ) e. |^| C <-> A. i e. C ( x ( 1st ` R ) y ) e. i )
35 32 34 imbitrrdi 
 |-  ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) -> ( A. i e. C ( x e. i /\ y e. i ) -> ( x ( 1st ` R ) y ) e. |^| C ) )
36 27 35 biimtrrid 
 |-  ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) -> ( ( A. i e. C x e. i /\ A. i e. C y e. i ) -> ( x ( 1st ` R ) y ) e. |^| C ) )
37 36 expdimp 
 |-  ( ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) /\ A. i e. C x e. i ) -> ( A. i e. C y e. i -> ( x ( 1st ` R ) y ) e. |^| C ) )
38 26 37 biimtrid 
 |-  ( ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) /\ A. i e. C x e. i ) -> ( y e. |^| C -> ( x ( 1st ` R ) y ) e. |^| C ) )
39 38 ralrimiv 
 |-  ( ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) /\ A. i e. C x e. i ) -> A. y e. |^| C ( x ( 1st ` R ) y ) e. |^| C )
40 eqid 
 |-  ( 2nd ` R ) = ( 2nd ` R )
41 4 40 5 idllmulcl 
 |-  ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ ( x e. i /\ z e. ran ( 1st ` R ) ) ) -> ( z ( 2nd ` R ) x ) e. i )
42 41 anass1rs 
 |-  ( ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ z e. ran ( 1st ` R ) ) /\ x e. i ) -> ( z ( 2nd ` R ) x ) e. i )
43 42 ex 
 |-  ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ z e. ran ( 1st ` R ) ) -> ( x e. i -> ( z ( 2nd ` R ) x ) e. i ) )
44 43 an32s 
 |-  ( ( ( R e. RingOps /\ z e. ran ( 1st ` R ) ) /\ i e. ( Idl ` R ) ) -> ( x e. i -> ( z ( 2nd ` R ) x ) e. i ) )
45 3 44 sylan2 
 |-  ( ( ( R e. RingOps /\ z e. ran ( 1st ` R ) ) /\ ( C C_ ( Idl ` R ) /\ i e. C ) ) -> ( x e. i -> ( z ( 2nd ` R ) x ) e. i ) )
46 45 an4s 
 |-  ( ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) /\ ( z e. ran ( 1st ` R ) /\ i e. C ) ) -> ( x e. i -> ( z ( 2nd ` R ) x ) e. i ) )
47 46 anassrs 
 |-  ( ( ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) /\ z e. ran ( 1st ` R ) ) /\ i e. C ) -> ( x e. i -> ( z ( 2nd ` R ) x ) e. i ) )
48 47 ralimdva 
 |-  ( ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) /\ z e. ran ( 1st ` R ) ) -> ( A. i e. C x e. i -> A. i e. C ( z ( 2nd ` R ) x ) e. i ) )
49 48 imp 
 |-  ( ( ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) /\ z e. ran ( 1st ` R ) ) /\ A. i e. C x e. i ) -> A. i e. C ( z ( 2nd ` R ) x ) e. i )
50 ovex 
 |-  ( z ( 2nd ` R ) x ) e. _V
51 50 elint2 
 |-  ( ( z ( 2nd ` R ) x ) e. |^| C <-> A. i e. C ( z ( 2nd ` R ) x ) e. i )
52 49 51 sylibr 
 |-  ( ( ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) /\ z e. ran ( 1st ` R ) ) /\ A. i e. C x e. i ) -> ( z ( 2nd ` R ) x ) e. |^| C )
53 4 40 5 idlrmulcl 
 |-  ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ ( x e. i /\ z e. ran ( 1st ` R ) ) ) -> ( x ( 2nd ` R ) z ) e. i )
54 53 anass1rs 
 |-  ( ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ z e. ran ( 1st ` R ) ) /\ x e. i ) -> ( x ( 2nd ` R ) z ) e. i )
55 54 ex 
 |-  ( ( ( R e. RingOps /\ i e. ( Idl ` R ) ) /\ z e. ran ( 1st ` R ) ) -> ( x e. i -> ( x ( 2nd ` R ) z ) e. i ) )
56 55 an32s 
 |-  ( ( ( R e. RingOps /\ z e. ran ( 1st ` R ) ) /\ i e. ( Idl ` R ) ) -> ( x e. i -> ( x ( 2nd ` R ) z ) e. i ) )
57 3 56 sylan2 
 |-  ( ( ( R e. RingOps /\ z e. ran ( 1st ` R ) ) /\ ( C C_ ( Idl ` R ) /\ i e. C ) ) -> ( x e. i -> ( x ( 2nd ` R ) z ) e. i ) )
58 57 an4s 
 |-  ( ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) /\ ( z e. ran ( 1st ` R ) /\ i e. C ) ) -> ( x e. i -> ( x ( 2nd ` R ) z ) e. i ) )
59 58 anassrs 
 |-  ( ( ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) /\ z e. ran ( 1st ` R ) ) /\ i e. C ) -> ( x e. i -> ( x ( 2nd ` R ) z ) e. i ) )
60 59 ralimdva 
 |-  ( ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) /\ z e. ran ( 1st ` R ) ) -> ( A. i e. C x e. i -> A. i e. C ( x ( 2nd ` R ) z ) e. i ) )
61 60 imp 
 |-  ( ( ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) /\ z e. ran ( 1st ` R ) ) /\ A. i e. C x e. i ) -> A. i e. C ( x ( 2nd ` R ) z ) e. i )
62 ovex 
 |-  ( x ( 2nd ` R ) z ) e. _V
63 62 elint2 
 |-  ( ( x ( 2nd ` R ) z ) e. |^| C <-> A. i e. C ( x ( 2nd ` R ) z ) e. i )
64 61 63 sylibr 
 |-  ( ( ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) /\ z e. ran ( 1st ` R ) ) /\ A. i e. C x e. i ) -> ( x ( 2nd ` R ) z ) e. |^| C )
65 52 64 jca 
 |-  ( ( ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) /\ z e. ran ( 1st ` R ) ) /\ A. i e. C x e. i ) -> ( ( z ( 2nd ` R ) x ) e. |^| C /\ ( x ( 2nd ` R ) z ) e. |^| C ) )
66 65 an32s 
 |-  ( ( ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) /\ A. i e. C x e. i ) /\ z e. ran ( 1st ` R ) ) -> ( ( z ( 2nd ` R ) x ) e. |^| C /\ ( x ( 2nd ` R ) z ) e. |^| C ) )
67 66 ralrimiva 
 |-  ( ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) /\ A. i e. C x e. i ) -> A. z e. ran ( 1st ` R ) ( ( z ( 2nd ` R ) x ) e. |^| C /\ ( x ( 2nd ` R ) z ) e. |^| C ) )
68 39 67 jca 
 |-  ( ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) /\ A. i e. C x e. i ) -> ( A. y e. |^| C ( x ( 1st ` R ) y ) e. |^| C /\ A. z e. ran ( 1st ` R ) ( ( z ( 2nd ` R ) x ) e. |^| C /\ ( x ( 2nd ` R ) z ) e. |^| C ) ) )
69 68 ex 
 |-  ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) -> ( A. i e. C x e. i -> ( A. y e. |^| C ( x ( 1st ` R ) y ) e. |^| C /\ A. z e. ran ( 1st ` R ) ( ( z ( 2nd ` R ) x ) e. |^| C /\ ( x ( 2nd ` R ) z ) e. |^| C ) ) ) )
70 24 69 biimtrid 
 |-  ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) -> ( x e. |^| C -> ( A. y e. |^| C ( x ( 1st ` R ) y ) e. |^| C /\ A. z e. ran ( 1st ` R ) ( ( z ( 2nd ` R ) x ) e. |^| C /\ ( x ( 2nd ` R ) z ) e. |^| C ) ) ) )
71 70 ralrimiv 
 |-  ( ( R e. RingOps /\ C C_ ( Idl ` R ) ) -> A. x e. |^| C ( A. y e. |^| C ( x ( 1st ` R ) y ) e. |^| C /\ A. z e. ran ( 1st ` R ) ( ( z ( 2nd ` R ) x ) e. |^| C /\ ( x ( 2nd ` R ) z ) e. |^| C ) ) )
72 71 3adant2 
 |-  ( ( R e. RingOps /\ C =/= (/) /\ C C_ ( Idl ` R ) ) -> A. x e. |^| C ( A. y e. |^| C ( x ( 1st ` R ) y ) e. |^| C /\ A. z e. ran ( 1st ` R ) ( ( z ( 2nd ` R ) x ) e. |^| C /\ ( x ( 2nd ` R ) z ) e. |^| C ) ) )
73 4 40 5 14 isidl 
 |-  ( R e. RingOps -> ( |^| C e. ( Idl ` R ) <-> ( |^| C C_ ran ( 1st ` R ) /\ ( GId ` ( 1st ` R ) ) e. |^| C /\ A. x e. |^| C ( A. y e. |^| C ( x ( 1st ` R ) y ) e. |^| C /\ A. z e. ran ( 1st ` R ) ( ( z ( 2nd ` R ) x ) e. |^| C /\ ( x ( 2nd ` R ) z ) e. |^| C ) ) ) ) )
74 73 3ad2ant1 
 |-  ( ( R e. RingOps /\ C =/= (/) /\ C C_ ( Idl ` R ) ) -> ( |^| C e. ( Idl ` R ) <-> ( |^| C C_ ran ( 1st ` R ) /\ ( GId ` ( 1st ` R ) ) e. |^| C /\ A. x e. |^| C ( A. y e. |^| C ( x ( 1st ` R ) y ) e. |^| C /\ A. z e. ran ( 1st ` R ) ( ( z ( 2nd ` R ) x ) e. |^| C /\ ( x ( 2nd ` R ) z ) e. |^| C ) ) ) ) )
75 13 22 72 74 mpbir3and 
 |-  ( ( R e. RingOps /\ C =/= (/) /\ C C_ ( Idl ` R ) ) -> |^| C e. ( Idl ` R ) )