Step | Hyp | Ref
| Expression |
1 | | isacs 17602 |
. 2
β’ (πΆ β (ACSβπ) β (πΆ β (Mooreβπ) β§ βπ(π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βͺ (π β (π« π‘ β© Fin)) β π‘)))) |
2 | | ffun 6713 |
. . . . . . . . . . 11
β’ (π:π« πβΆπ« π β Fun π) |
3 | | funiunfv 7242 |
. . . . . . . . . . 11
β’ (Fun
π β βͺ π§ β (π« π‘ β© Fin)(πβπ§) = βͺ (π β (π« π‘ β© Fin))) |
4 | 2, 3 | syl 17 |
. . . . . . . . . 10
β’ (π:π« πβΆπ« π β βͺ
π§ β (π« π‘ β© Fin)(πβπ§) = βͺ (π β (π« π‘ β© Fin))) |
5 | 4 | sseq1d 4008 |
. . . . . . . . 9
β’ (π:π« πβΆπ« π β (βͺ
π§ β (π« π‘ β© Fin)(πβπ§) β π‘ β βͺ (π β (π« π‘ β© Fin)) β π‘)) |
6 | | iunss 5041 |
. . . . . . . . 9
β’ (βͺ π§ β (π« π‘ β© Fin)(πβπ§) β π‘ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘) |
7 | 5, 6 | bitr3di 286 |
. . . . . . . 8
β’ (π:π« πβΆπ« π β (βͺ (π β (π« π‘ β© Fin)) β π‘ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘)) |
8 | 7 | bibi2d 342 |
. . . . . . 7
β’ (π:π« πβΆπ« π β ((π‘ β πΆ β βͺ (π β (π« π‘ β© Fin)) β π‘) β (π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) |
9 | 8 | ralbidv 3171 |
. . . . . 6
β’ (π:π« πβΆπ« π β (βπ‘ β π« π(π‘ β πΆ β βͺ (π β (π« π‘ β© Fin)) β π‘) β βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) |
10 | 9 | pm5.32i 574 |
. . . . 5
β’ ((π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βͺ (π β (π« π‘ β© Fin)) β π‘)) β (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) |
11 | 10 | exbii 1842 |
. . . 4
β’
(βπ(π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βͺ (π β (π« π‘ β© Fin)) β π‘)) β βπ(π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) |
12 | | simpll 764 |
. . . . . . . . . . . 12
β’ (((πΆ β (Mooreβπ) β§ π β πΆ) β§ π¦ β (π« π β© Fin)) β πΆ β (Mooreβπ)) |
13 | | elinel1 4190 |
. . . . . . . . . . . . . 14
β’ (π¦ β (π« π β© Fin) β π¦ β π« π ) |
14 | 13 | elpwid 4606 |
. . . . . . . . . . . . 13
β’ (π¦ β (π« π β© Fin) β π¦ β π ) |
15 | 14 | adantl 481 |
. . . . . . . . . . . 12
β’ (((πΆ β (Mooreβπ) β§ π β πΆ) β§ π¦ β (π« π β© Fin)) β π¦ β π ) |
16 | | simplr 766 |
. . . . . . . . . . . 12
β’ (((πΆ β (Mooreβπ) β§ π β πΆ) β§ π¦ β (π« π β© Fin)) β π β πΆ) |
17 | | isacs2.f |
. . . . . . . . . . . . 13
β’ πΉ = (mrClsβπΆ) |
18 | 17 | mrcsscl 17571 |
. . . . . . . . . . . 12
β’ ((πΆ β (Mooreβπ) β§ π¦ β π β§ π β πΆ) β (πΉβπ¦) β π ) |
19 | 12, 15, 16, 18 | syl3anc 1368 |
. . . . . . . . . . 11
β’ (((πΆ β (Mooreβπ) β§ π β πΆ) β§ π¦ β (π« π β© Fin)) β (πΉβπ¦) β π ) |
20 | 19 | ralrimiva 3140 |
. . . . . . . . . 10
β’ ((πΆ β (Mooreβπ) β§ π β πΆ) β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π ) |
21 | 20 | ad4ant14 749 |
. . . . . . . . 9
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ π β πΆ) β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π ) |
22 | | fveq2 6884 |
. . . . . . . . . . . . . . . 16
β’ (π§ = π¦ β (πβπ§) = (πβπ¦)) |
23 | 22 | sseq1d 4008 |
. . . . . . . . . . . . . . 15
β’ (π§ = π¦ β ((πβπ§) β (πΉβπ¦) β (πβπ¦) β (πΉβπ¦))) |
24 | | simplll 772 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ π¦ β (π« π β© Fin)) β πΆ β (Mooreβπ)) |
25 | 14 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ π¦ β (π« π β© Fin)) β π¦ β π ) |
26 | | elpwi 4604 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π« π β π β π) |
27 | 26 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ π¦ β (π« π β© Fin)) β π β π) |
28 | 25, 27 | sstrd 3987 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ π¦ β (π« π β© Fin)) β π¦ β π) |
29 | 17 | mrccl 17562 |
. . . . . . . . . . . . . . . . 17
β’ ((πΆ β (Mooreβπ) β§ π¦ β π) β (πΉβπ¦) β πΆ) |
30 | 24, 28, 29 | syl2anc 583 |
. . . . . . . . . . . . . . . 16
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ π¦ β (π« π β© Fin)) β (πΉβπ¦) β πΆ) |
31 | | eleq1 2815 |
. . . . . . . . . . . . . . . . . 18
β’ (π‘ = (πΉβπ¦) β (π‘ β πΆ β (πΉβπ¦) β πΆ)) |
32 | | pweq 4611 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π‘ = (πΉβπ¦) β π« π‘ = π« (πΉβπ¦)) |
33 | 32 | ineq1d 4206 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ = (πΉβπ¦) β (π« π‘ β© Fin) = (π« (πΉβπ¦) β© Fin)) |
34 | | sseq2 4003 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ = (πΉβπ¦) β ((πβπ§) β π‘ β (πβπ§) β (πΉβπ¦))) |
35 | 33, 34 | raleqbidv 3336 |
. . . . . . . . . . . . . . . . . 18
β’ (π‘ = (πΉβπ¦) β (βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘ β βπ§ β (π« (πΉβπ¦) β© Fin)(πβπ§) β (πΉβπ¦))) |
36 | 31, 35 | bibi12d 345 |
. . . . . . . . . . . . . . . . 17
β’ (π‘ = (πΉβπ¦) β ((π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘) β ((πΉβπ¦) β πΆ β βπ§ β (π« (πΉβπ¦) β© Fin)(πβπ§) β (πΉβπ¦)))) |
37 | | simprr 770 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘)) |
38 | 37 | ad2antrr 723 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ π¦ β (π« π β© Fin)) β βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘)) |
39 | | mresspw 17543 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΆ β (Mooreβπ) β πΆ β π« π) |
40 | 39 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ π¦ β (π« π β© Fin)) β πΆ β π« π) |
41 | 40, 30 | sseldd 3978 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ π¦ β (π« π β© Fin)) β (πΉβπ¦) β π« π) |
42 | 36, 38, 41 | rspcdva 3607 |
. . . . . . . . . . . . . . . 16
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ π¦ β (π« π β© Fin)) β ((πΉβπ¦) β πΆ β βπ§ β (π« (πΉβπ¦) β© Fin)(πβπ§) β (πΉβπ¦))) |
43 | 30, 42 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ π¦ β (π« π β© Fin)) β βπ§ β (π« (πΉβπ¦) β© Fin)(πβπ§) β (πΉβπ¦)) |
44 | 24, 17, 28 | mrcssidd 17576 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ π¦ β (π« π β© Fin)) β π¦ β (πΉβπ¦)) |
45 | | vex 3472 |
. . . . . . . . . . . . . . . . . 18
β’ π¦ β V |
46 | 45 | elpw 4601 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β π« (πΉβπ¦) β π¦ β (πΉβπ¦)) |
47 | 44, 46 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ π¦ β (π« π β© Fin)) β π¦ β π« (πΉβπ¦)) |
48 | | elinel2 4191 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β (π« π β© Fin) β π¦ β Fin) |
49 | 48 | adantl 481 |
. . . . . . . . . . . . . . . 16
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ π¦ β (π« π β© Fin)) β π¦ β Fin) |
50 | 47, 49 | elind 4189 |
. . . . . . . . . . . . . . 15
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ π¦ β (π« π β© Fin)) β π¦ β (π« (πΉβπ¦) β© Fin)) |
51 | 23, 43, 50 | rspcdva 3607 |
. . . . . . . . . . . . . 14
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ π¦ β (π« π β© Fin)) β (πβπ¦) β (πΉβπ¦)) |
52 | | sstr2 3984 |
. . . . . . . . . . . . . 14
β’ ((πβπ¦) β (πΉβπ¦) β ((πΉβπ¦) β π β (πβπ¦) β π )) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ π¦ β (π« π β© Fin)) β ((πΉβπ¦) β π β (πβπ¦) β π )) |
54 | 53 | ralimdva 3161 |
. . . . . . . . . . . 12
β’ (((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β (βπ¦ β (π« π β© Fin)(πΉβπ¦) β π β βπ¦ β (π« π β© Fin)(πβπ¦) β π )) |
55 | 54 | imp 406 |
. . . . . . . . . . 11
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ βπ¦ β (π« π β© Fin)(πΉβπ¦) β π ) β βπ¦ β (π« π β© Fin)(πβπ¦) β π ) |
56 | | fveq2 6884 |
. . . . . . . . . . . . 13
β’ (π¦ = π§ β (πβπ¦) = (πβπ§)) |
57 | 56 | sseq1d 4008 |
. . . . . . . . . . . 12
β’ (π¦ = π§ β ((πβπ¦) β π β (πβπ§) β π )) |
58 | 57 | cbvralvw 3228 |
. . . . . . . . . . 11
β’
(βπ¦ β
(π« π β©
Fin)(πβπ¦) β π β βπ§ β (π« π β© Fin)(πβπ§) β π ) |
59 | 55, 58 | sylib 217 |
. . . . . . . . . 10
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ βπ¦ β (π« π β© Fin)(πΉβπ¦) β π ) β βπ§ β (π« π β© Fin)(πβπ§) β π ) |
60 | | eleq1 2815 |
. . . . . . . . . . . 12
β’ (π‘ = π β (π‘ β πΆ β π β πΆ)) |
61 | | pweq 4611 |
. . . . . . . . . . . . . 14
β’ (π‘ = π β π« π‘ = π« π ) |
62 | 61 | ineq1d 4206 |
. . . . . . . . . . . . 13
β’ (π‘ = π β (π« π‘ β© Fin) = (π« π β© Fin)) |
63 | | sseq2 4003 |
. . . . . . . . . . . . 13
β’ (π‘ = π β ((πβπ§) β π‘ β (πβπ§) β π )) |
64 | 62, 63 | raleqbidv 3336 |
. . . . . . . . . . . 12
β’ (π‘ = π β (βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘ β βπ§ β (π« π β© Fin)(πβπ§) β π )) |
65 | 60, 64 | bibi12d 345 |
. . . . . . . . . . 11
β’ (π‘ = π β ((π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘) β (π β πΆ β βπ§ β (π« π β© Fin)(πβπ§) β π ))) |
66 | 37 | ad2antrr 723 |
. . . . . . . . . . 11
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ βπ¦ β (π« π β© Fin)(πΉβπ¦) β π ) β βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘)) |
67 | | simplr 766 |
. . . . . . . . . . 11
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ βπ¦ β (π« π β© Fin)(πΉβπ¦) β π ) β π β π« π) |
68 | 65, 66, 67 | rspcdva 3607 |
. . . . . . . . . 10
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ βπ¦ β (π« π β© Fin)(πΉβπ¦) β π ) β (π β πΆ β βπ§ β (π« π β© Fin)(πβπ§) β π )) |
69 | 59, 68 | mpbird 257 |
. . . . . . . . 9
β’ ((((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β§ βπ¦ β (π« π β© Fin)(πΉβπ¦) β π ) β π β πΆ) |
70 | 21, 69 | impbida 798 |
. . . . . . . 8
β’ (((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β§ π β π« π) β (π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π )) |
71 | 70 | ralrimiva 3140 |
. . . . . . 7
β’ ((πΆ β (Mooreβπ) β§ (π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) β βπ β π« π(π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π )) |
72 | 71 | ex 412 |
. . . . . 6
β’ (πΆ β (Mooreβπ) β ((π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘)) β βπ β π« π(π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π ))) |
73 | 72 | exlimdv 1928 |
. . . . 5
β’ (πΆ β (Mooreβπ) β (βπ(π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘)) β βπ β π« π(π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π ))) |
74 | 17 | mrcf 17560 |
. . . . . . . 8
β’ (πΆ β (Mooreβπ) β πΉ:π« πβΆπΆ) |
75 | 74, 39 | fssd 6728 |
. . . . . . 7
β’ (πΆ β (Mooreβπ) β πΉ:π« πβΆπ« π) |
76 | 17 | fvexi 6898 |
. . . . . . . 8
β’ πΉ β V |
77 | | feq1 6691 |
. . . . . . . . 9
β’ (π = πΉ β (π:π« πβΆπ« π β πΉ:π« πβΆπ« π)) |
78 | | fveq1 6883 |
. . . . . . . . . . . . . . 15
β’ (π = πΉ β (πβπ§) = (πΉβπ§)) |
79 | 78 | sseq1d 4008 |
. . . . . . . . . . . . . 14
β’ (π = πΉ β ((πβπ§) β π‘ β (πΉβπ§) β π‘)) |
80 | 79 | ralbidv 3171 |
. . . . . . . . . . . . 13
β’ (π = πΉ β (βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘ β βπ§ β (π« π‘ β© Fin)(πΉβπ§) β π‘)) |
81 | | fveq2 6884 |
. . . . . . . . . . . . . . 15
β’ (π§ = π¦ β (πΉβπ§) = (πΉβπ¦)) |
82 | 81 | sseq1d 4008 |
. . . . . . . . . . . . . 14
β’ (π§ = π¦ β ((πΉβπ§) β π‘ β (πΉβπ¦) β π‘)) |
83 | 82 | cbvralvw 3228 |
. . . . . . . . . . . . 13
β’
(βπ§ β
(π« π‘ β©
Fin)(πΉβπ§) β π‘ β βπ¦ β (π« π‘ β© Fin)(πΉβπ¦) β π‘) |
84 | 80, 83 | bitrdi 287 |
. . . . . . . . . . . 12
β’ (π = πΉ β (βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘ β βπ¦ β (π« π‘ β© Fin)(πΉβπ¦) β π‘)) |
85 | 84 | bibi2d 342 |
. . . . . . . . . . 11
β’ (π = πΉ β ((π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘) β (π‘ β πΆ β βπ¦ β (π« π‘ β© Fin)(πΉβπ¦) β π‘))) |
86 | 85 | ralbidv 3171 |
. . . . . . . . . 10
β’ (π = πΉ β (βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘) β βπ‘ β π« π(π‘ β πΆ β βπ¦ β (π« π‘ β© Fin)(πΉβπ¦) β π‘))) |
87 | | sseq2 4003 |
. . . . . . . . . . . . 13
β’ (π‘ = π β ((πΉβπ¦) β π‘ β (πΉβπ¦) β π )) |
88 | 62, 87 | raleqbidv 3336 |
. . . . . . . . . . . 12
β’ (π‘ = π β (βπ¦ β (π« π‘ β© Fin)(πΉβπ¦) β π‘ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π )) |
89 | 60, 88 | bibi12d 345 |
. . . . . . . . . . 11
β’ (π‘ = π β ((π‘ β πΆ β βπ¦ β (π« π‘ β© Fin)(πΉβπ¦) β π‘) β (π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π ))) |
90 | 89 | cbvralvw 3228 |
. . . . . . . . . 10
β’
(βπ‘ β
π« π(π‘ β πΆ β βπ¦ β (π« π‘ β© Fin)(πΉβπ¦) β π‘) β βπ β π« π(π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π )) |
91 | 86, 90 | bitrdi 287 |
. . . . . . . . 9
β’ (π = πΉ β (βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘) β βπ β π« π(π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π ))) |
92 | 77, 91 | anbi12d 630 |
. . . . . . . 8
β’ (π = πΉ β ((π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘)) β (πΉ:π« πβΆπ« π β§ βπ β π« π(π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π )))) |
93 | 76, 92 | spcev 3590 |
. . . . . . 7
β’ ((πΉ:π« πβΆπ« π β§ βπ β π« π(π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π )) β βπ(π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) |
94 | 75, 93 | sylan 579 |
. . . . . 6
β’ ((πΆ β (Mooreβπ) β§ βπ β π« π(π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π )) β βπ(π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘))) |
95 | 94 | ex 412 |
. . . . 5
β’ (πΆ β (Mooreβπ) β (βπ β π« π(π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π ) β βπ(π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘)))) |
96 | 73, 95 | impbid 211 |
. . . 4
β’ (πΆ β (Mooreβπ) β (βπ(π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βπ§ β (π« π‘ β© Fin)(πβπ§) β π‘)) β βπ β π« π(π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π ))) |
97 | 11, 96 | bitrid 283 |
. . 3
β’ (πΆ β (Mooreβπ) β (βπ(π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βͺ (π β (π« π‘ β© Fin)) β π‘)) β βπ β π« π(π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π ))) |
98 | 97 | pm5.32i 574 |
. 2
β’ ((πΆ β (Mooreβπ) β§ βπ(π:π« πβΆπ« π β§ βπ‘ β π« π(π‘ β πΆ β βͺ (π β (π« π‘ β© Fin)) β π‘))) β (πΆ β (Mooreβπ) β§ βπ β π« π(π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π ))) |
99 | 1, 98 | bitri 275 |
1
β’ (πΆ β (ACSβπ) β (πΆ β (Mooreβπ) β§ βπ β π« π(π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π ))) |