Step | Hyp | Ref
| Expression |
1 | | isf32lem.f |
. . . 4
β’ πΎ = ((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€))) β π½) |
2 | 1 | fveq1i 6893 |
. . 3
β’ (πΎβπ΄) = (((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€))) β π½)βπ΄) |
3 | | isf32lem.d |
. . . . . . . 8
β’ π = {π¦ β Ο β£ (πΉβsuc π¦) β (πΉβπ¦)} |
4 | 3 | ssrab3 4081 |
. . . . . . 7
β’ π β
Ο |
5 | | isf32lem.a |
. . . . . . . 8
β’ (π β πΉ:ΟβΆπ« πΊ) |
6 | | isf32lem.b |
. . . . . . . 8
β’ (π β βπ₯ β Ο (πΉβsuc π₯) β (πΉβπ₯)) |
7 | | isf32lem.c |
. . . . . . . 8
β’ (π β Β¬ β© ran πΉ β ran πΉ) |
8 | 5, 6, 7, 3 | isf32lem5 10352 |
. . . . . . 7
β’ (π β Β¬ π β Fin) |
9 | | isf32lem.e |
. . . . . . . 8
β’ π½ = (π’ β Ο β¦ (β©π£ β π (π£ β© π) β π’)) |
10 | 9 | fin23lem22 10322 |
. . . . . . 7
β’ ((π β Ο β§ Β¬
π β Fin) β π½:Οβ1-1-ontoβπ) |
11 | 4, 8, 10 | sylancr 588 |
. . . . . 6
β’ (π β π½:Οβ1-1-ontoβπ) |
12 | | f1of 6834 |
. . . . . 6
β’ (π½:Οβ1-1-ontoβπ β π½:ΟβΆπ) |
13 | 11, 12 | syl 17 |
. . . . 5
β’ (π β π½:ΟβΆπ) |
14 | | fvco3 6991 |
. . . . 5
β’ ((π½:ΟβΆπ β§ π΄ β Ο) β (((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€))) β π½)βπ΄) = ((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€)))β(π½βπ΄))) |
15 | 13, 14 | sylan 581 |
. . . 4
β’ ((π β§ π΄ β Ο) β (((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€))) β π½)βπ΄) = ((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€)))β(π½βπ΄))) |
16 | 8 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π΄ β Ο) β Β¬ π β Fin) |
17 | 4, 16, 10 | sylancr 588 |
. . . . . . 7
β’ ((π β§ π΄ β Ο) β π½:Οβ1-1-ontoβπ) |
18 | 17, 12 | syl 17 |
. . . . . 6
β’ ((π β§ π΄ β Ο) β π½:ΟβΆπ) |
19 | | ffvelcdm 7084 |
. . . . . 6
β’ ((π½:ΟβΆπ β§ π΄ β Ο) β (π½βπ΄) β π) |
20 | 18, 19 | sylancom 589 |
. . . . 5
β’ ((π β§ π΄ β Ο) β (π½βπ΄) β π) |
21 | | fveq2 6892 |
. . . . . . 7
β’ (π€ = (π½βπ΄) β (πΉβπ€) = (πΉβ(π½βπ΄))) |
22 | | suceq 6431 |
. . . . . . . 8
β’ (π€ = (π½βπ΄) β suc π€ = suc (π½βπ΄)) |
23 | 22 | fveq2d 6896 |
. . . . . . 7
β’ (π€ = (π½βπ΄) β (πΉβsuc π€) = (πΉβsuc (π½βπ΄))) |
24 | 21, 23 | difeq12d 4124 |
. . . . . 6
β’ (π€ = (π½βπ΄) β ((πΉβπ€) β (πΉβsuc π€)) = ((πΉβ(π½βπ΄)) β (πΉβsuc (π½βπ΄)))) |
25 | | eqid 2733 |
. . . . . 6
β’ (π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€))) = (π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€))) |
26 | | fvex 6905 |
. . . . . . 7
β’ (πΉβ(π½βπ΄)) β V |
27 | 26 | difexi 5329 |
. . . . . 6
β’ ((πΉβ(π½βπ΄)) β (πΉβsuc (π½βπ΄))) β V |
28 | 24, 25, 27 | fvmpt 6999 |
. . . . 5
β’ ((π½βπ΄) β π β ((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€)))β(π½βπ΄)) = ((πΉβ(π½βπ΄)) β (πΉβsuc (π½βπ΄)))) |
29 | 20, 28 | syl 17 |
. . . 4
β’ ((π β§ π΄ β Ο) β ((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€)))β(π½βπ΄)) = ((πΉβ(π½βπ΄)) β (πΉβsuc (π½βπ΄)))) |
30 | 15, 29 | eqtrd 2773 |
. . 3
β’ ((π β§ π΄ β Ο) β (((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€))) β π½)βπ΄) = ((πΉβ(π½βπ΄)) β (πΉβsuc (π½βπ΄)))) |
31 | 2, 30 | eqtrid 2785 |
. 2
β’ ((π β§ π΄ β Ο) β (πΎβπ΄) = ((πΉβ(π½βπ΄)) β (πΉβsuc (π½βπ΄)))) |
32 | | suceq 6431 |
. . . . . . . . 9
β’ (π¦ = (π½βπ΄) β suc π¦ = suc (π½βπ΄)) |
33 | 32 | fveq2d 6896 |
. . . . . . . 8
β’ (π¦ = (π½βπ΄) β (πΉβsuc π¦) = (πΉβsuc (π½βπ΄))) |
34 | | fveq2 6892 |
. . . . . . . 8
β’ (π¦ = (π½βπ΄) β (πΉβπ¦) = (πΉβ(π½βπ΄))) |
35 | 33, 34 | psseq12d 4095 |
. . . . . . 7
β’ (π¦ = (π½βπ΄) β ((πΉβsuc π¦) β (πΉβπ¦) β (πΉβsuc (π½βπ΄)) β (πΉβ(π½βπ΄)))) |
36 | 35, 3 | elrab2 3687 |
. . . . . 6
β’ ((π½βπ΄) β π β ((π½βπ΄) β Ο β§ (πΉβsuc (π½βπ΄)) β (πΉβ(π½βπ΄)))) |
37 | 36 | simprbi 498 |
. . . . 5
β’ ((π½βπ΄) β π β (πΉβsuc (π½βπ΄)) β (πΉβ(π½βπ΄))) |
38 | 20, 37 | syl 17 |
. . . 4
β’ ((π β§ π΄ β Ο) β (πΉβsuc (π½βπ΄)) β (πΉβ(π½βπ΄))) |
39 | | df-pss 3968 |
. . . 4
β’ ((πΉβsuc (π½βπ΄)) β (πΉβ(π½βπ΄)) β ((πΉβsuc (π½βπ΄)) β (πΉβ(π½βπ΄)) β§ (πΉβsuc (π½βπ΄)) β (πΉβ(π½βπ΄)))) |
40 | 38, 39 | sylib 217 |
. . 3
β’ ((π β§ π΄ β Ο) β ((πΉβsuc (π½βπ΄)) β (πΉβ(π½βπ΄)) β§ (πΉβsuc (π½βπ΄)) β (πΉβ(π½βπ΄)))) |
41 | | pssdifn0 4366 |
. . 3
β’ (((πΉβsuc (π½βπ΄)) β (πΉβ(π½βπ΄)) β§ (πΉβsuc (π½βπ΄)) β (πΉβ(π½βπ΄))) β ((πΉβ(π½βπ΄)) β (πΉβsuc (π½βπ΄))) β β
) |
42 | 40, 41 | syl 17 |
. 2
β’ ((π β§ π΄ β Ο) β ((πΉβ(π½βπ΄)) β (πΉβsuc (π½βπ΄))) β β
) |
43 | 31, 42 | eqnetrd 3009 |
1
β’ ((π β§ π΄ β Ο) β (πΎβπ΄) β β
) |