Step | Hyp | Ref
| Expression |
1 | | cdgraa 41510 |
. 2
class
degAA |
2 | | vx |
. . 3
setvar π₯ |
3 | | caa 25690 |
. . 3
class
πΈ |
4 | | vp |
. . . . . . . . . 10
setvar π |
5 | 4 | cv 1541 |
. . . . . . . . 9
class π |
6 | | cdgr 25564 |
. . . . . . . . 9
class
deg |
7 | 5, 6 | cfv 6497 |
. . . . . . . 8
class
(degβπ) |
8 | | vd |
. . . . . . . . 9
setvar π |
9 | 8 | cv 1541 |
. . . . . . . 8
class π |
10 | 7, 9 | wceq 1542 |
. . . . . . 7
wff
(degβπ) =
π |
11 | 2 | cv 1541 |
. . . . . . . . 9
class π₯ |
12 | 11, 5 | cfv 6497 |
. . . . . . . 8
class (πβπ₯) |
13 | | cc0 11056 |
. . . . . . . 8
class
0 |
14 | 12, 13 | wceq 1542 |
. . . . . . 7
wff (πβπ₯) = 0 |
15 | 10, 14 | wa 397 |
. . . . . 6
wff
((degβπ) =
π β§ (πβπ₯) = 0) |
16 | | cq 12878 |
. . . . . . . 8
class
β |
17 | | cply 25561 |
. . . . . . . 8
class
Poly |
18 | 16, 17 | cfv 6497 |
. . . . . . 7
class
(Polyββ) |
19 | | c0p 25049 |
. . . . . . . 8
class
0π |
20 | 19 | csn 4587 |
. . . . . . 7
class
{0π} |
21 | 18, 20 | cdif 3908 |
. . . . . 6
class
((Polyββ) β {0π}) |
22 | 15, 4, 21 | wrex 3070 |
. . . . 5
wff
βπ β
((Polyββ) β {0π})((degβπ) = π β§ (πβπ₯) = 0) |
23 | | cn 12158 |
. . . . 5
class
β |
24 | 22, 8, 23 | crab 3406 |
. . . 4
class {π β β β£
βπ β
((Polyββ) β {0π})((degβπ) = π β§ (πβπ₯) = 0)} |
25 | | cr 11055 |
. . . 4
class
β |
26 | | clt 11194 |
. . . 4
class
< |
27 | 24, 25, 26 | cinf 9382 |
. . 3
class
inf({π β
β β£ βπ
β ((Polyββ) β {0π})((degβπ) = π β§ (πβπ₯) = 0)}, β, < ) |
28 | 2, 3, 27 | cmpt 5189 |
. 2
class (π₯ β πΈ β¦
inf({π β β
β£ βπ β
((Polyββ) β {0π})((degβπ) = π β§ (πβπ₯) = 0)}, β, < )) |
29 | 1, 28 | wceq 1542 |
1
wff
degAA = (π₯ β πΈ β¦ inf({π β β β£
βπ β
((Polyββ) β {0π})((degβπ) = π β§ (πβπ₯) = 0)}, β, < )) |