Step | Hyp | Ref
| Expression |
1 | | cmxidl 32276 |
. 2
class
MaxIdeal |
2 | | vr |
. . 3
setvar π |
3 | | crg 19969 |
. . 3
class
Ring |
4 | | vi |
. . . . . . 7
setvar π |
5 | 4 | cv 1541 |
. . . . . 6
class π |
6 | 2 | cv 1541 |
. . . . . . 7
class π |
7 | | cbs 17088 |
. . . . . . 7
class
Base |
8 | 6, 7 | cfv 6497 |
. . . . . 6
class
(Baseβπ) |
9 | 5, 8 | wne 2940 |
. . . . 5
wff π β (Baseβπ) |
10 | | vj |
. . . . . . . . 9
setvar π |
11 | 10 | cv 1541 |
. . . . . . . 8
class π |
12 | 5, 11 | wss 3911 |
. . . . . . 7
wff π β π |
13 | 10, 4 | weq 1967 |
. . . . . . . 8
wff π = π |
14 | 11, 8 | wceq 1542 |
. . . . . . . 8
wff π = (Baseβπ) |
15 | 13, 14 | wo 846 |
. . . . . . 7
wff (π = π β¨ π = (Baseβπ)) |
16 | 12, 15 | wi 4 |
. . . . . 6
wff (π β π β (π = π β¨ π = (Baseβπ))) |
17 | | clidl 20647 |
. . . . . . 7
class
LIdeal |
18 | 6, 17 | cfv 6497 |
. . . . . 6
class
(LIdealβπ) |
19 | 16, 10, 18 | wral 3061 |
. . . . 5
wff
βπ β
(LIdealβπ)(π β π β (π = π β¨ π = (Baseβπ))) |
20 | 9, 19 | wa 397 |
. . . 4
wff (π β (Baseβπ) β§ βπ β (LIdealβπ)(π β π β (π = π β¨ π = (Baseβπ)))) |
21 | 20, 4, 18 | crab 3406 |
. . 3
class {π β (LIdealβπ) β£ (π β (Baseβπ) β§ βπ β (LIdealβπ)(π β π β (π = π β¨ π = (Baseβπ))))} |
22 | 2, 3, 21 | cmpt 5189 |
. 2
class (π β Ring β¦ {π β (LIdealβπ) β£ (π β (Baseβπ) β§ βπ β (LIdealβπ)(π β π β (π = π β¨ π = (Baseβπ))))}) |
23 | 1, 22 | wceq 1542 |
1
wff MaxIdeal =
(π β Ring β¦
{π β
(LIdealβπ) β£
(π β (Baseβπ) β§ βπ β (LIdealβπ)(π β π β (π = π β¨ π = (Baseβπ))))}) |