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	|- B = ( Base ` R )
Assertion	mxidlval	|- ( R e. Ring -> ( MaxIdeal ` R ) = { i e. ( LIdeal ` R ) | ( i =/= B /\ A. j e. ( LIdeal ` R ) ( i C_ j -> ( j = i \/ j = B ) ) ) } )

Proof

Step	Hyp	Ref	Expression
1		mxidlval.1	|- B = ( Base ` R )
2		fveq2	|- ( r = R -> ( LIdeal ` r ) = ( LIdeal ` R ) )
3		fveq2	|- ( r = R -> ( Base ` r ) = ( Base ` R ) )
4	3 1	eqtr4di	|- ( r = R -> ( Base ` r ) = B )
5	4	neeq2d	|- ( r = R -> ( i =/= ( Base ` r ) <-> i =/= B ) )
6	4	eqeq2d	|- ( r = R -> ( j = ( Base ` r ) <-> j = B ) )
7	6	orbi2d	|- ( r = R -> ( ( j = i \/ j = ( Base ` r ) ) <-> ( j = i \/ j = B ) ) )
8	7	imbi2d	|- ( r = R -> ( ( i C_ j -> ( j = i \/ j = ( Base ` r ) ) ) <-> ( i C_ j -> ( j = i \/ j = B ) ) ) )
9	2 8	raleqbidv	|- ( r = R -> ( A. j e. ( LIdeal ` r ) ( i C_ j -> ( j = i \/ j = ( Base ` r ) ) ) <-> A. j e. ( LIdeal ` R ) ( i C_ j -> ( j = i \/ j = B ) ) ) )
10	5 9	anbi12d	|- ( r = R -> ( ( i =/= ( Base ` r ) /\ A. j e. ( LIdeal ` r ) ( i C_ j -> ( j = i \/ j = ( Base ` r ) ) ) ) <-> ( i =/= B /\ A. j e. ( LIdeal ` R ) ( i C_ j -> ( j = i \/ j = B ) ) ) ) )
11	2 10	rabeqbidv	|- ( r = R -> { i e. ( LIdeal ` r ) | ( i =/= ( Base ` r ) /\ A. j e. ( LIdeal ` r ) ( i C_ j -> ( j = i \/ j = ( Base ` r ) ) ) ) } = { i e. ( LIdeal ` R ) | ( i =/= B /\ A. j e. ( LIdeal ` R ) ( i C_ j -> ( j = i \/ j = B ) ) ) } )
12		df-mxidl	|- MaxIdeal = ( r e. Ring |-> { i e. ( LIdeal ` r ) | ( i =/= ( Base ` r ) /\ A. j e. ( LIdeal ` r ) ( i C_ j -> ( j = i \/ j = ( Base ` r ) ) ) ) } )
13		fvex	|- ( LIdeal ` R ) e. _V
14	13	rabex	|- { i e. ( LIdeal ` R ) | ( i =/= B /\ A. j e. ( LIdeal ` R ) ( i C_ j -> ( j = i \/ j = B ) ) ) } e. _V
15	11 12 14	fvmpt	|- ( R e. Ring -> ( MaxIdeal ` R ) = { i e. ( LIdeal ` R ) | ( i =/= B /\ A. j e. ( LIdeal ` R ) ( i C_ j -> ( j = i \/ j = B ) ) ) } )