Step | Hyp | Ref
| Expression |
1 | | clpidl 20878 |
. 2
class
LPIdeal |
2 | | vw |
. . 3
setvar π€ |
3 | | crg 20055 |
. . 3
class
Ring |
4 | | vg |
. . . 4
setvar π |
5 | 2 | cv 1540 |
. . . . 5
class π€ |
6 | | cbs 17143 |
. . . . 5
class
Base |
7 | 5, 6 | cfv 6543 |
. . . 4
class
(Baseβπ€) |
8 | 4 | cv 1540 |
. . . . . . 7
class π |
9 | 8 | csn 4628 |
. . . . . 6
class {π} |
10 | | crsp 20783 |
. . . . . . 7
class
RSpan |
11 | 5, 10 | cfv 6543 |
. . . . . 6
class
(RSpanβπ€) |
12 | 9, 11 | cfv 6543 |
. . . . 5
class
((RSpanβπ€)β{π}) |
13 | 12 | csn 4628 |
. . . 4
class
{((RSpanβπ€)β{π})} |
14 | 4, 7, 13 | ciun 4997 |
. . 3
class βͺ π β (Baseβπ€){((RSpanβπ€)β{π})} |
15 | 2, 3, 14 | cmpt 5231 |
. 2
class (π€ β Ring β¦ βͺ π β (Baseβπ€){((RSpanβπ€)β{π})}) |
16 | 1, 15 | wceq 1541 |
1
wff LPIdeal =
(π€ β Ring β¦
βͺ π β (Baseβπ€){((RSpanβπ€)β{π})}) |