Step | Hyp | Ref
| Expression |
1 | | isnacs.f |
. . . . . . . . 9
β’ πΉ = (mrClsβπΆ) |
2 | 1 | mrcssid 17502 |
. . . . . . . 8
β’ ((πΆ β (Mooreβπ) β§ π β π) β π β (πΉβπ)) |
3 | | simpr 486 |
. . . . . . . . 9
β’ ((πΆ β (Mooreβπ) β§ π β (πΉβπ)) β π β (πΉβπ)) |
4 | 1 | mrcssv 17499 |
. . . . . . . . . 10
β’ (πΆ β (Mooreβπ) β (πΉβπ) β π) |
5 | 4 | adantr 482 |
. . . . . . . . 9
β’ ((πΆ β (Mooreβπ) β§ π β (πΉβπ)) β (πΉβπ) β π) |
6 | 3, 5 | sstrd 3955 |
. . . . . . . 8
β’ ((πΆ β (Mooreβπ) β§ π β (πΉβπ)) β π β π) |
7 | 2, 6 | impbida 800 |
. . . . . . 7
β’ (πΆ β (Mooreβπ) β (π β π β π β (πΉβπ))) |
8 | | vex 3448 |
. . . . . . . 8
β’ π β V |
9 | 8 | elpw 4565 |
. . . . . . 7
β’ (π β π« π β π β π) |
10 | 8 | elpw 4565 |
. . . . . . 7
β’ (π β π« (πΉβπ) β π β (πΉβπ)) |
11 | 7, 9, 10 | 3bitr4g 314 |
. . . . . 6
β’ (πΆ β (Mooreβπ) β (π β π« π β π β π« (πΉβπ))) |
12 | 11 | anbi1d 631 |
. . . . 5
β’ (πΆ β (Mooreβπ) β ((π β π« π β§ π β Fin) β (π β π« (πΉβπ) β§ π β Fin))) |
13 | | elin 3927 |
. . . . 5
β’ (π β (π« π β© Fin) β (π β π« π β§ π β Fin)) |
14 | | elin 3927 |
. . . . 5
β’ (π β (π« (πΉβπ) β© Fin) β (π β π« (πΉβπ) β§ π β Fin)) |
15 | 12, 13, 14 | 3bitr4g 314 |
. . . 4
β’ (πΆ β (Mooreβπ) β (π β (π« π β© Fin) β π β (π« (πΉβπ) β© Fin))) |
16 | | pweq 4575 |
. . . . . . 7
β’ (π = (πΉβπ) β π« π = π« (πΉβπ)) |
17 | 16 | ineq1d 4172 |
. . . . . 6
β’ (π = (πΉβπ) β (π« π β© Fin) = (π« (πΉβπ) β© Fin)) |
18 | 17 | eleq2d 2820 |
. . . . 5
β’ (π = (πΉβπ) β (π β (π« π β© Fin) β π β (π« (πΉβπ) β© Fin))) |
19 | 18 | bibi2d 343 |
. . . 4
β’ (π = (πΉβπ) β ((π β (π« π β© Fin) β π β (π« π β© Fin)) β (π β (π« π β© Fin) β π β (π« (πΉβπ) β© Fin)))) |
20 | 15, 19 | syl5ibrcom 247 |
. . 3
β’ (πΆ β (Mooreβπ) β (π = (πΉβπ) β (π β (π« π β© Fin) β π β (π« π β© Fin)))) |
21 | 20 | pm5.32rd 579 |
. 2
β’ (πΆ β (Mooreβπ) β ((π β (π« π β© Fin) β§ π = (πΉβπ)) β (π β (π« π β© Fin) β§ π = (πΉβπ)))) |
22 | 21 | rexbidv2 3168 |
1
β’ (πΆ β (Mooreβπ) β (βπ β (π« π β© Fin)π = (πΉβπ) β βπ β (π« π β© Fin)π = (πΉβπ))) |