Step | Hyp | Ref
| Expression |
1 | | cacs 17533 |
. 2
class
ACS |
2 | | vx |
. . 3
setvar π₯ |
3 | | cvv 3474 |
. . 3
class
V |
4 | 2 | cv 1540 |
. . . . . . . 8
class π₯ |
5 | 4 | cpw 4602 |
. . . . . . 7
class π«
π₯ |
6 | | vf |
. . . . . . . 8
setvar π |
7 | 6 | cv 1540 |
. . . . . . 7
class π |
8 | 5, 5, 7 | wf 6539 |
. . . . . 6
wff π:π« π₯βΆπ« π₯ |
9 | | vs |
. . . . . . . . 9
setvar π |
10 | | vc |
. . . . . . . . 9
setvar π |
11 | 9, 10 | wel 2107 |
. . . . . . . 8
wff π β π |
12 | 9 | cv 1540 |
. . . . . . . . . . . . 13
class π |
13 | 12 | cpw 4602 |
. . . . . . . . . . . 12
class π«
π |
14 | | cfn 8941 |
. . . . . . . . . . . 12
class
Fin |
15 | 13, 14 | cin 3947 |
. . . . . . . . . . 11
class
(π« π β©
Fin) |
16 | 7, 15 | cima 5679 |
. . . . . . . . . 10
class (π β (π« π β© Fin)) |
17 | 16 | cuni 4908 |
. . . . . . . . 9
class βͺ (π
β (π« π β©
Fin)) |
18 | 17, 12 | wss 3948 |
. . . . . . . 8
wff βͺ (π
β (π« π β©
Fin)) β π |
19 | 11, 18 | wb 205 |
. . . . . . 7
wff (π β π β βͺ (π β (π« π β© Fin)) β π ) |
20 | 19, 9, 5 | wral 3061 |
. . . . . 6
wff
βπ β
π« π₯(π β π β βͺ (π β (π« π β© Fin)) β π ) |
21 | 8, 20 | wa 396 |
. . . . 5
wff (π:π« π₯βΆπ« π₯ β§ βπ β π« π₯(π β π β βͺ (π β (π« π β© Fin)) β π )) |
22 | 21, 6 | wex 1781 |
. . . 4
wff
βπ(π:π« π₯βΆπ« π₯ β§ βπ β π« π₯(π β π β βͺ (π β (π« π β© Fin)) β π )) |
23 | | cmre 17530 |
. . . . 5
class
Moore |
24 | 4, 23 | cfv 6543 |
. . . 4
class
(Mooreβπ₯) |
25 | 22, 10, 24 | crab 3432 |
. . 3
class {π β (Mooreβπ₯) β£ βπ(π:π« π₯βΆπ« π₯ β§ βπ β π« π₯(π β π β βͺ (π β (π« π β© Fin)) β π ))} |
26 | 2, 3, 25 | cmpt 5231 |
. 2
class (π₯ β V β¦ {π β (Mooreβπ₯) β£ βπ(π:π« π₯βΆπ« π₯ β§ βπ β π« π₯(π β π β βͺ (π β (π« π β© Fin)) β π ))}) |
27 | 1, 26 | wceq 1541 |
1
wff ACS =
(π₯ β V β¦ {π β (Mooreβπ₯) β£ βπ(π:π« π₯βΆπ« π₯ β§ βπ β π« π₯(π β π β βͺ (π β (π« π β© Fin)) β π ))}) |