Step | Hyp | Ref
| Expression |
1 | | isnacs.f |
. . 3
β’ πΉ = (mrClsβπΆ) |
2 | 1 | isnacs 41074 |
. 2
β’ (πΆ β (NoeACSβπ) β (πΆ β (ACSβπ) β§ βπ β πΆ βπ β (π« π β© Fin)π = (πΉβπ))) |
3 | | eqcom 2740 |
. . . . . . . 8
β’ (π = (πΉβπ) β (πΉβπ) = π ) |
4 | 3 | rexbii 3094 |
. . . . . . 7
β’
(βπ β
(π« π β©
Fin)π = (πΉβπ) β βπ β (π« π β© Fin)(πΉβπ) = π ) |
5 | | acsmre 17540 |
. . . . . . . . 9
β’ (πΆ β (ACSβπ) β πΆ β (Mooreβπ)) |
6 | 1 | mrcf 17497 |
. . . . . . . . 9
β’ (πΆ β (Mooreβπ) β πΉ:π« πβΆπΆ) |
7 | | ffn 6672 |
. . . . . . . . 9
β’ (πΉ:π« πβΆπΆ β πΉ Fn π« π) |
8 | 5, 6, 7 | 3syl 18 |
. . . . . . . 8
β’ (πΆ β (ACSβπ) β πΉ Fn π« π) |
9 | | inss1 4192 |
. . . . . . . 8
β’
(π« π β©
Fin) β π« π |
10 | | fvelimab 6918 |
. . . . . . . 8
β’ ((πΉ Fn π« π β§ (π« π β© Fin) β π« π) β (π β (πΉ β (π« π β© Fin)) β βπ β (π« π β© Fin)(πΉβπ) = π )) |
11 | 8, 9, 10 | sylancl 587 |
. . . . . . 7
β’ (πΆ β (ACSβπ) β (π β (πΉ β (π« π β© Fin)) β βπ β (π« π β© Fin)(πΉβπ) = π )) |
12 | 4, 11 | bitr4id 290 |
. . . . . 6
β’ (πΆ β (ACSβπ) β (βπ β (π« π β© Fin)π = (πΉβπ) β π β (πΉ β (π« π β© Fin)))) |
13 | 12 | ralbidv 3171 |
. . . . 5
β’ (πΆ β (ACSβπ) β (βπ β πΆ βπ β (π« π β© Fin)π = (πΉβπ) β βπ β πΆ π β (πΉ β (π« π β© Fin)))) |
14 | | dfss3 3936 |
. . . . 5
β’ (πΆ β (πΉ β (π« π β© Fin)) β βπ β πΆ π β (πΉ β (π« π β© Fin))) |
15 | 13, 14 | bitr4di 289 |
. . . 4
β’ (πΆ β (ACSβπ) β (βπ β πΆ βπ β (π« π β© Fin)π = (πΉβπ) β πΆ β (πΉ β (π« π β© Fin)))) |
16 | | imassrn 6028 |
. . . . . . 7
β’ (πΉ β (π« π β© Fin)) β ran πΉ |
17 | | frn 6679 |
. . . . . . . 8
β’ (πΉ:π« πβΆπΆ β ran πΉ β πΆ) |
18 | 5, 6, 17 | 3syl 18 |
. . . . . . 7
β’ (πΆ β (ACSβπ) β ran πΉ β πΆ) |
19 | 16, 18 | sstrid 3959 |
. . . . . 6
β’ (πΆ β (ACSβπ) β (πΉ β (π« π β© Fin)) β πΆ) |
20 | 19 | biantrurd 534 |
. . . . 5
β’ (πΆ β (ACSβπ) β (πΆ β (πΉ β (π« π β© Fin)) β ((πΉ β (π« π β© Fin)) β πΆ β§ πΆ β (πΉ β (π« π β© Fin))))) |
21 | | eqss 3963 |
. . . . 5
β’ ((πΉ β (π« π β© Fin)) = πΆ β ((πΉ β (π« π β© Fin)) β πΆ β§ πΆ β (πΉ β (π« π β© Fin)))) |
22 | 20, 21 | bitr4di 289 |
. . . 4
β’ (πΆ β (ACSβπ) β (πΆ β (πΉ β (π« π β© Fin)) β (πΉ β (π« π β© Fin)) = πΆ)) |
23 | 15, 22 | bitrd 279 |
. . 3
β’ (πΆ β (ACSβπ) β (βπ β πΆ βπ β (π« π β© Fin)π = (πΉβπ) β (πΉ β (π« π β© Fin)) = πΆ)) |
24 | 23 | pm5.32i 576 |
. 2
β’ ((πΆ β (ACSβπ) β§ βπ β πΆ βπ β (π« π β© Fin)π = (πΉβπ)) β (πΆ β (ACSβπ) β§ (πΉ β (π« π β© Fin)) = πΆ)) |
25 | 2, 24 | bitri 275 |
1
β’ (πΆ β (NoeACSβπ) β (πΆ β (ACSβπ) β§ (πΉ β (π« π β© Fin)) = πΆ)) |