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

Metamath Proof Explorer

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