Step | Hyp | Ref
| Expression |
1 | | cvdwp 16900 |
. 2
class
PolyAP |
2 | | va |
. . . . . . . . . . 11
setvar π |
3 | 2 | cv 1541 |
. . . . . . . . . 10
class π |
4 | | vi |
. . . . . . . . . . . 12
setvar π |
5 | 4 | cv 1541 |
. . . . . . . . . . 11
class π |
6 | | vd |
. . . . . . . . . . . 12
setvar π |
7 | 6 | cv 1541 |
. . . . . . . . . . 11
class π |
8 | 5, 7 | cfv 6544 |
. . . . . . . . . 10
class (πβπ) |
9 | | caddc 11113 |
. . . . . . . . . 10
class
+ |
10 | 3, 8, 9 | co 7409 |
. . . . . . . . 9
class (π + (πβπ)) |
11 | | vk |
. . . . . . . . . . 11
setvar π |
12 | 11 | cv 1541 |
. . . . . . . . . 10
class π |
13 | | cvdwa 16898 |
. . . . . . . . . 10
class
AP |
14 | 12, 13 | cfv 6544 |
. . . . . . . . 9
class
(APβπ) |
15 | 10, 8, 14 | co 7409 |
. . . . . . . 8
class ((π + (πβπ))(APβπ)(πβπ)) |
16 | | vf |
. . . . . . . . . . 11
setvar π |
17 | 16 | cv 1541 |
. . . . . . . . . 10
class π |
18 | 17 | ccnv 5676 |
. . . . . . . . 9
class β‘π |
19 | 10, 17 | cfv 6544 |
. . . . . . . . . 10
class (πβ(π + (πβπ))) |
20 | 19 | csn 4629 |
. . . . . . . . 9
class {(πβ(π + (πβπ)))} |
21 | 18, 20 | cima 5680 |
. . . . . . . 8
class (β‘π β {(πβ(π + (πβπ)))}) |
22 | 15, 21 | wss 3949 |
. . . . . . 7
wff ((π + (πβπ))(APβπ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))}) |
23 | | c1 11111 |
. . . . . . . 8
class
1 |
24 | | vm |
. . . . . . . . 9
setvar π |
25 | 24 | cv 1541 |
. . . . . . . 8
class π |
26 | | cfz 13484 |
. . . . . . . 8
class
... |
27 | 23, 25, 26 | co 7409 |
. . . . . . 7
class
(1...π) |
28 | 22, 4, 27 | wral 3062 |
. . . . . 6
wff
βπ β
(1...π)((π + (πβπ))(APβπ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))}) |
29 | 4, 27, 19 | cmpt 5232 |
. . . . . . . . 9
class (π β (1...π) β¦ (πβ(π + (πβπ)))) |
30 | 29 | crn 5678 |
. . . . . . . 8
class ran
(π β (1...π) β¦ (πβ(π + (πβπ)))) |
31 | | chash 14290 |
. . . . . . . 8
class
β― |
32 | 30, 31 | cfv 6544 |
. . . . . . 7
class
(β―βran (π β (1...π) β¦ (πβ(π + (πβπ))))) |
33 | 32, 25 | wceq 1542 |
. . . . . 6
wff
(β―βran (π β (1...π) β¦ (πβ(π + (πβπ))))) = π |
34 | 28, 33 | wa 397 |
. . . . 5
wff
(βπ β
(1...π)((π + (πβπ))(APβπ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πβ(π + (πβπ))))) = π) |
35 | | cn 12212 |
. . . . . 6
class
β |
36 | | cmap 8820 |
. . . . . 6
class
βm |
37 | 35, 27, 36 | co 7409 |
. . . . 5
class (β
βm (1...π)) |
38 | 34, 6, 37 | wrex 3071 |
. . . 4
wff
βπ β
(β βm (1...π))(βπ β (1...π)((π + (πβπ))(APβπ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πβ(π + (πβπ))))) = π) |
39 | 38, 2, 35 | wrex 3071 |
. . 3
wff
βπ β
β βπ β
(β βm (1...π))(βπ β (1...π)((π + (πβπ))(APβπ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πβ(π + (πβπ))))) = π) |
40 | 39, 24, 11, 16 | coprab 7410 |
. 2
class
{β¨β¨π,
πβ©, πβ© β£ βπ β β βπ β (β βm
(1...π))(βπ β (1...π)((π + (πβπ))(APβπ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πβ(π + (πβπ))))) = π)} |
41 | 1, 40 | wceq 1542 |
1
wff PolyAP =
{β¨β¨π, πβ©, πβ© β£ βπ β β βπ β (β βm
(1...π))(βπ β (1...π)((π + (πβπ))(APβπ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πβ(π + (πβπ))))) = π)} |