Definition df-pridl

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 and ispridlc . (Contributed by Jeff Madsen, 10-Jun-2010)

	Ref	Expression
Assertion	df-pridl	⊢ PrIdl = ( 𝑟 ∈ RingOps ↦ { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1st ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑟 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpridl	⊢ PrIdl
1		vr	⊢ 𝑟
2		crngo	⊢ RingOps
3		vi	⊢ 𝑖
4		cidl	⊢ Idl
5	1	cv	⊢ 𝑟
6	5 4	cfv	⊢ ( Idl ‘ 𝑟 )
7	3	cv	⊢ 𝑖
8		c1st	⊢ 1st
9	5 8	cfv	⊢ ( 1st ‘ 𝑟 )
10	9	crn	⊢ ran ( 1st ‘ 𝑟 )
11	7 10	wne	⊢ 𝑖 ≠ ran ( 1st ‘ 𝑟 )
12		va	⊢ 𝑎
13		vb	⊢ 𝑏
14		vx	⊢ 𝑥
15	12	cv	⊢ 𝑎
16		vy	⊢ 𝑦
17	13	cv	⊢ 𝑏
18	14	cv	⊢ 𝑥
19		c2nd	⊢ 2nd
20	5 19	cfv	⊢ ( 2nd ‘ 𝑟 )
21	16	cv	⊢ 𝑦
22	18 21 20	co	⊢ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 )
23	22 7	wcel	⊢ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖
24	23 16 17	wral	⊢ ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖
25	24 14 15	wral	⊢ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖
26	15 7	wss	⊢ 𝑎 ⊆ 𝑖
27	17 7	wss	⊢ 𝑏 ⊆ 𝑖
28	26 27	wo	⊢ ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 )
29	25 28	wi	⊢ ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) )
30	29 13 6	wral	⊢ ∀ 𝑏 ∈ ( Idl ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) )
31	30 12 6	wral	⊢ ∀ 𝑎 ∈ ( Idl ‘ 𝑟 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) )
32	11 31	wa	⊢ ( 𝑖 ≠ ran ( 1st ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑟 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) )
33	32 3 6	crab	⊢ { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1st ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑟 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) }
34	1 2 33	cmpt	⊢ ( 𝑟 ∈ RingOps ↦ { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1st ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑟 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) } )
35	0 34	wceq	⊢ PrIdl = ( 𝑟 ∈ RingOps ↦ { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1st ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑟 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) } )