Step | Hyp | Ref
| Expression |
1 | | metakunt25.1 |
. . 3
β’ (π β π β β) |
2 | | metakunt25.2 |
. . 3
β’ (π β πΌ β β) |
3 | | metakunt25.3 |
. . 3
β’ (π β πΌ β€ π) |
4 | | eqid 2733 |
. . 3
β’ (π₯ β (1...(πΌ β 1)) β¦ (π₯ + (π β πΌ))) = (π₯ β (1...(πΌ β 1)) β¦ (π₯ + (π β πΌ))) |
5 | 1, 2, 3, 4 | metakunt15 40637 |
. 2
β’ (π β (π₯ β (1...(πΌ β 1)) β¦ (π₯ + (π β πΌ))):(1...(πΌ β 1))β1-1-ontoβ(((π β πΌ) + 1)...(π β 1))) |
6 | | eqid 2733 |
. . 3
β’ (π₯ β (πΌ...(π β 1)) β¦ (π₯ + (1 β πΌ))) = (π₯ β (πΌ...(π β 1)) β¦ (π₯ + (1 β πΌ))) |
7 | 1, 2, 3, 6 | metakunt16 40638 |
. 2
β’ (π β (π₯ β (πΌ...(π β 1)) β¦ (π₯ + (1 β πΌ))):(πΌ...(π β 1))β1-1-ontoβ(1...(π β πΌ))) |
8 | | f1osng 6826 |
. . 3
β’ ((π β β β§ π β β) β
{β¨π, πβ©}:{π}β1-1-ontoβ{π}) |
9 | 1, 1, 8 | syl2anc 585 |
. 2
β’ (π β {β¨π, πβ©}:{π}β1-1-ontoβ{π}) |
10 | 1, 2, 3 | metakunt18 40640 |
. . . 4
β’ (π β ((((1...(πΌ β 1)) β© (πΌ...(π β 1))) = β
β§ ((1...(πΌ β 1)) β© {π}) = β
β§ ((πΌ...(π β 1)) β© {π}) = β
) β§ (((((π β πΌ) + 1)...(π β 1)) β© (1...(π β πΌ))) = β
β§ ((((π β πΌ) + 1)...(π β 1)) β© {π}) = β
β§ ((1...(π β πΌ)) β© {π}) = β
))) |
11 | 10 | simpld 496 |
. . 3
β’ (π β (((1...(πΌ β 1)) β© (πΌ...(π β 1))) = β
β§ ((1...(πΌ β 1)) β© {π}) = β
β§ ((πΌ...(π β 1)) β© {π}) = β
)) |
12 | 11 | simp1d 1143 |
. 2
β’ (π β ((1...(πΌ β 1)) β© (πΌ...(π β 1))) = β
) |
13 | 11 | simp2d 1144 |
. 2
β’ (π β ((1...(πΌ β 1)) β© {π}) = β
) |
14 | 11 | simp3d 1145 |
. 2
β’ (π β ((πΌ...(π β 1)) β© {π}) = β
) |
15 | 10 | simprd 497 |
. . 3
β’ (π β (((((π β πΌ) + 1)...(π β 1)) β© (1...(π β πΌ))) = β
β§ ((((π β πΌ) + 1)...(π β 1)) β© {π}) = β
β§ ((1...(π β πΌ)) β© {π}) = β
)) |
16 | 15 | simp1d 1143 |
. 2
β’ (π β ((((π β πΌ) + 1)...(π β 1)) β© (1...(π β πΌ))) = β
) |
17 | 15 | simp2d 1144 |
. 2
β’ (π β ((((π β πΌ) + 1)...(π β 1)) β© {π}) = β
) |
18 | 15 | simp3d 1145 |
. 2
β’ (π β ((1...(π β πΌ)) β© {π}) = β
) |
19 | | eleq1 2822 |
. . . . . 6
β’ (π = if(π₯ = π, π, if(π₯ < πΌ, (π₯ + (π β πΌ)), (π₯ + (1 β πΌ)))) β (π β β€ β if(π₯ = π, π, if(π₯ < πΌ, (π₯ + (π β πΌ)), (π₯ + (1 β πΌ)))) β β€)) |
20 | | eleq1 2822 |
. . . . . 6
β’ (if(π₯ < πΌ, (π₯ + (π β πΌ)), (π₯ + (1 β πΌ))) = if(π₯ = π, π, if(π₯ < πΌ, (π₯ + (π β πΌ)), (π₯ + (1 β πΌ)))) β (if(π₯ < πΌ, (π₯ + (π β πΌ)), (π₯ + (1 β πΌ))) β β€ β if(π₯ = π, π, if(π₯ < πΌ, (π₯ + (π β πΌ)), (π₯ + (1 β πΌ)))) β β€)) |
21 | 1 | nnzd 12531 |
. . . . . . . 8
β’ (π β π β β€) |
22 | 21 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β (1...π)) β π β β€) |
23 | 22 | adantr 482 |
. . . . . 6
β’ (((π β§ π₯ β (1...π)) β§ π₯ = π) β π β β€) |
24 | | eleq1 2822 |
. . . . . . 7
β’ ((π₯ + (π β πΌ)) = if(π₯ < πΌ, (π₯ + (π β πΌ)), (π₯ + (1 β πΌ))) β ((π₯ + (π β πΌ)) β β€ β if(π₯ < πΌ, (π₯ + (π β πΌ)), (π₯ + (1 β πΌ))) β β€)) |
25 | | eleq1 2822 |
. . . . . . 7
β’ ((π₯ + (1 β πΌ)) = if(π₯ < πΌ, (π₯ + (π β πΌ)), (π₯ + (1 β πΌ))) β ((π₯ + (1 β πΌ)) β β€ β if(π₯ < πΌ, (π₯ + (π β πΌ)), (π₯ + (1 β πΌ))) β β€)) |
26 | | elfzelz 13447 |
. . . . . . . . . . 11
β’ (π₯ β (1...π) β π₯ β β€) |
27 | 26 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1...π)) β π₯ β β€) |
28 | 27 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π₯ β (1...π)) β§ Β¬ π₯ = π) β π₯ β β€) |
29 | 28 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ π₯ β (1...π)) β§ Β¬ π₯ = π) β§ π₯ < πΌ) β π₯ β β€) |
30 | 22 | ad2antrr 725 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (1...π)) β§ Β¬ π₯ = π) β§ π₯ < πΌ) β π β β€) |
31 | 2 | nnzd 12531 |
. . . . . . . . . . . 12
β’ (π β πΌ β β€) |
32 | 31 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1...π)) β πΌ β β€) |
33 | 32 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (1...π)) β§ Β¬ π₯ = π) β πΌ β β€) |
34 | 33 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (1...π)) β§ Β¬ π₯ = π) β§ π₯ < πΌ) β πΌ β β€) |
35 | 30, 34 | zsubcld 12617 |
. . . . . . . 8
β’ ((((π β§ π₯ β (1...π)) β§ Β¬ π₯ = π) β§ π₯ < πΌ) β (π β πΌ) β β€) |
36 | 29, 35 | zaddcld 12616 |
. . . . . . 7
β’ ((((π β§ π₯ β (1...π)) β§ Β¬ π₯ = π) β§ π₯ < πΌ) β (π₯ + (π β πΌ)) β β€) |
37 | 28 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ π₯ β (1...π)) β§ Β¬ π₯ = π) β§ Β¬ π₯ < πΌ) β π₯ β β€) |
38 | | 1zzd 12539 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (1...π)) β§ Β¬ π₯ = π) β§ Β¬ π₯ < πΌ) β 1 β β€) |
39 | 33 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ π₯ β (1...π)) β§ Β¬ π₯ = π) β§ Β¬ π₯ < πΌ) β πΌ β β€) |
40 | 38, 39 | zsubcld 12617 |
. . . . . . . 8
β’ ((((π β§ π₯ β (1...π)) β§ Β¬ π₯ = π) β§ Β¬ π₯ < πΌ) β (1 β πΌ) β β€) |
41 | 37, 40 | zaddcld 12616 |
. . . . . . 7
β’ ((((π β§ π₯ β (1...π)) β§ Β¬ π₯ = π) β§ Β¬ π₯ < πΌ) β (π₯ + (1 β πΌ)) β β€) |
42 | 24, 25, 36, 41 | ifbothda 4525 |
. . . . . 6
β’ (((π β§ π₯ β (1...π)) β§ Β¬ π₯ = π) β if(π₯ < πΌ, (π₯ + (π β πΌ)), (π₯ + (1 β πΌ))) β β€) |
43 | 19, 20, 23, 42 | ifbothda 4525 |
. . . . 5
β’ ((π β§ π₯ β (1...π)) β if(π₯ = π, π, if(π₯ < πΌ, (π₯ + (π β πΌ)), (π₯ + (1 β πΌ)))) β β€) |
44 | | metakunt25.4 |
. . . . 5
β’ π΅ = (π₯ β (1...π) β¦ if(π₯ = π, π, if(π₯ < πΌ, (π₯ + (π β πΌ)), (π₯ + (1 β πΌ))))) |
45 | 43, 44 | fmptd 7063 |
. . . 4
β’ (π β π΅:(1...π)βΆβ€) |
46 | 45 | ffnd 6670 |
. . 3
β’ (π β π΅ Fn (1...π)) |
47 | 1, 2, 3, 44, 4, 6 | metakunt19 40641 |
. . . . . 6
β’ (π β (((π₯ β (1...(πΌ β 1)) β¦ (π₯ + (π β πΌ))) Fn (1...(πΌ β 1)) β§ (π₯ β (πΌ...(π β 1)) β¦ (π₯ + (1 β πΌ))) Fn (πΌ...(π β 1)) β§ ((π₯ β (1...(πΌ β 1)) β¦ (π₯ + (π β πΌ))) βͺ (π₯ β (πΌ...(π β 1)) β¦ (π₯ + (1 β πΌ)))) Fn ((1...(πΌ β 1)) βͺ (πΌ...(π β 1)))) β§ {β¨π, πβ©} Fn {π})) |
48 | 47 | simpld 496 |
. . . . 5
β’ (π β ((π₯ β (1...(πΌ β 1)) β¦ (π₯ + (π β πΌ))) Fn (1...(πΌ β 1)) β§ (π₯ β (πΌ...(π β 1)) β¦ (π₯ + (1 β πΌ))) Fn (πΌ...(π β 1)) β§ ((π₯ β (1...(πΌ β 1)) β¦ (π₯ + (π β πΌ))) βͺ (π₯ β (πΌ...(π β 1)) β¦ (π₯ + (1 β πΌ)))) Fn ((1...(πΌ β 1)) βͺ (πΌ...(π β 1))))) |
49 | 48 | simp3d 1145 |
. . . 4
β’ (π β ((π₯ β (1...(πΌ β 1)) β¦ (π₯ + (π β πΌ))) βͺ (π₯ β (πΌ...(π β 1)) β¦ (π₯ + (1 β πΌ)))) Fn ((1...(πΌ β 1)) βͺ (πΌ...(π β 1)))) |
50 | 47 | simprd 497 |
. . . 4
β’ (π β {β¨π, πβ©} Fn {π}) |
51 | 1, 2, 3 | metakunt24 40646 |
. . . . 5
β’ (π β ((((1...(πΌ β 1)) βͺ (πΌ...(π β 1))) β© {π}) = β
β§ (1...π) = (((1...(πΌ β 1)) βͺ (πΌ...(π β 1))) βͺ {π}) β§ (1...π) = (((((π β πΌ) + 1)...(π β 1)) βͺ (1...(π β πΌ))) βͺ {π}))) |
52 | 51 | simp1d 1143 |
. . . 4
β’ (π β (((1...(πΌ β 1)) βͺ (πΌ...(π β 1))) β© {π}) = β
) |
53 | 49, 50, 52 | fnund 6616 |
. . 3
β’ (π β (((π₯ β (1...(πΌ β 1)) β¦ (π₯ + (π β πΌ))) βͺ (π₯ β (πΌ...(π β 1)) β¦ (π₯ + (1 β πΌ)))) βͺ {β¨π, πβ©}) Fn (((1...(πΌ β 1)) βͺ (πΌ...(π β 1))) βͺ {π})) |
54 | 51 | simp2d 1144 |
. . 3
β’ (π β (1...π) = (((1...(πΌ β 1)) βͺ (πΌ...(π β 1))) βͺ {π})) |
55 | 1 | adantr 482 |
. . . 4
β’ ((π β§ π¦ β (1...π)) β π β β) |
56 | 2 | adantr 482 |
. . . 4
β’ ((π β§ π¦ β (1...π)) β πΌ β β) |
57 | 3 | adantr 482 |
. . . 4
β’ ((π β§ π¦ β (1...π)) β πΌ β€ π) |
58 | | simpr 486 |
. . . 4
β’ ((π β§ π¦ β (1...π)) β π¦ β (1...π)) |
59 | 55, 56, 57, 44, 4, 6, 58 | metakunt23 40645 |
. . 3
β’ ((π β§ π¦ β (1...π)) β (π΅βπ¦) = ((((π₯ β (1...(πΌ β 1)) β¦ (π₯ + (π β πΌ))) βͺ (π₯ β (πΌ...(π β 1)) β¦ (π₯ + (1 β πΌ)))) βͺ {β¨π, πβ©})βπ¦)) |
60 | 46, 53, 54, 59 | eqfnfv2d2 40485 |
. 2
β’ (π β π΅ = (((π₯ β (1...(πΌ β 1)) β¦ (π₯ + (π β πΌ))) βͺ (π₯ β (πΌ...(π β 1)) β¦ (π₯ + (1 β πΌ)))) βͺ {β¨π, πβ©})) |
61 | 51 | simp3d 1145 |
. 2
β’ (π β (1...π) = (((((π β πΌ) + 1)...(π β 1)) βͺ (1...(π β πΌ))) βͺ {π})) |
62 | 5, 7, 9, 12, 13, 14, 16, 17, 18, 60, 54, 61 | metakunt17 40639 |
1
β’ (π β π΅:(1...π)β1-1-ontoβ(1...π)) |