This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑟 ) ) ) ) } )