Step | Hyp | Ref
| Expression |
1 | | mrissmrcd.1 |
. . . . . 6
β’ (π β π΄ β (Mooreβπ)) |
2 | | mrissmrcd.2 |
. . . . . 6
β’ π = (mrClsβπ΄) |
3 | | mrissmrcd.4 |
. . . . . 6
β’ (π β π β (πβπ)) |
4 | | mrissmrcd.5 |
. . . . . 6
β’ (π β π β π) |
5 | 1, 2, 3, 4 | mressmrcd 17571 |
. . . . 5
β’ (π β (πβπ) = (πβπ)) |
6 | | pssne 4097 |
. . . . . . 7
β’ ((πβπ) β (πβπ) β (πβπ) β (πβπ)) |
7 | 6 | necomd 2997 |
. . . . . 6
β’ ((πβπ) β (πβπ) β (πβπ) β (πβπ)) |
8 | 7 | necon2bi 2972 |
. . . . 5
β’ ((πβπ) = (πβπ) β Β¬ (πβπ) β (πβπ)) |
9 | 5, 8 | syl 17 |
. . . 4
β’ (π β Β¬ (πβπ) β (πβπ)) |
10 | | mrissmrcd.6 |
. . . . . 6
β’ (π β π β πΌ) |
11 | | mrissmrcd.3 |
. . . . . . 7
β’ πΌ = (mrIndβπ΄) |
12 | 11, 1, 10 | mrissd 17580 |
. . . . . . 7
β’ (π β π β π) |
13 | 1, 2, 11, 12 | mrieqv2d 17583 |
. . . . . 6
β’ (π β (π β πΌ β βπ (π β π β (πβπ ) β (πβπ)))) |
14 | 10, 13 | mpbid 231 |
. . . . 5
β’ (π β βπ (π β π β (πβπ ) β (πβπ))) |
15 | 10, 4 | ssexd 5325 |
. . . . . 6
β’ (π β π β V) |
16 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π = π) β π = π) |
17 | 16 | psseq1d 4093 |
. . . . . . 7
β’ ((π β§ π = π) β (π β π β π β π)) |
18 | 16 | fveq2d 6896 |
. . . . . . . 8
β’ ((π β§ π = π) β (πβπ ) = (πβπ)) |
19 | 18 | psseq1d 4093 |
. . . . . . 7
β’ ((π β§ π = π) β ((πβπ ) β (πβπ) β (πβπ) β (πβπ))) |
20 | 17, 19 | imbi12d 345 |
. . . . . 6
β’ ((π β§ π = π) β ((π β π β (πβπ ) β (πβπ)) β (π β π β (πβπ) β (πβπ)))) |
21 | 15, 20 | spcdv 3585 |
. . . . 5
β’ (π β (βπ (π β π β (πβπ ) β (πβπ)) β (π β π β (πβπ) β (πβπ)))) |
22 | 14, 21 | mpd 15 |
. . . 4
β’ (π β (π β π β (πβπ) β (πβπ))) |
23 | 9, 22 | mtod 197 |
. . 3
β’ (π β Β¬ π β π) |
24 | | sspss 4100 |
. . . . 5
β’ (π β π β (π β π β¨ π = π)) |
25 | 4, 24 | sylib 217 |
. . . 4
β’ (π β (π β π β¨ π = π)) |
26 | 25 | ord 863 |
. . 3
β’ (π β (Β¬ π β π β π = π)) |
27 | 23, 26 | mpd 15 |
. 2
β’ (π β π = π) |
28 | 27 | eqcomd 2739 |
1
β’ (π β π = π) |