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 Could not format assertion : 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 |-

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 j j = i j = Base r i j j = i j = B
9 2 8 raleqbidv r = R j LIdeal r i j j = i j = Base r j LIdeal R i j j = i j = B
10 5 9 anbi12d r = R i Base r j LIdeal r i j j = i j = Base r i B j LIdeal R i j j = i j = B
11 2 10 rabeqbidv r = R i LIdeal r | i Base r j LIdeal r i j j = i j = Base r = i LIdeal R | i B j LIdeal R i j j = i j = B
12 df-mxidl Could not format MaxIdeal = ( r e. Ring |-> { i e. ( LIdeal ` r ) | ( i =/= ( Base ` r ) /\ A. j e. ( LIdeal ` r ) ( i C_ j -> ( j = i \/ j = ( Base ` r ) ) ) ) } ) : No typesetting found for |- MaxIdeal = ( r e. Ring |-> { i e. ( LIdeal ` r ) | ( i =/= ( Base ` r ) /\ A. j e. ( LIdeal ` r ) ( i C_ j -> ( j = i \/ j = ( Base ` r ) ) ) ) } ) with typecode |-
13 fvex LIdeal R V
14 13 rabex i LIdeal R | i B j LIdeal R i j j = i j = B V
15 11 12 14 fvmpt 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 |-