Metamath Proof Explorer


Definition df-mxidl

Description: Define the class of maximal ideals of a ring R . A proper ideal is called maximal if it is maximal with respect to inclusion among proper ideals. (Contributed by Jeff Madsen, 5-Jan-2011) (Revised by Thierry Arnoux, 19-Jan-2024)

Ref Expression
Assertion df-mxidl Could not format assertion : 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 |-

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmxidl Could not format MaxIdeal : No typesetting found for class MaxIdeal with typecode class
1 vr setvar r
2 crg class Ring
3 vi setvar i
4 clidl class LIdeal
5 1 cv setvar r
6 5 4 cfv class LIdeal r
7 3 cv setvar i
8 cbs class Base
9 5 8 cfv class Base r
10 7 9 wne wff i Base r
11 vj setvar j
12 11 cv setvar j
13 7 12 wss wff i j
14 12 7 wceq wff j = i
15 12 9 wceq wff j = Base r
16 14 15 wo wff j = i j = Base r
17 13 16 wi wff i j j = i j = Base r
18 17 11 6 wral wff j LIdeal r i j j = i j = Base r
19 10 18 wa wff i Base r j LIdeal r i j j = i j = Base r
20 19 3 6 crab class i LIdeal r | i Base r j LIdeal r i j j = i j = Base r
21 1 2 20 cmpt class r Ring i LIdeal r | i Base r j LIdeal r i j j = i j = Base r
22 0 21 wceq 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 wff 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 wff