Metamath Proof Explorer

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 = r ∈ RingOps ⟼ i ∈ Idl ⁡ r | i ≠ ran ⁡ 1 st ⁡ r ∧ ∀ a ∈ Idl ⁡ r ∀ b ∈ Idl ⁡ r ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ r y ∈ i → a ⊆ i ∨ b ⊆ i

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpridl class PrIdl
1 vr setvar r
2 crngo class RingOps
3 vi setvar i
4 cidl class Idl
5 1 cv setvar r
6 5 4 cfv class Idl ⁡ r
7 3 cv setvar i
8 c1st class 1 st
9 5 8 cfv class 1 st ⁡ r
10 9 crn class ran ⁡ 1 st ⁡ r
11 7 10 wne wff i ≠ ran ⁡ 1 st ⁡ r
12 va setvar a
13 vb setvar b
14 vx setvar x
15 12 cv setvar a
16 vy setvar y
17 13 cv setvar b
18 14 cv setvar x
19 c2nd class 2 nd
20 5 19 cfv class 2 nd ⁡ r
21 16 cv setvar y
22 18 21 20 co class x 2 nd ⁡ r y
23 22 7 wcel wff x 2 nd ⁡ r y ∈ i
24 23 16 17 wral wff ∀ y ∈ b x 2 nd ⁡ r y ∈ i
25 24 14 15 wral wff ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ r y ∈ i
26 15 7 wss wff a ⊆ i
27 17 7 wss wff b ⊆ i
28 26 27 wo wff a ⊆ i ∨ b ⊆ i
29 25 28 wi wff ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ r y ∈ i → a ⊆ i ∨ b ⊆ i
30 29 13 6 wral wff ∀ b ∈ Idl ⁡ r ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ r y ∈ i → a ⊆ i ∨ b ⊆ i
31 30 12 6 wral wff ∀ a ∈ Idl ⁡ r ∀ b ∈ Idl ⁡ r ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ r y ∈ i → a ⊆ i ∨ b ⊆ i
32 11 31 wa wff i ≠ ran ⁡ 1 st ⁡ r ∧ ∀ a ∈ Idl ⁡ r ∀ b ∈ Idl ⁡ r ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ r y ∈ i → a ⊆ i ∨ b ⊆ i
33 32 3 6 crab class i ∈ Idl ⁡ r | i ≠ ran ⁡ 1 st ⁡ r ∧ ∀ a ∈ Idl ⁡ r ∀ b ∈ Idl ⁡ r ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ r y ∈ i → a ⊆ i ∨ b ⊆ i
34 1 2 33 cmpt class r ∈ RingOps ⟼ i ∈ Idl ⁡ r | i ≠ ran ⁡ 1 st ⁡ r ∧ ∀ a ∈ Idl ⁡ r ∀ b ∈ Idl ⁡ r ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ r y ∈ i → a ⊆ i ∨ b ⊆ i
35 0 34 wceq wff PrIdl = r ∈ RingOps ⟼ i ∈ Idl ⁡ r | i ≠ ran ⁡ 1 st ⁡ r ∧ ∀ a ∈ Idl ⁡ r ∀ b ∈ Idl ⁡ r ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ r y ∈ i → a ⊆ i ∨ b ⊆ i