Metamath Proof Explorer

Theorem ismaxidl

Description: The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011)

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

Proof

Step	Hyp	Ref	Expression
1		ismaxidl.1	\|- G = ( 1st ` R )
2		ismaxidl.2	\|- X = ran G
3	1 2	maxidlval	\|- ( R e. RingOps -> ( MaxIdl ` R ) = { i e. ( Idl ` R ) \| ( i =/= X /\ A. j e. ( Idl ` R ) ( i C_ j -> ( j = i \/ j = X ) ) ) } )
4	3	eleq2d	\|- ( R e. RingOps -> ( M e. ( MaxIdl ` R ) <-> M e. { i e. ( Idl ` R ) \| ( i =/= X /\ A. j e. ( Idl ` R ) ( i C_ j -> ( j = i \/ j = X ) ) ) } ) )
5		neeq1	\|- ( i = M -> ( i =/= X <-> M =/= X ) )
6		sseq1	\|- ( i = M -> ( i C_ j <-> M C_ j ) )
7		eqeq2	\|- ( i = M -> ( j = i <-> j = M ) )
8	7	orbi1d	\|- ( i = M -> ( ( j = i \/ j = X ) <-> ( j = M \/ j = X ) ) )
9	6 8	imbi12d	\|- ( i = M -> ( ( i C_ j -> ( j = i \/ j = X ) ) <-> ( M C_ j -> ( j = M \/ j = X ) ) ) )
10	9	ralbidv	\|- ( i = M -> ( A. j e. ( Idl ` R ) ( i C_ j -> ( j = i \/ j = X ) ) <-> A. j e. ( Idl ` R ) ( M C_ j -> ( j = M \/ j = X ) ) ) )
11	5 10	anbi12d	\|- ( i = M -> ( ( i =/= X /\ A. j e. ( Idl ` R ) ( i C_ j -> ( j = i \/ j = X ) ) ) <-> ( M =/= X /\ A. j e. ( Idl ` R ) ( M C_ j -> ( j = M \/ j = X ) ) ) ) )
12	11	elrab	\|- ( M e. { i e. ( Idl ` R ) \| ( i =/= X /\ A. j e. ( Idl ` R ) ( i C_ j -> ( j = i \/ j = X ) ) ) } <-> ( M e. ( Idl ` R ) /\ ( M =/= X /\ A. j e. ( Idl ` R ) ( M C_ j -> ( j = M \/ j = X ) ) ) ) )
13		3anass	\|- ( ( M e. ( Idl ` R ) /\ M =/= X /\ A. j e. ( Idl ` R ) ( M C_ j -> ( j = M \/ j = X ) ) ) <-> ( M e. ( Idl ` R ) /\ ( M =/= X /\ A. j e. ( Idl ` R ) ( M C_ j -> ( j = M \/ j = X ) ) ) ) )
14	12 13	bitr4i	\|- ( M e. { i e. ( Idl ` R ) \| ( i =/= X /\ A. j e. ( Idl ` R ) ( i C_ j -> ( j = i \/ j = X ) ) ) } <-> ( M e. ( Idl ` R ) /\ M =/= X /\ A. j e. ( Idl ` R ) ( M C_ j -> ( j = M \/ j = X ) ) ) )
15	4 14	bitrdi	\|- ( R e. RingOps -> ( M e. ( MaxIdl ` R ) <-> ( M e. ( Idl ` R ) /\ M =/= X /\ A. j e. ( Idl ` R ) ( M C_ j -> ( j = M \/ j = X ) ) ) ) )