Definition df-pridl 33810

Description: Define the class of prime ideals of a ring R. A proper ideal I of R is prime if whenever A B C_ I for ideals A and B, either A C_ I or B C_ I. The more familiar definition using elements rather than ideals is equivalent provided R is commutative; see ispridl2 33837 and ispridlc 33869. (Contributed by Jeff Madsen, 10-Jun-2010.)

Assertion

Ref	Expression
df-pridl	|- 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 ) ) ) } )

Distinct variable group:   i, r, a, b, x, y

Detailed syntax breakdown of Definition df-pridl

Step	Hyp	Ref	Expression
1		cpridl 33807	. 2 class PrIdl
2		vr	. . 3 setvar r
3		crngo 33693	. . 3 class RingOps
4		vi	. . . . . . 7 setvar i
5	4	cv 1482	. . . . . 6 class i
6	2	cv 1482	. . . . . . . 8 class r
7		c1st 7166	. . . . . . . 8 class 1st
8	6, 7	cfv 5888	. . . . . . 7 class ( 1st ` r )
9	8	crn 5115	. . . . . 6 class ran ( 1st ` r )
10	5, 9	wne 2794	. . . . 5 wff i =/= ran ( 1st ` r )
11		vx	. . . . . . . . . . . . 13 setvar x
12	11	cv 1482	. . . . . . . . . . . 12 class x
13		vy	. . . . . . . . . . . . 13 setvar y
14	13	cv 1482	. . . . . . . . . . . 12 class y
15		c2nd 7167	. . . . . . . . . . . . 13 class 2nd
16	6, 15	cfv 5888	. . . . . . . . . . . 12 class ( 2nd ` r )
17	12, 14, 16	co 6650	. . . . . . . . . . 11 class ( x ( 2nd ` r ) y )
18	17, 5	wcel 1990	. . . . . . . . . 10 wff ( x ( 2nd ` r ) y ) e. i
19		vb	. . . . . . . . . . 11 setvar b
20	19	cv 1482	. . . . . . . . . 10 class b
21	18, 13, 20	wral 2912	. . . . . . . . 9 wff A. y e. b ( x ( 2nd ` r ) y ) e. i
22		va	. . . . . . . . . 10 setvar a
23	22	cv 1482	. . . . . . . . 9 class a
24	21, 11, 23	wral 2912	. . . . . . . 8 wff A. x e. a A. y e. b ( x ( 2nd ` r ) y ) e. i
25	23, 5	wss 3574	. . . . . . . . 9 wff a C_ i
26	20, 5	wss 3574	. . . . . . . . 9 wff b C_ i
27	25, 26	wo 383	. . . . . . . 8 wff ( a C_ i \/ b C_ i )
28	24, 27	wi 4	. . . . . . 7 wff ( A. x e. a A. y e. b ( x ( 2nd ` r ) y ) e. i -> ( a C_ i \/ b C_ i ) )
29		cidl 33806	. . . . . . . 8 class Idl
30	6, 29	cfv 5888	. . . . . . 7 class ( Idl ` r )
31	28, 19, 30	wral 2912	. . . . . 6 wff 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	31, 22, 30	wral 2912	. . . . 5 wff 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	10, 32	wa 384	. . . 4 wff ( 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	33, 4, 30	crab 2916	. . 3 class { 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	2, 3, 34	cmpt 4729	. 2 class ( 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 ) ) ) } )
36	1, 35	wceq 1483	1 wff 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 ) ) ) } )

This definition is referenced by:  pridlval  33832