Step | Hyp | Ref
| Expression |
1 | | isnacs.f |
. . . 4
β’ πΉ = (mrClsβπΆ) |
2 | 1 | mrefg2 41445 |
. . 3
β’ (πΆ β (Mooreβπ) β (βπ β (π« π β© Fin)π = (πΉβπ) β βπ β (π« π β© Fin)π = (πΉβπ))) |
3 | 2 | adantr 482 |
. 2
β’ ((πΆ β (Mooreβπ) β§ π β πΆ) β (βπ β (π« π β© Fin)π = (πΉβπ) β βπ β (π« π β© Fin)π = (πΉβπ))) |
4 | | eqss 3998 |
. . . 4
β’ (π = (πΉβπ) β (π β (πΉβπ) β§ (πΉβπ) β π)) |
5 | | simpll 766 |
. . . . . 6
β’ (((πΆ β (Mooreβπ) β§ π β πΆ) β§ π β (π« π β© Fin)) β πΆ β (Mooreβπ)) |
6 | | inss1 4229 |
. . . . . . . . 9
β’
(π« π β©
Fin) β π« π |
7 | 6 | sseli 3979 |
. . . . . . . 8
β’ (π β (π« π β© Fin) β π β π« π) |
8 | 7 | elpwid 4612 |
. . . . . . 7
β’ (π β (π« π β© Fin) β π β π) |
9 | 8 | adantl 483 |
. . . . . 6
β’ (((πΆ β (Mooreβπ) β§ π β πΆ) β§ π β (π« π β© Fin)) β π β π) |
10 | | simplr 768 |
. . . . . 6
β’ (((πΆ β (Mooreβπ) β§ π β πΆ) β§ π β (π« π β© Fin)) β π β πΆ) |
11 | 1 | mrcsscl 17564 |
. . . . . 6
β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β πΆ) β (πΉβπ) β π) |
12 | 5, 9, 10, 11 | syl3anc 1372 |
. . . . 5
β’ (((πΆ β (Mooreβπ) β§ π β πΆ) β§ π β (π« π β© Fin)) β (πΉβπ) β π) |
13 | 12 | biantrud 533 |
. . . 4
β’ (((πΆ β (Mooreβπ) β§ π β πΆ) β§ π β (π« π β© Fin)) β (π β (πΉβπ) β (π β (πΉβπ) β§ (πΉβπ) β π))) |
14 | 4, 13 | bitr4id 290 |
. . 3
β’ (((πΆ β (Mooreβπ) β§ π β πΆ) β§ π β (π« π β© Fin)) β (π = (πΉβπ) β π β (πΉβπ))) |
15 | 14 | rexbidva 3177 |
. 2
β’ ((πΆ β (Mooreβπ) β§ π β πΆ) β (βπ β (π« π β© Fin)π = (πΉβπ) β βπ β (π« π β© Fin)π β (πΉβπ))) |
16 | 3, 15 | bitrd 279 |
1
β’ ((πΆ β (Mooreβπ) β§ π β πΆ) β (βπ β (π« π β© Fin)π = (πΉβπ) β βπ β (π« π β© Fin)π β (πΉβπ))) |