| Step | Hyp | Ref
| Expression |
|---|
| 1 | | simp1 1135 |
. . 3
β’ ((πΉ:ΟβΆπ« πΊ β§ βπ β Ο (πΉβsuc π) β (πΉβπ) β§ Β¬ β©
ran πΉ β ran πΉ) β πΉ:ΟβΆπ« πΊ) |
| 2 | | suceq 6431 |
. . . . . . . 8
β’ (π = π β suc π = suc π) |
| 3 | 2 | fveq2d 6896 |
. . . . . . 7
β’ (π = π β (πΉβsuc π) = (πΉβsuc π)) |
| 4 | | fveq2 6892 |
. . . . . . 7
β’ (π = π β (πΉβπ) = (πΉβπ)) |
| 5 | 3, 4 | sseq12d 4016 |
. . . . . 6
β’ (π = π β ((πΉβsuc π) β (πΉβπ) β (πΉβsuc π) β (πΉβπ))) |
| 6 | 5 | cbvralvw 3233 |
. . . . 5
β’
(βπ β
Ο (πΉβsuc π) β (πΉβπ) β βπ β Ο (πΉβsuc π) β (πΉβπ)) |
| 7 | 6 | biimpi 215 |
. . . 4
β’
(βπ β
Ο (πΉβsuc π) β (πΉβπ) β βπ β Ο (πΉβsuc π) β (πΉβπ)) |
| 8 | 7 | 3ad2ant2 1133 |
. . 3
β’ ((πΉ:ΟβΆπ« πΊ β§ βπ β Ο (πΉβsuc π) β (πΉβπ) β§ Β¬ β©
ran πΉ β ran πΉ) β βπ β Ο (πΉβsuc π) β (πΉβπ)) |
| 9 | | simp3 1137 |
. . 3
β’ ((πΉ:ΟβΆπ« πΊ β§ βπ β Ο (πΉβsuc π) β (πΉβπ) β§ Β¬ β©
ran πΉ β ran πΉ) β Β¬ β© ran πΉ β ran πΉ) |
| 10 | | suceq 6431 |
. . . . . 6
β’ (π = π β suc π = suc π) |
| 11 | 10 | fveq2d 6896 |
. . . . 5
β’ (π = π β (πΉβsuc π) = (πΉβsuc π)) |
| 12 | | fveq2 6892 |
. . . . 5
β’ (π = π β (πΉβπ) = (πΉβπ)) |
| 13 | 11, 12 | psseq12d 4095 |
. . . 4
β’ (π = π β ((πΉβsuc π) β (πΉβπ) β (πΉβsuc π) β (πΉβπ))) |
| 14 | 13 | cbvrabv 3441 |
. . 3
β’ {π β Ο β£ (πΉβsuc π) β (πΉβπ)} = {π β Ο β£ (πΉβsuc π) β (πΉβπ)} |
| 15 | | eqid 2731 |
. . 3
β’ (π β Ο β¦
(β©π β
{π β Ο β£
(πΉβsuc π) β (πΉβπ)} (π β© {π β Ο β£ (πΉβsuc π) β (πΉβπ)}) β π)) = (π β Ο β¦ (β©π β {π β Ο β£ (πΉβsuc π) β (πΉβπ)} (π β© {π β Ο β£ (πΉβsuc π) β (πΉβπ)}) β π)) |
| 16 | | eqid 2731 |
. . 3
β’ ((β β {π β Ο β£ (πΉβsuc π) β (πΉβπ)} β¦ ((πΉββ) β (πΉβsuc β))) β (π β Ο β¦ (β©π β {π β Ο β£ (πΉβsuc π) β (πΉβπ)} (π β© {π β Ο β£ (πΉβsuc π) β (πΉβπ)}) β π))) = ((β β {π β Ο β£ (πΉβsuc π) β (πΉβπ)} β¦ ((πΉββ) β (πΉβsuc β))) β (π β Ο β¦ (β©π β {π β Ο β£ (πΉβsuc π) β (πΉβπ)} (π β© {π β Ο β£ (πΉβsuc π) β (πΉβπ)}) β π))) |
| 17 | | eqid 2731 |
. . 3
β’ (π β πΊ β¦ (β©π(π β Ο β§ π β (((β β {π β Ο β£ (πΉβsuc π) β (πΉβπ)} β¦ ((πΉββ) β (πΉβsuc β))) β (π β Ο β¦ (β©π β {π β Ο β£ (πΉβsuc π) β (πΉβπ)} (π β© {π β Ο β£ (πΉβsuc π) β (πΉβπ)}) β π)))βπ)))) = (π β πΊ β¦ (β©π(π β Ο β§ π β (((β β {π β Ο β£ (πΉβsuc π) β (πΉβπ)} β¦ ((πΉββ) β (πΉβsuc β))) β (π β Ο β¦ (β©π β {π β Ο β£ (πΉβsuc π) β (πΉβπ)} (π β© {π β Ο β£ (πΉβsuc π) β (πΉβπ)}) β π)))βπ)))) |
| 18 | 1, 8, 9, 14, 15, 16, 17 | isf32lem10 10360 |
. 2
β’ ((πΉ:ΟβΆπ« πΊ β§ βπ β Ο (πΉβsuc π) β (πΉβπ) β§ Β¬ β©
ran πΉ β ran πΉ) β (πΊ β π β Ο βΌ* πΊ)) |
| 19 | 18 | impcom 407 |
1
β’ ((πΊ β π β§ (πΉ:ΟβΆπ« πΊ β§ βπ β Ο (πΉβsuc π) β (πΉβπ) β§ Β¬ β©
ran πΉ β ran πΉ)) β Ο
βΌ* πΊ) |
