Step | Hyp | Ref
| Expression |
1 | | cprrng 36909 |
. 2
class
PrRing |
2 | | vr |
. . . . . . . 8
setvar π |
3 | 2 | cv 1540 |
. . . . . . 7
class π |
4 | | c1st 7972 |
. . . . . . 7
class
1st |
5 | 3, 4 | cfv 6543 |
. . . . . 6
class
(1st βπ) |
6 | | cgi 29738 |
. . . . . 6
class
GId |
7 | 5, 6 | cfv 6543 |
. . . . 5
class
(GIdβ(1st βπ)) |
8 | 7 | csn 4628 |
. . . 4
class
{(GIdβ(1st βπ))} |
9 | | cpridl 36871 |
. . . . 5
class
PrIdl |
10 | 3, 9 | cfv 6543 |
. . . 4
class
(PrIdlβπ) |
11 | 8, 10 | wcel 2106 |
. . 3
wff
{(GIdβ(1st βπ))} β (PrIdlβπ) |
12 | | crngo 36757 |
. . 3
class
RingOps |
13 | 11, 2, 12 | crab 3432 |
. 2
class {π β RingOps β£
{(GIdβ(1st βπ))} β (PrIdlβπ)} |
14 | 1, 13 | wceq 1541 |
1
wff PrRing =
{π β RingOps β£
{(GIdβ(1st βπ))} β (PrIdlβπ)} |