Step | Hyp | Ref
| Expression |
1 | | isf32lem.f |
. . . . 5
β’ πΎ = ((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€))) β π½) |
2 | 1 | fveq1i 6893 |
. . . 4
β’ (πΎβπ΄) = (((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€))) β π½)βπ΄) |
3 | | isf32lem.d |
. . . . . . . . . 10
β’ π = {π¦ β Ο β£ (πΉβsuc π¦) β (πΉβπ¦)} |
4 | 3 | ssrab3 4081 |
. . . . . . . . 9
β’ π β
Ο |
5 | | isf32lem.a |
. . . . . . . . . 10
β’ (π β πΉ:ΟβΆπ« πΊ) |
6 | | isf32lem.b |
. . . . . . . . . 10
β’ (π β βπ₯ β Ο (πΉβsuc π₯) β (πΉβπ₯)) |
7 | | isf32lem.c |
. . . . . . . . . 10
β’ (π β Β¬ β© ran πΉ β ran πΉ) |
8 | 5, 6, 7, 3 | isf32lem5 10352 |
. . . . . . . . 9
β’ (π β Β¬ π β Fin) |
9 | | isf32lem.e |
. . . . . . . . . 10
β’ π½ = (π’ β Ο β¦ (β©π£ β π (π£ β© π) β π’)) |
10 | 9 | fin23lem22 10322 |
. . . . . . . . 9
β’ ((π β Ο β§ Β¬
π β Fin) β π½:Οβ1-1-ontoβπ) |
11 | 4, 8, 10 | sylancr 588 |
. . . . . . . 8
β’ (π β π½:Οβ1-1-ontoβπ) |
12 | | f1of 6834 |
. . . . . . . 8
β’ (π½:Οβ1-1-ontoβπ β π½:ΟβΆπ) |
13 | 11, 12 | syl 17 |
. . . . . . 7
β’ (π β π½:ΟβΆπ) |
14 | | fvco3 6991 |
. . . . . . 7
β’ ((π½:ΟβΆπ β§ π΄ β Ο) β (((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€))) β π½)βπ΄) = ((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€)))β(π½βπ΄))) |
15 | 13, 14 | sylan 581 |
. . . . . 6
β’ ((π β§ π΄ β Ο) β (((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€))) β π½)βπ΄) = ((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€)))β(π½βπ΄))) |
16 | 15 | ad2ant2r 746 |
. . . . 5
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β (((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€))) β π½)βπ΄) = ((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€)))β(π½βπ΄))) |
17 | 13 | adantr 482 |
. . . . . . 7
β’ ((π β§ π΄ β π΅) β π½:ΟβΆπ) |
18 | | simpl 484 |
. . . . . . 7
β’ ((π΄ β Ο β§ π΅ β Ο) β π΄ β
Ο) |
19 | | ffvelcdm 7084 |
. . . . . . 7
β’ ((π½:ΟβΆπ β§ π΄ β Ο) β (π½βπ΄) β π) |
20 | 17, 18, 19 | syl2an 597 |
. . . . . 6
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β (π½βπ΄) β π) |
21 | | fveq2 6892 |
. . . . . . . 8
β’ (π€ = (π½βπ΄) β (πΉβπ€) = (πΉβ(π½βπ΄))) |
22 | | suceq 6431 |
. . . . . . . . 9
β’ (π€ = (π½βπ΄) β suc π€ = suc (π½βπ΄)) |
23 | 22 | fveq2d 6896 |
. . . . . . . 8
β’ (π€ = (π½βπ΄) β (πΉβsuc π€) = (πΉβsuc (π½βπ΄))) |
24 | 21, 23 | difeq12d 4124 |
. . . . . . 7
β’ (π€ = (π½βπ΄) β ((πΉβπ€) β (πΉβsuc π€)) = ((πΉβ(π½βπ΄)) β (πΉβsuc (π½βπ΄)))) |
25 | | eqid 2733 |
. . . . . . 7
β’ (π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€))) = (π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€))) |
26 | | fvex 6905 |
. . . . . . . 8
β’ (πΉβ(π½βπ΄)) β V |
27 | 26 | difexi 5329 |
. . . . . . 7
β’ ((πΉβ(π½βπ΄)) β (πΉβsuc (π½βπ΄))) β V |
28 | 24, 25, 27 | fvmpt 6999 |
. . . . . 6
β’ ((π½βπ΄) β π β ((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€)))β(π½βπ΄)) = ((πΉβ(π½βπ΄)) β (πΉβsuc (π½βπ΄)))) |
29 | 20, 28 | syl 17 |
. . . . 5
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β ((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€)))β(π½βπ΄)) = ((πΉβ(π½βπ΄)) β (πΉβsuc (π½βπ΄)))) |
30 | 16, 29 | eqtrd 2773 |
. . . 4
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β (((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€))) β π½)βπ΄) = ((πΉβ(π½βπ΄)) β (πΉβsuc (π½βπ΄)))) |
31 | 2, 30 | eqtrid 2785 |
. . 3
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β (πΎβπ΄) = ((πΉβ(π½βπ΄)) β (πΉβsuc (π½βπ΄)))) |
32 | 1 | fveq1i 6893 |
. . . 4
β’ (πΎβπ΅) = (((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€))) β π½)βπ΅) |
33 | | fvco3 6991 |
. . . . . . 7
β’ ((π½:ΟβΆπ β§ π΅ β Ο) β (((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€))) β π½)βπ΅) = ((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€)))β(π½βπ΅))) |
34 | 13, 33 | sylan 581 |
. . . . . 6
β’ ((π β§ π΅ β Ο) β (((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€))) β π½)βπ΅) = ((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€)))β(π½βπ΅))) |
35 | 34 | ad2ant2rl 748 |
. . . . 5
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β (((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€))) β π½)βπ΅) = ((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€)))β(π½βπ΅))) |
36 | | simpr 486 |
. . . . . . 7
β’ ((π΄ β Ο β§ π΅ β Ο) β π΅ β
Ο) |
37 | | ffvelcdm 7084 |
. . . . . . 7
β’ ((π½:ΟβΆπ β§ π΅ β Ο) β (π½βπ΅) β π) |
38 | 17, 36, 37 | syl2an 597 |
. . . . . 6
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β (π½βπ΅) β π) |
39 | | fveq2 6892 |
. . . . . . . 8
β’ (π€ = (π½βπ΅) β (πΉβπ€) = (πΉβ(π½βπ΅))) |
40 | | suceq 6431 |
. . . . . . . . 9
β’ (π€ = (π½βπ΅) β suc π€ = suc (π½βπ΅)) |
41 | 40 | fveq2d 6896 |
. . . . . . . 8
β’ (π€ = (π½βπ΅) β (πΉβsuc π€) = (πΉβsuc (π½βπ΅))) |
42 | 39, 41 | difeq12d 4124 |
. . . . . . 7
β’ (π€ = (π½βπ΅) β ((πΉβπ€) β (πΉβsuc π€)) = ((πΉβ(π½βπ΅)) β (πΉβsuc (π½βπ΅)))) |
43 | | fvex 6905 |
. . . . . . . 8
β’ (πΉβ(π½βπ΅)) β V |
44 | 43 | difexi 5329 |
. . . . . . 7
β’ ((πΉβ(π½βπ΅)) β (πΉβsuc (π½βπ΅))) β V |
45 | 42, 25, 44 | fvmpt 6999 |
. . . . . 6
β’ ((π½βπ΅) β π β ((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€)))β(π½βπ΅)) = ((πΉβ(π½βπ΅)) β (πΉβsuc (π½βπ΅)))) |
46 | 38, 45 | syl 17 |
. . . . 5
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β ((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€)))β(π½βπ΅)) = ((πΉβ(π½βπ΅)) β (πΉβsuc (π½βπ΅)))) |
47 | 35, 46 | eqtrd 2773 |
. . . 4
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β (((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€))) β π½)βπ΅) = ((πΉβ(π½βπ΅)) β (πΉβsuc (π½βπ΅)))) |
48 | 32, 47 | eqtrid 2785 |
. . 3
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β (πΎβπ΅) = ((πΉβ(π½βπ΅)) β (πΉβsuc (π½βπ΅)))) |
49 | 31, 48 | ineq12d 4214 |
. 2
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β ((πΎβπ΄) β© (πΎβπ΅)) = (((πΉβ(π½βπ΄)) β (πΉβsuc (π½βπ΄))) β© ((πΉβ(π½βπ΅)) β (πΉβsuc (π½βπ΅))))) |
50 | | simpll 766 |
. . 3
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β π) |
51 | | simplr 768 |
. . . 4
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β π΄ β π΅) |
52 | | f1of1 6833 |
. . . . . . . . 9
β’ (π½:Οβ1-1-ontoβπ β π½:Οβ1-1βπ) |
53 | 11, 52 | syl 17 |
. . . . . . . 8
β’ (π β π½:Οβ1-1βπ) |
54 | 53 | adantr 482 |
. . . . . . 7
β’ ((π β§ π΄ β π΅) β π½:Οβ1-1βπ) |
55 | | f1fveq 7261 |
. . . . . . 7
β’ ((π½:Οβ1-1βπ β§ (π΄ β Ο β§ π΅ β Ο)) β ((π½βπ΄) = (π½βπ΅) β π΄ = π΅)) |
56 | 54, 55 | sylan 581 |
. . . . . 6
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β ((π½βπ΄) = (π½βπ΅) β π΄ = π΅)) |
57 | 56 | biimpd 228 |
. . . . 5
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β ((π½βπ΄) = (π½βπ΅) β π΄ = π΅)) |
58 | 57 | necon3d 2962 |
. . . 4
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β (π΄ β π΅ β (π½βπ΄) β (π½βπ΅))) |
59 | 51, 58 | mpd 15 |
. . 3
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β (π½βπ΄) β (π½βπ΅)) |
60 | 4, 20 | sselid 3981 |
. . 3
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β (π½βπ΄) β Ο) |
61 | 4, 38 | sselid 3981 |
. . 3
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β (π½βπ΅) β Ο) |
62 | 5, 6, 7 | isf32lem4 10351 |
. . 3
β’ (((π β§ (π½βπ΄) β (π½βπ΅)) β§ ((π½βπ΄) β Ο β§ (π½βπ΅) β Ο)) β (((πΉβ(π½βπ΄)) β (πΉβsuc (π½βπ΄))) β© ((πΉβ(π½βπ΅)) β (πΉβsuc (π½βπ΅)))) = β
) |
63 | 50, 59, 60, 61, 62 | syl22anc 838 |
. 2
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β (((πΉβ(π½βπ΄)) β (πΉβsuc (π½βπ΄))) β© ((πΉβ(π½βπ΅)) β (πΉβsuc (π½βπ΅)))) = β
) |
64 | 49, 63 | eqtrd 2773 |
1
β’ (((π β§ π΄ β π΅) β§ (π΄ β Ο β§ π΅ β Ο)) β ((πΎβπ΄) β© (πΎβπ΅)) = β
) |