Theorem mxidlval

Description: The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011) (Revised by Thierry Arnoux, 19-Jan-2024)

	Ref	Expression
Hypothesis	mxidlval.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	mxidlval	⊢ ( 𝑅 ∈ Ring → ( MaxIdeal ‘ 𝑅 ) = { 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝐵 ) ) ) } )

Proof

Step	Hyp	Ref	Expression
1		mxidlval.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		fveq2	⊢ ( 𝑟 = 𝑅 → ( LIdeal ‘ 𝑟 ) = ( LIdeal ‘ 𝑅 ) )
3		fveq2	⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
4	3 1	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = 𝐵 )
5	4	neeq2d	⊢ ( 𝑟 = 𝑅 → ( 𝑖 ≠ ( Base ‘ 𝑟 ) ↔ 𝑖 ≠ 𝐵 ) )
6	4	eqeq2d	⊢ ( 𝑟 = 𝑅 → ( 𝑗 = ( Base ‘ 𝑟 ) ↔ 𝑗 = 𝐵 ) )
7	6	orbi2d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑗 = 𝑖 ∨ 𝑗 = ( Base ‘ 𝑟 ) ) ↔ ( 𝑗 = 𝑖 ∨ 𝑗 = 𝐵 ) ) )
8	7	imbi2d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ( Base ‘ 𝑟 ) ) ) ↔ ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝐵 ) ) ) )
9	2 8	raleqbidv	⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑗 ∈ ( LIdeal ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ( Base ‘ 𝑟 ) ) ) ↔ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝐵 ) ) ) )
10	5 9	anbi12d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑖 ≠ ( Base ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ( Base ‘ 𝑟 ) ) ) ) ↔ ( 𝑖 ≠ 𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝐵 ) ) ) ) )
11	2 10	rabeqbidv	⊢ ( 𝑟 = 𝑅 → { 𝑖 ∈ ( LIdeal ‘ 𝑟 ) ∣ ( 𝑖 ≠ ( Base ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ( Base ‘ 𝑟 ) ) ) ) } = { 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝐵 ) ) ) } )
12		df-mxidl	⊢ MaxIdeal = ( 𝑟 ∈ Ring ↦ { 𝑖 ∈ ( LIdeal ‘ 𝑟 ) ∣ ( 𝑖 ≠ ( Base ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ( Base ‘ 𝑟 ) ) ) ) } )
13		fvex	⊢ ( LIdeal ‘ 𝑅 ) ∈ V
14	13	rabex	⊢ { 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝐵 ) ) ) } ∈ V
15	11 12 14	fvmpt	⊢ ( 𝑅 ∈ Ring → ( MaxIdeal ‘ 𝑅 ) = { 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( 𝑖 ≠ 𝐵 ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = 𝐵 ) ) ) } )