df-maxidl

Description: Define the class of maximal ideals of a ring R . A proper ideal is called maximal if it is maximal with respect to inclusion among proper ideals. (Contributed by Jeff Madsen, 5-Jan-2011)

		Ref	Expression
	Assertion	df-maxidl	⊢ MaxIdl = ( 𝑟 ∈ RingOps ↦ { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1^st ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ran ( 1^st ‘ 𝑟 ) ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmaxidl	⊢ MaxIdl
1		vr	⊢ 𝑟
2		crngo	⊢ RingOps
3		vi	⊢ 𝑖
4		cidl	⊢ Idl
5	1	cv	⊢ 𝑟
6	5 4	cfv	⊢ ( Idl ‘ 𝑟 )
7	3	cv	⊢ 𝑖
8		c1st	⊢ 1^st
9	5 8	cfv	⊢ ( 1^st ‘ 𝑟 )
10	9	crn	⊢ ran ( 1^st ‘ 𝑟 )
11	7 10	wne	⊢ 𝑖 ≠ ran ( 1^st ‘ 𝑟 )
12		vj	⊢ 𝑗
13	12	cv	⊢ 𝑗
14	7 13	wss	⊢ 𝑖 ⊆ 𝑗
15	13 7	wceq	⊢ 𝑗 = 𝑖
16	13 10	wceq	⊢ 𝑗 = ran ( 1^st ‘ 𝑟 )
17	15 16	wo	⊢ ( 𝑗 = 𝑖 ∨ 𝑗 = ran ( 1^st ‘ 𝑟 ) )
18	14 17	wi	⊢ ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ran ( 1^st ‘ 𝑟 ) ) )
19	18 12 6	wral	⊢ ∀ 𝑗 ∈ ( Idl ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ran ( 1^st ‘ 𝑟 ) ) )
20	11 19	wa	⊢ ( 𝑖 ≠ ran ( 1^st ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ran ( 1^st ‘ 𝑟 ) ) ) )
21	20 3 6	crab	⊢ { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1^st ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ran ( 1^st ‘ 𝑟 ) ) ) ) }
22	1 2 21	cmpt	⊢ ( 𝑟 ∈ RingOps ↦ { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1^st ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ran ( 1^st ‘ 𝑟 ) ) ) ) } )
23	0 22	wceq	⊢ MaxIdl = ( 𝑟 ∈ RingOps ↦ { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1^st ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ran ( 1^st ‘ 𝑟 ) ) ) ) } )

Metamath Proof Explorer

Definition df-maxidl

Detailed syntax breakdown