Step | Hyp | Ref
| Expression |
1 | | acsmre 17602 |
. . . . 5
β’ (πΆ β (ACSβπ) β πΆ β (Mooreβπ)) |
2 | | mress 17543 |
. . . . 5
β’ ((πΆ β (Mooreβπ) β§ π β πΆ) β π β π) |
3 | 1, 2 | sylan 579 |
. . . 4
β’ ((πΆ β (ACSβπ) β§ π β πΆ) β π β π) |
4 | 3 | ex 412 |
. . 3
β’ (πΆ β (ACSβπ) β (π β πΆ β π β π)) |
5 | 4 | pm4.71rd 562 |
. 2
β’ (πΆ β (ACSβπ) β (π β πΆ β (π β π β§ π β πΆ))) |
6 | | eleq1 2815 |
. . . . 5
β’ (π = π β (π β πΆ β π β πΆ)) |
7 | | pweq 4611 |
. . . . . . 7
β’ (π = π β π« π = π« π) |
8 | 7 | ineq1d 4206 |
. . . . . 6
β’ (π = π β (π« π β© Fin) = (π« π β© Fin)) |
9 | | sseq2 4003 |
. . . . . 6
β’ (π = π β ((πΉβπ¦) β π β (πΉβπ¦) β π)) |
10 | 8, 9 | raleqbidv 3336 |
. . . . 5
β’ (π = π β (βπ¦ β (π« π β© Fin)(πΉβπ¦) β π β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π)) |
11 | 6, 10 | bibi12d 345 |
. . . 4
β’ (π = π β ((π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π ) β (π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π))) |
12 | | isacs2.f |
. . . . . . 7
β’ πΉ = (mrClsβπΆ) |
13 | 12 | isacs2 17603 |
. . . . . 6
β’ (πΆ β (ACSβπ) β (πΆ β (Mooreβπ) β§ βπ β π« π(π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π ))) |
14 | 13 | simprbi 496 |
. . . . 5
β’ (πΆ β (ACSβπ) β βπ β π« π(π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π )) |
15 | 14 | adantr 480 |
. . . 4
β’ ((πΆ β (ACSβπ) β§ π β π) β βπ β π« π(π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π )) |
16 | | elfvdm 6921 |
. . . . . 6
β’ (πΆ β (ACSβπ) β π β dom ACS) |
17 | | elpw2g 5337 |
. . . . . 6
β’ (π β dom ACS β (π β π« π β π β π)) |
18 | 16, 17 | syl 17 |
. . . . 5
β’ (πΆ β (ACSβπ) β (π β π« π β π β π)) |
19 | 18 | biimpar 477 |
. . . 4
β’ ((πΆ β (ACSβπ) β§ π β π) β π β π« π) |
20 | 11, 15, 19 | rspcdva 3607 |
. . 3
β’ ((πΆ β (ACSβπ) β§ π β π) β (π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π)) |
21 | 20 | pm5.32da 578 |
. 2
β’ (πΆ β (ACSβπ) β ((π β π β§ π β πΆ) β (π β π β§ βπ¦ β (π« π β© Fin)(πΉβπ¦) β π))) |
22 | 5, 21 | bitrd 279 |
1
β’ (πΆ β (ACSβπ) β (π β πΆ β (π β π β§ βπ¦ β (π« π β© Fin)(πΉβπ¦) β π))) |