Metamath Proof Explorer

Theorem maxidlval

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

		Ref	Expression
	Hypotheses	maxidlval.1	\|- G = ( 1st ` R )
		maxidlval.2	\|- X = ran G
	Assertion	maxidlval	\|- ( R e. RingOps -> ( MaxIdl ` R ) = { i e. ( Idl ` R ) \| ( i =/= X /\ A. j e. ( Idl ` R ) ( i C_ j -> ( j = i \/ j = X ) ) ) } )

Proof

Step	Hyp	Ref	Expression
1		maxidlval.1	\|- G = ( 1st ` R )
2		maxidlval.2	\|- X = ran G
3		fveq2	\|- ( r = R -> ( Idl ` r ) = ( Idl ` R ) )
4		fveq2	\|- ( r = R -> ( 1st ` r ) = ( 1st ` R ) )
5	4 1	eqtr4di	\|- ( r = R -> ( 1st ` r ) = G )
6	5	rneqd	\|- ( r = R -> ran ( 1st ` r ) = ran G )
7	6 2	eqtr4di	\|- ( r = R -> ran ( 1st ` r ) = X )
8	7	neeq2d	\|- ( r = R -> ( i =/= ran ( 1st ` r ) <-> i =/= X ) )
9	7	eqeq2d	\|- ( r = R -> ( j = ran ( 1st ` r ) <-> j = X ) )
10	9	orbi2d	\|- ( r = R -> ( ( j = i \/ j = ran ( 1st ` r ) ) <-> ( j = i \/ j = X ) ) )
11	10	imbi2d	\|- ( r = R -> ( ( i C_ j -> ( j = i \/ j = ran ( 1st ` r ) ) ) <-> ( i C_ j -> ( j = i \/ j = X ) ) ) )
12	3 11	raleqbidv	\|- ( r = R -> ( A. j e. ( Idl ` r ) ( i C_ j -> ( j = i \/ j = ran ( 1st ` r ) ) ) <-> A. j e. ( Idl ` R ) ( i C_ j -> ( j = i \/ j = X ) ) ) )
13	8 12	anbi12d	\|- ( r = R -> ( ( i =/= ran ( 1st ` r ) /\ A. j e. ( Idl ` r ) ( i C_ j -> ( j = i \/ j = ran ( 1st ` r ) ) ) ) <-> ( i =/= X /\ A. j e. ( Idl ` R ) ( i C_ j -> ( j = i \/ j = X ) ) ) ) )
14	3 13	rabeqbidv	\|- ( r = R -> { i e. ( Idl ` r ) \| ( i =/= ran ( 1st ` r ) /\ A. j e. ( Idl ` r ) ( i C_ j -> ( j = i \/ j = ran ( 1st ` r ) ) ) ) } = { i e. ( Idl ` R ) \| ( i =/= X /\ A. j e. ( Idl ` R ) ( i C_ j -> ( j = i \/ j = X ) ) ) } )
15		df-maxidl	\|- MaxIdl = ( r e. RingOps \|-> { i e. ( Idl ` r ) \| ( i =/= ran ( 1st ` r ) /\ A. j e. ( Idl ` r ) ( i C_ j -> ( j = i \/ j = ran ( 1st ` r ) ) ) ) } )
16		fvex	\|- ( Idl ` R ) e. _V
17	16	rabex	\|- { i e. ( Idl ` R ) \| ( i =/= X /\ A. j e. ( Idl ` R ) ( i C_ j -> ( j = i \/ j = X ) ) ) } e. _V
18	14 15 17	fvmpt	\|- ( R e. RingOps -> ( MaxIdl ` R ) = { i e. ( Idl ` R ) \| ( i =/= X /\ A. j e. ( Idl ` R ) ( i C_ j -> ( j = i \/ j = X ) ) ) } )