Metamath Proof Explorer


Theorem ismxidl

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

Ref Expression
Hypothesis mxidlval.1 B = Base R
Assertion ismxidl Could not format assertion : No typesetting found for |- ( R e. Ring -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( LIdeal ` R ) /\ M =/= B /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = B ) ) ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 mxidlval.1 B = Base R
2 1 mxidlval Could not format ( R e. Ring -> ( MaxIdeal ` R ) = { i e. ( LIdeal ` R ) | ( i =/= B /\ A. j e. ( LIdeal ` R ) ( i C_ j -> ( j = i \/ j = B ) ) ) } ) : No typesetting found for |- ( R e. Ring -> ( MaxIdeal ` R ) = { i e. ( LIdeal ` R ) | ( i =/= B /\ A. j e. ( LIdeal ` R ) ( i C_ j -> ( j = i \/ j = B ) ) ) } ) with typecode |-
3 2 eleq2d Could not format ( R e. Ring -> ( M e. ( MaxIdeal ` R ) <-> M e. { i e. ( LIdeal ` R ) | ( i =/= B /\ A. j e. ( LIdeal ` R ) ( i C_ j -> ( j = i \/ j = B ) ) ) } ) ) : No typesetting found for |- ( R e. Ring -> ( M e. ( MaxIdeal ` R ) <-> M e. { i e. ( LIdeal ` R ) | ( i =/= B /\ A. j e. ( LIdeal ` R ) ( i C_ j -> ( j = i \/ j = B ) ) ) } ) ) with typecode |-
4 neeq1 i = M i B M B
5 sseq1 i = M i j M j
6 eqeq2 i = M j = i j = M
7 6 orbi1d i = M j = i j = B j = M j = B
8 5 7 imbi12d i = M i j j = i j = B M j j = M j = B
9 8 ralbidv i = M j LIdeal R i j j = i j = B j LIdeal R M j j = M j = B
10 4 9 anbi12d i = M i B j LIdeal R i j j = i j = B M B j LIdeal R M j j = M j = B
11 10 elrab M i LIdeal R | i B j LIdeal R i j j = i j = B M LIdeal R M B j LIdeal R M j j = M j = B
12 3anass M LIdeal R M B j LIdeal R M j j = M j = B M LIdeal R M B j LIdeal R M j j = M j = B
13 11 12 bitr4i M i LIdeal R | i B j LIdeal R i j j = i j = B M LIdeal R M B j LIdeal R M j j = M j = B
14 3 13 bitrdi Could not format ( R e. Ring -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( LIdeal ` R ) /\ M =/= B /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = B ) ) ) ) ) : No typesetting found for |- ( R e. Ring -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( LIdeal ` R ) /\ M =/= B /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = B ) ) ) ) ) with typecode |-