Step |
Hyp |
Ref |
Expression |
0 |
|
cpridl |
|- PrIdl |
1 |
|
vr |
|- r |
2 |
|
crngo |
|- RingOps |
3 |
|
vi |
|- i |
4 |
|
cidl |
|- Idl |
5 |
1
|
cv |
|- r |
6 |
5 4
|
cfv |
|- ( Idl ` r ) |
7 |
3
|
cv |
|- i |
8 |
|
c1st |
|- 1st |
9 |
5 8
|
cfv |
|- ( 1st ` r ) |
10 |
9
|
crn |
|- ran ( 1st ` r ) |
11 |
7 10
|
wne |
|- i =/= ran ( 1st ` r ) |
12 |
|
va |
|- a |
13 |
|
vb |
|- b |
14 |
|
vx |
|- x |
15 |
12
|
cv |
|- a |
16 |
|
vy |
|- y |
17 |
13
|
cv |
|- b |
18 |
14
|
cv |
|- x |
19 |
|
c2nd |
|- 2nd |
20 |
5 19
|
cfv |
|- ( 2nd ` r ) |
21 |
16
|
cv |
|- y |
22 |
18 21 20
|
co |
|- ( x ( 2nd ` r ) y ) |
23 |
22 7
|
wcel |
|- ( x ( 2nd ` r ) y ) e. i |
24 |
23 16 17
|
wral |
|- A. y e. b ( x ( 2nd ` r ) y ) e. i |
25 |
24 14 15
|
wral |
|- A. x e. a A. y e. b ( x ( 2nd ` r ) y ) e. i |
26 |
15 7
|
wss |
|- a C_ i |
27 |
17 7
|
wss |
|- b C_ i |
28 |
26 27
|
wo |
|- ( a C_ i \/ b C_ i ) |
29 |
25 28
|
wi |
|- ( A. x e. a A. y e. b ( x ( 2nd ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) |
30 |
29 13 6
|
wral |
|- A. b e. ( Idl ` r ) ( A. x e. a A. y e. b ( x ( 2nd ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) |
31 |
30 12 6
|
wral |
|- A. a e. ( Idl ` r ) A. b e. ( Idl ` r ) ( A. x e. a A. y e. b ( x ( 2nd ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) |
32 |
11 31
|
wa |
|- ( i =/= ran ( 1st ` r ) /\ A. a e. ( Idl ` r ) A. b e. ( Idl ` r ) ( A. x e. a A. y e. b ( x ( 2nd ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) ) |
33 |
32 3 6
|
crab |
|- { i e. ( Idl ` r ) | ( i =/= ran ( 1st ` r ) /\ A. a e. ( Idl ` r ) A. b e. ( Idl ` r ) ( A. x e. a A. y e. b ( x ( 2nd ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } |
34 |
1 2 33
|
cmpt |
|- ( r e. RingOps |-> { i e. ( Idl ` r ) | ( i =/= ran ( 1st ` r ) /\ A. a e. ( Idl ` r ) A. b e. ( Idl ` r ) ( A. x e. a A. y e. b ( x ( 2nd ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } ) |
35 |
0 34
|
wceq |
|- PrIdl = ( r e. RingOps |-> { i e. ( Idl ` r ) | ( i =/= ran ( 1st ` r ) /\ A. a e. ( Idl ` r ) A. b e. ( Idl ` r ) ( A. x e. a A. y e. b ( x ( 2nd ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } ) |