Definition df-mxidl

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) (Revised by Thierry Arnoux, 19-Jan-2024)

	Ref	Expression
Assertion	df-mxidl	⊢ MaxIdeal = ( 𝑟 ∈ Ring ↦ { 𝑖 ∈ ( LIdeal ‘ 𝑟 ) ∣ ( 𝑖 ≠ ( Base ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ( Base ‘ 𝑟 ) ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmxidl	⊢ MaxIdeal
1		vr	⊢ 𝑟
2		crg	⊢ Ring
3		vi	⊢ 𝑖
4		clidl	⊢ LIdeal
5	1	cv	⊢ 𝑟
6	5 4	cfv	⊢ ( LIdeal ‘ 𝑟 )
7	3	cv	⊢ 𝑖
8		cbs	⊢ Base
9	5 8	cfv	⊢ ( Base ‘ 𝑟 )
10	7 9	wne	⊢ 𝑖 ≠ ( Base ‘ 𝑟 )
11		vj	⊢ 𝑗
12	11	cv	⊢ 𝑗
13	7 12	wss	⊢ 𝑖 ⊆ 𝑗
14	12 7	wceq	⊢ 𝑗 = 𝑖
15	12 9	wceq	⊢ 𝑗 = ( Base ‘ 𝑟 )
16	14 15	wo	⊢ ( 𝑗 = 𝑖 ∨ 𝑗 = ( Base ‘ 𝑟 ) )
17	13 16	wi	⊢ ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ( Base ‘ 𝑟 ) ) )
18	17 11 6	wral	⊢ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ( Base ‘ 𝑟 ) ) )
19	10 18	wa	⊢ ( 𝑖 ≠ ( Base ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ( Base ‘ 𝑟 ) ) ) )
20	19 3 6	crab	⊢ { 𝑖 ∈ ( LIdeal ‘ 𝑟 ) ∣ ( 𝑖 ≠ ( Base ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ( Base ‘ 𝑟 ) ) ) ) }
21	1 2 20	cmpt	⊢ ( 𝑟 ∈ Ring ↦ { 𝑖 ∈ ( LIdeal ‘ 𝑟 ) ∣ ( 𝑖 ≠ ( Base ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ( Base ‘ 𝑟 ) ) ) ) } )
22	0 21	wceq	⊢ MaxIdeal = ( 𝑟 ∈ Ring ↦ { 𝑖 ∈ ( LIdeal ‘ 𝑟 ) ∣ ( 𝑖 ≠ ( Base ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ( Base ‘ 𝑟 ) ) ) ) } )