Step | Hyp | Ref
| Expression |
1 | | isnacs.f |
. . 3
β’ πΉ = (mrClsβπΆ) |
2 | 1 | isnacs 41432 |
. 2
β’ (πΆ β (NoeACSβπ) β (πΆ β (ACSβπ) β§ βπ β πΆ βπ β (π« π β© Fin)π = (πΉβπ))) |
3 | | eqcom 2739 |
. . . . . . . 8
β’ (π = (πΉβπ) β (πΉβπ) = π ) |
4 | 3 | rexbii 3094 |
. . . . . . 7
β’
(βπ β
(π« π β©
Fin)π = (πΉβπ) β βπ β (π« π β© Fin)(πΉβπ) = π ) |
5 | | acsmre 17595 |
. . . . . . . . 9
β’ (πΆ β (ACSβπ) β πΆ β (Mooreβπ)) |
6 | 1 | mrcf 17552 |
. . . . . . . . 9
β’ (πΆ β (Mooreβπ) β πΉ:π« πβΆπΆ) |
7 | | ffn 6717 |
. . . . . . . . 9
β’ (πΉ:π« πβΆπΆ β πΉ Fn π« π) |
8 | 5, 6, 7 | 3syl 18 |
. . . . . . . 8
β’ (πΆ β (ACSβπ) β πΉ Fn π« π) |
9 | | inss1 4228 |
. . . . . . . 8
β’
(π« π β©
Fin) β π« π |
10 | | fvelimab 6964 |
. . . . . . . 8
β’ ((πΉ Fn π« π β§ (π« π β© Fin) β π« π) β (π β (πΉ β (π« π β© Fin)) β βπ β (π« π β© Fin)(πΉβπ) = π )) |
11 | 8, 9, 10 | sylancl 586 |
. . . . . . 7
β’ (πΆ β (ACSβπ) β (π β (πΉ β (π« π β© Fin)) β βπ β (π« π β© Fin)(πΉβπ) = π )) |
12 | 4, 11 | bitr4id 289 |
. . . . . 6
β’ (πΆ β (ACSβπ) β (βπ β (π« π β© Fin)π = (πΉβπ) β π β (πΉ β (π« π β© Fin)))) |
13 | 12 | ralbidv 3177 |
. . . . 5
β’ (πΆ β (ACSβπ) β (βπ β πΆ βπ β (π« π β© Fin)π = (πΉβπ) β βπ β πΆ π β (πΉ β (π« π β© Fin)))) |
14 | | dfss3 3970 |
. . . . 5
β’ (πΆ β (πΉ β (π« π β© Fin)) β βπ β πΆ π β (πΉ β (π« π β© Fin))) |
15 | 13, 14 | bitr4di 288 |
. . . 4
β’ (πΆ β (ACSβπ) β (βπ β πΆ βπ β (π« π β© Fin)π = (πΉβπ) β πΆ β (πΉ β (π« π β© Fin)))) |
16 | | imassrn 6070 |
. . . . . . 7
β’ (πΉ β (π« π β© Fin)) β ran πΉ |
17 | | frn 6724 |
. . . . . . . 8
β’ (πΉ:π« πβΆπΆ β ran πΉ β πΆ) |
18 | 5, 6, 17 | 3syl 18 |
. . . . . . 7
β’ (πΆ β (ACSβπ) β ran πΉ β πΆ) |
19 | 16, 18 | sstrid 3993 |
. . . . . 6
β’ (πΆ β (ACSβπ) β (πΉ β (π« π β© Fin)) β πΆ) |
20 | 19 | biantrurd 533 |
. . . . 5
β’ (πΆ β (ACSβπ) β (πΆ β (πΉ β (π« π β© Fin)) β ((πΉ β (π« π β© Fin)) β πΆ β§ πΆ β (πΉ β (π« π β© Fin))))) |
21 | | eqss 3997 |
. . . . 5
β’ ((πΉ β (π« π β© Fin)) = πΆ β ((πΉ β (π« π β© Fin)) β πΆ β§ πΆ β (πΉ β (π« π β© Fin)))) |
22 | 20, 21 | bitr4di 288 |
. . . 4
β’ (πΆ β (ACSβπ) β (πΆ β (πΉ β (π« π β© Fin)) β (πΉ β (π« π β© Fin)) = πΆ)) |
23 | 15, 22 | bitrd 278 |
. . 3
β’ (πΆ β (ACSβπ) β (βπ β πΆ βπ β (π« π β© Fin)π = (πΉβπ) β (πΉ β (π« π β© Fin)) = πΆ)) |
24 | 23 | pm5.32i 575 |
. 2
β’ ((πΆ β (ACSβπ) β§ βπ β πΆ βπ β (π« π β© Fin)π = (πΉβπ)) β (πΆ β (ACSβπ) β§ (πΉ β (π« π β© Fin)) = πΆ)) |
25 | 2, 24 | bitri 274 |
1
β’ (πΆ β (NoeACSβπ) β (πΆ β (ACSβπ) β§ (πΉ β (π« π β© Fin)) = πΆ)) |