Step | Hyp | Ref
| Expression |
1 | | cvdwp 16765 |
. 2
class
PolyAP |
2 | | va |
. . . . . . . . . . 11
setvar π |
3 | 2 | cv 1539 |
. . . . . . . . . 10
class π |
4 | | vi |
. . . . . . . . . . . 12
setvar π |
5 | 4 | cv 1539 |
. . . . . . . . . . 11
class π |
6 | | vd |
. . . . . . . . . . . 12
setvar π |
7 | 6 | cv 1539 |
. . . . . . . . . . 11
class π |
8 | 5, 7 | cfv 6479 |
. . . . . . . . . 10
class (πβπ) |
9 | | caddc 10975 |
. . . . . . . . . 10
class
+ |
10 | 3, 8, 9 | co 7337 |
. . . . . . . . 9
class (π + (πβπ)) |
11 | | vk |
. . . . . . . . . . 11
setvar π |
12 | 11 | cv 1539 |
. . . . . . . . . 10
class π |
13 | | cvdwa 16763 |
. . . . . . . . . 10
class
AP |
14 | 12, 13 | cfv 6479 |
. . . . . . . . 9
class
(APβπ) |
15 | 10, 8, 14 | co 7337 |
. . . . . . . 8
class ((π + (πβπ))(APβπ)(πβπ)) |
16 | | vf |
. . . . . . . . . . 11
setvar π |
17 | 16 | cv 1539 |
. . . . . . . . . 10
class π |
18 | 17 | ccnv 5619 |
. . . . . . . . 9
class β‘π |
19 | 10, 17 | cfv 6479 |
. . . . . . . . . 10
class (πβ(π + (πβπ))) |
20 | 19 | csn 4573 |
. . . . . . . . 9
class {(πβ(π + (πβπ)))} |
21 | 18, 20 | cima 5623 |
. . . . . . . 8
class (β‘π β {(πβ(π + (πβπ)))}) |
22 | 15, 21 | wss 3898 |
. . . . . . 7
wff ((π + (πβπ))(APβπ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))}) |
23 | | c1 10973 |
. . . . . . . 8
class
1 |
24 | | vm |
. . . . . . . . 9
setvar π |
25 | 24 | cv 1539 |
. . . . . . . 8
class π |
26 | | cfz 13340 |
. . . . . . . 8
class
... |
27 | 23, 25, 26 | co 7337 |
. . . . . . 7
class
(1...π) |
28 | 22, 4, 27 | wral 3061 |
. . . . . 6
wff
βπ β
(1...π)((π + (πβπ))(APβπ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))}) |
29 | 4, 27, 19 | cmpt 5175 |
. . . . . . . . 9
class (π β (1...π) β¦ (πβ(π + (πβπ)))) |
30 | 29 | crn 5621 |
. . . . . . . 8
class ran
(π β (1...π) β¦ (πβ(π + (πβπ)))) |
31 | | chash 14145 |
. . . . . . . 8
class
β― |
32 | 30, 31 | cfv 6479 |
. . . . . . 7
class
(β―βran (π β (1...π) β¦ (πβ(π + (πβπ))))) |
33 | 32, 25 | wceq 1540 |
. . . . . 6
wff
(β―βran (π β (1...π) β¦ (πβ(π + (πβπ))))) = π |
34 | 28, 33 | wa 396 |
. . . . 5
wff
(βπ β
(1...π)((π + (πβπ))(APβπ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πβ(π + (πβπ))))) = π) |
35 | | cn 12074 |
. . . . . 6
class
β |
36 | | cmap 8686 |
. . . . . 6
class
βm |
37 | 35, 27, 36 | co 7337 |
. . . . 5
class (β
βm (1...π)) |
38 | 34, 6, 37 | wrex 3070 |
. . . 4
wff
βπ β
(β βm (1...π))(βπ β (1...π)((π + (πβπ))(APβπ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πβ(π + (πβπ))))) = π) |
39 | 38, 2, 35 | wrex 3070 |
. . 3
wff
βπ β
β βπ β
(β βm (1...π))(βπ β (1...π)((π + (πβπ))(APβπ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πβ(π + (πβπ))))) = π) |
40 | 39, 24, 11, 16 | coprab 7338 |
. 2
class
{β¨β¨π,
πβ©, πβ© β£ βπ β β βπ β (β βm
(1...π))(βπ β (1...π)((π + (πβπ))(APβπ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πβ(π + (πβπ))))) = π)} |
41 | 1, 40 | wceq 1540 |
1
wff PolyAP =
{β¨β¨π, πβ©, πβ© β£ βπ β β βπ β (β βm
(1...π))(βπ β (1...π)((π + (πβπ))(APβπ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πβ(π + (πβπ))))) = π)} |