Step | Hyp | Ref
| Expression |
1 | | isnacs.f |
. . . 4
β’ πΉ = (mrClsβπΆ) |
2 | 1 | mrefg2 42004 |
. . 3
β’ (πΆ β (Mooreβπ) β (βπ β (π« π β© Fin)π = (πΉβπ) β βπ β (π« π β© Fin)π = (πΉβπ))) |
3 | 2 | adantr 480 |
. 2
β’ ((πΆ β (Mooreβπ) β§ π β πΆ) β (βπ β (π« π β© Fin)π = (πΉβπ) β βπ β (π« π β© Fin)π = (πΉβπ))) |
4 | | eqss 3992 |
. . . 4
β’ (π = (πΉβπ) β (π β (πΉβπ) β§ (πΉβπ) β π)) |
5 | | simpll 764 |
. . . . . 6
β’ (((πΆ β (Mooreβπ) β§ π β πΆ) β§ π β (π« π β© Fin)) β πΆ β (Mooreβπ)) |
6 | | inss1 4223 |
. . . . . . . . 9
β’
(π« π β©
Fin) β π« π |
7 | 6 | sseli 3973 |
. . . . . . . 8
β’ (π β (π« π β© Fin) β π β π« π) |
8 | 7 | elpwid 4606 |
. . . . . . 7
β’ (π β (π« π β© Fin) β π β π) |
9 | 8 | adantl 481 |
. . . . . 6
β’ (((πΆ β (Mooreβπ) β§ π β πΆ) β§ π β (π« π β© Fin)) β π β π) |
10 | | simplr 766 |
. . . . . 6
β’ (((πΆ β (Mooreβπ) β§ π β πΆ) β§ π β (π« π β© Fin)) β π β πΆ) |
11 | 1 | mrcsscl 17571 |
. . . . . 6
β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β πΆ) β (πΉβπ) β π) |
12 | 5, 9, 10, 11 | syl3anc 1368 |
. . . . 5
β’ (((πΆ β (Mooreβπ) β§ π β πΆ) β§ π β (π« π β© Fin)) β (πΉβπ) β π) |
13 | 12 | biantrud 531 |
. . . 4
β’ (((πΆ β (Mooreβπ) β§ π β πΆ) β§ π β (π« π β© Fin)) β (π β (πΉβπ) β (π β (πΉβπ) β§ (πΉβπ) β π))) |
14 | 4, 13 | bitr4id 290 |
. . 3
β’ (((πΆ β (Mooreβπ) β§ π β πΆ) β§ π β (π« π β© Fin)) β (π = (πΉβπ) β π β (πΉβπ))) |
15 | 14 | rexbidva 3170 |
. 2
β’ ((πΆ β (Mooreβπ) β§ π β πΆ) β (βπ β (π« π β© Fin)π = (πΉβπ) β βπ β (π« π β© Fin)π β (πΉβπ))) |
16 | 3, 15 | bitrd 279 |
1
β’ ((πΆ β (Mooreβπ) β§ π β πΆ) β (βπ β (π« π β© Fin)π = (πΉβπ) β βπ β (π« π β© Fin)π β (πΉβπ))) |