Step | Hyp | Ref
| Expression |
1 | | acsmre 17537 |
. . . . 5
β’ (πΆ β (ACSβπ) β πΆ β (Mooreβπ)) |
2 | | mress 17478 |
. . . . 5
β’ ((πΆ β (Mooreβπ) β§ π β πΆ) β π β π) |
3 | 1, 2 | sylan 581 |
. . . 4
β’ ((πΆ β (ACSβπ) β§ π β πΆ) β π β π) |
4 | 3 | ex 414 |
. . 3
β’ (πΆ β (ACSβπ) β (π β πΆ β π β π)) |
5 | 4 | pm4.71rd 564 |
. 2
β’ (πΆ β (ACSβπ) β (π β πΆ β (π β π β§ π β πΆ))) |
6 | | eleq1 2822 |
. . . . 5
β’ (π = π β (π β πΆ β π β πΆ)) |
7 | | pweq 4575 |
. . . . . . 7
β’ (π = π β π« π = π« π) |
8 | 7 | ineq1d 4172 |
. . . . . 6
β’ (π = π β (π« π β© Fin) = (π« π β© Fin)) |
9 | | sseq2 3971 |
. . . . . 6
β’ (π = π β ((πΉβπ¦) β π β (πΉβπ¦) β π)) |
10 | 8, 9 | raleqbidv 3318 |
. . . . 5
β’ (π = π β (βπ¦ β (π« π β© Fin)(πΉβπ¦) β π β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π)) |
11 | 6, 10 | bibi12d 346 |
. . . 4
β’ (π = π β ((π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π ) β (π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π))) |
12 | | isacs2.f |
. . . . . . 7
β’ πΉ = (mrClsβπΆ) |
13 | 12 | isacs2 17538 |
. . . . . 6
β’ (πΆ β (ACSβπ) β (πΆ β (Mooreβπ) β§ βπ β π« π(π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π ))) |
14 | 13 | simprbi 498 |
. . . . 5
β’ (πΆ β (ACSβπ) β βπ β π« π(π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π )) |
15 | 14 | adantr 482 |
. . . 4
β’ ((πΆ β (ACSβπ) β§ π β π) β βπ β π« π(π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π )) |
16 | | elfvdm 6880 |
. . . . . 6
β’ (πΆ β (ACSβπ) β π β dom ACS) |
17 | | elpw2g 5302 |
. . . . . 6
β’ (π β dom ACS β (π β π« π β π β π)) |
18 | 16, 17 | syl 17 |
. . . . 5
β’ (πΆ β (ACSβπ) β (π β π« π β π β π)) |
19 | 18 | biimpar 479 |
. . . 4
β’ ((πΆ β (ACSβπ) β§ π β π) β π β π« π) |
20 | 11, 15, 19 | rspcdva 3581 |
. . 3
β’ ((πΆ β (ACSβπ) β§ π β π) β (π β πΆ β βπ¦ β (π« π β© Fin)(πΉβπ¦) β π)) |
21 | 20 | pm5.32da 580 |
. 2
β’ (πΆ β (ACSβπ) β ((π β π β§ π β πΆ) β (π β π β§ βπ¦ β (π« π β© Fin)(πΉβπ¦) β π))) |
22 | 5, 21 | bitrd 279 |
1
β’ (πΆ β (ACSβπ) β (π β πΆ β (π β π β§ βπ¦ β (π« π β© Fin)(πΉβπ¦) β π))) |