Step | Hyp | Ref
| Expression |
1 | | sticksstones11.1 |
. . 3
β’ (π β π β
β0) |
2 | | sticksstones11.2 |
. . . 4
β’ (π β πΎ = 0) |
3 | | 0nn0 12433 |
. . . . 5
β’ 0 β
β0 |
4 | 3 | a1i 11 |
. . . 4
β’ (π β 0 β
β0) |
5 | 2, 4 | eqeltrd 2834 |
. . 3
β’ (π β πΎ β
β0) |
6 | | sticksstones11.3 |
. . 3
β’ πΉ = (π β π΄ β¦ (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))) |
7 | | sticksstones11.5 |
. . 3
β’ π΄ = {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)} |
8 | | sticksstones11.6 |
. . 3
β’ π΅ = {π β£ (π:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))} |
9 | 1, 5, 6, 7, 8 | sticksstones8 40607 |
. 2
β’ (π β πΉ:π΄βΆπ΅) |
10 | | sticksstones11.4 |
. . 3
β’ πΊ = (π β π΅ β¦ if(πΎ = 0, {β¨1, πβ©}, (π β (1...(πΎ + 1)) β¦ if(π = (πΎ + 1), ((π + πΎ) β (πβπΎ)), if(π = 1, ((πβ1) β 1), (((πβπ) β (πβ(π β 1))) β
1)))))) |
11 | 1, 2, 10, 7, 8 | sticksstones9 40608 |
. 2
β’ (π β πΊ:π΅βΆπ΄) |
12 | 7 | a1i 11 |
. . . . . . . . 9
β’ (π β π΄ = {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)}) |
13 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π’π |
14 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²π’{π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)} |
15 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²π’{{β¨1, πβ©}} |
16 | | ffn 6669 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π’:{1}βΆβ0
β π’ Fn
{1}) |
17 | 16 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β π’ Fn {1}) |
18 | | 1nn 12169 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 1 β
β |
19 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β 1 β β) |
20 | 1 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β π β
β0) |
21 | | fnsng 6554 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((1
β β β§ π
β β0) β {β¨1, πβ©} Fn {1}) |
22 | 19, 20, 21 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β {β¨1, πβ©} Fn {1}) |
23 | | elsni 4604 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β {1} β π = 1) |
24 | 23 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β§ π β {1}) β π = 1) |
25 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β§ π β {1}) β§ π = 1) β π = 1) |
26 | 25 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β§ π β {1}) β§ π = 1) β (π’βπ) = (π’β1)) |
27 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β π’:{1}βΆβ0) |
28 | | 1ex 11156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ 1 β
V |
29 | 28 | snid 4623 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ 1 β
{1} |
30 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β 1 β {1}) |
31 | 27, 30 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β (π’β1) β
β0) |
32 | 31 | nn0cnd 12480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β (π’β1) β β) |
33 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = 1 β (π’βπ) = (π’β1)) |
34 | 33 | sumsn 15636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((1
β β β§ (π’β1) β β) β Ξ£π β {1} (π’βπ) = (π’β1)) |
35 | 19, 32, 34 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β Ξ£π β {1} (π’βπ) = (π’β1)) |
36 | 35 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β§ Ξ£π β {1} (π’βπ) = (π’β1)) β Ξ£π β {1} (π’βπ) = (π’β1)) |
37 | 36 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β§ Ξ£π β {1} (π’βπ) = (π’β1)) β (π’β1) = Ξ£π β {1} (π’βπ)) |
38 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β§ Ξ£π β {1} (π’βπ) = (π’β1)) β Ξ£π β {1} (π’βπ) = π) |
39 | 37, 38 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β§ Ξ£π β {1} (π’βπ) = (π’β1)) β (π’β1) = π) |
40 | 39 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β (Ξ£π β {1} (π’βπ) = (π’β1) β (π’β1) = π)) |
41 | 35, 40 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β (π’β1) = π) |
42 | 41 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β§ π β {1}) β (π’β1) = π) |
43 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β§ π β {1}) β 1 β
β) |
44 | 20 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β§ π β {1}) β π β
β0) |
45 | | fvsng 7127 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((1
β β β§ π
β β0) β ({β¨1, πβ©}β1) = π) |
46 | 43, 44, 45 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β§ π β {1}) β ({β¨1, πβ©}β1) = π) |
47 | 46 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β§ π β {1}) β π = ({β¨1, πβ©}β1)) |
48 | 42, 47 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β§ π β {1}) β (π’β1) = ({β¨1, πβ©}β1)) |
49 | 48 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β§ π β {1}) β§ π = 1) β (π’β1) = ({β¨1, πβ©}β1)) |
50 | 25 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β§ π β {1}) β§ π = 1) β 1 = π) |
51 | 50 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β§ π β {1}) β§ π = 1) β ({β¨1, πβ©}β1) = ({β¨1, πβ©}βπ)) |
52 | 26, 49, 51 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β§ π β {1}) β§ π = 1) β (π’βπ) = ({β¨1, πβ©}βπ)) |
53 | 24, 52 | mpdan 686 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β§ π β {1}) β (π’βπ) = ({β¨1, πβ©}βπ)) |
54 | 17, 22, 53 | eqfnfvd 6986 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β π’ = {β¨1, πβ©}) |
55 | | fsng 7084 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((1
β β β§ π
β β0) β (π’:{1}βΆ{π} β π’ = {β¨1, πβ©})) |
56 | 19, 20, 55 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β (π’:{1}βΆ{π} β π’ = {β¨1, πβ©})) |
57 | 54, 56 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β π’:{1}βΆ{π}) |
58 | | ssidd 3968 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β {π} β {π}) |
59 | | fss 6686 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π’:{1}βΆ{π} β§ {π} β {π}) β π’:{1}βΆ{π}) |
60 | 57, 58, 59 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β π’:{1}βΆ{π}) |
61 | 60, 58, 59 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β π’:{1}βΆ{π}) |
62 | 61, 56 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β π’ = {β¨1, πβ©}) |
63 | | vex 3448 |
. . . . . . . . . . . . . . . . . 18
β’ π’ β V |
64 | 63 | elsn 4602 |
. . . . . . . . . . . . . . . . 17
β’ (π’ β {{β¨1, πβ©}} β π’ = {β¨1, πβ©}) |
65 | 62, 64 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π)) β π’ β {{β¨1, πβ©}}) |
66 | 65 | ex 414 |
. . . . . . . . . . . . . . 15
β’ (π β ((π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π) β π’ β {{β¨1, πβ©}})) |
67 | | 1zzd 12539 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β 1 β
β€) |
68 | | fzsn 13489 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (1 β
β€ β (1...1) = {1}) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (1...1) =
{1}) |
70 | 69 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β {1} =
(1...1)) |
71 | | 1e0p1 12665 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 1 = (0 +
1) |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β 1 = (0 +
1)) |
73 | 72 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...1) = (1...(0 +
1))) |
74 | 70, 73 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β {1} = (1...(0 +
1))) |
75 | 2 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β 0 = πΎ) |
76 | 75 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (0 + 1) = (πΎ + 1)) |
77 | 76 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...(0 + 1)) =
(1...(πΎ +
1))) |
78 | 74, 77 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
β’ (π β {1} = (1...(πΎ + 1))) |
79 | 78 | feq2d 6655 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π’:{1}βΆβ0 β π’:(1...(πΎ +
1))βΆβ0)) |
80 | 78 | sumeq1d 15591 |
. . . . . . . . . . . . . . . . . 18
β’ (π β Ξ£π β {1} (π’βπ) = Ξ£π β (1...(πΎ + 1))(π’βπ)) |
81 | 80 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . 17
β’ (π β (Ξ£π β {1} (π’βπ) = π β Ξ£π β (1...(πΎ + 1))(π’βπ) = π)) |
82 | 79, 81 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
β’ (π β ((π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π) β (π’:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(π’βπ) = π))) |
83 | 82 | imbi1d 342 |
. . . . . . . . . . . . . . 15
β’ (π β (((π’:{1}βΆβ0 β§
Ξ£π β {1} (π’βπ) = π) β π’ β {{β¨1, πβ©}}) β ((π’:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(π’βπ) = π) β π’ β {{β¨1, πβ©}}))) |
84 | 66, 83 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (π β ((π’:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(π’βπ) = π) β π’ β {{β¨1, πβ©}})) |
85 | | feq1 6650 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π’ β (π:(1...(πΎ + 1))βΆβ0 β
π’:(1...(πΎ +
1))βΆβ0)) |
86 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π = π’ β§ π β (1...(πΎ + 1))) β π = π’) |
87 | 86 | fveq1d 6845 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π = π’ β§ π β (1...(πΎ + 1))) β (πβπ) = (π’βπ)) |
88 | 87 | sumeq2dv 15593 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π’ β Ξ£π β (1...(πΎ + 1))(πβπ) = Ξ£π β (1...(πΎ + 1))(π’βπ)) |
89 | 88 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π’ β (Ξ£π β (1...(πΎ + 1))(πβπ) = π β Ξ£π β (1...(πΎ + 1))(π’βπ) = π)) |
90 | 85, 89 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
β’ (π = π’ β ((π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π) β (π’:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(π’βπ) = π))) |
91 | 63, 90 | elab 3631 |
. . . . . . . . . . . . . . . 16
β’ (π’ β {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)} β (π’:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(π’βπ) = π)) |
92 | 91 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β (π’ β {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)} β (π’:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(π’βπ) = π))) |
93 | 92 | imbi1d 342 |
. . . . . . . . . . . . . 14
β’ (π β ((π’ β {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)} β π’ β {{β¨1, πβ©}}) β ((π’:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(π’βπ) = π) β π’ β {{β¨1, πβ©}}))) |
94 | 84, 93 | mpbird 257 |
. . . . . . . . . . . . 13
β’ (π β (π’ β {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)} β π’ β {{β¨1, πβ©}})) |
95 | 94 | imp 408 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)}) β π’ β {{β¨1, πβ©}}) |
96 | 95 | ex 414 |
. . . . . . . . . . 11
β’ (π β (π’ β {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)} β π’ β {{β¨1, πβ©}})) |
97 | 13, 14, 15, 96 | ssrd 3950 |
. . . . . . . . . 10
β’ (π β {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)} β {{β¨1, πβ©}}) |
98 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β 1 β
β) |
99 | 98, 1, 55 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π’:{1}βΆ{π} β π’ = {β¨1, πβ©})) |
100 | 99 | bicomd 222 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π’ = {β¨1, πβ©} β π’:{1}βΆ{π})) |
101 | 100 | biimpd 228 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π’ = {β¨1, πβ©} β π’:{1}βΆ{π})) |
102 | | elsni 4604 |
. . . . . . . . . . . . . . . . 17
β’ (π’ β {{β¨1, πβ©}} β π’ = {β¨1, πβ©}) |
103 | 101, 102 | impel 507 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β {{β¨1, πβ©}}) β π’:{1}βΆ{π}) |
104 | 1 | snssd 4770 |
. . . . . . . . . . . . . . . . 17
β’ (π β {π} β
β0) |
105 | 104 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β {{β¨1, πβ©}}) β {π} β
β0) |
106 | | fss 6686 |
. . . . . . . . . . . . . . . 16
β’ ((π’:{1}βΆ{π} β§ {π} β β0) β π’:{1}βΆβ0) |
107 | 103, 105,
106 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β {{β¨1, πβ©}}) β π’:{1}βΆβ0) |
108 | 79 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β {{β¨1, πβ©}}) β (π’:{1}βΆβ0 β π’:(1...(πΎ +
1))βΆβ0)) |
109 | 107, 108 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β {{β¨1, πβ©}}) β π’:(1...(πΎ +
1))βΆβ0) |
110 | 102 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β {{β¨1, πβ©}}) β π’ = {β¨1, πβ©}) |
111 | 78 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π’ β {{β¨1, πβ©}} β§ π’ = {β¨1, πβ©}) β {1} = (1...(πΎ + 1))) |
112 | 111 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π’ β {{β¨1, πβ©}} β§ π’ = {β¨1, πβ©}) β (1...(πΎ + 1)) = {1}) |
113 | 112 | sumeq1d 15591 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β {{β¨1, πβ©}} β§ π’ = {β¨1, πβ©}) β Ξ£π β (1...(πΎ + 1))(π’βπ) = Ξ£π β {1} (π’βπ)) |
114 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π’ β {{β¨1, πβ©}} β§ π’ = {β¨1, πβ©}) β 1 β
β) |
115 | 1 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π’ β {{β¨1, πβ©}} β§ π’ = {β¨1, πβ©}) β π β
β0) |
116 | 115 | nn0cnd 12480 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π’ β {{β¨1, πβ©}} β§ π’ = {β¨1, πβ©}) β π β β) |
117 | 114, 115,
45 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π’ β {{β¨1, πβ©}} β§ π’ = {β¨1, πβ©}) β ({β¨1, πβ©}β1) = π) |
118 | 117 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π’ β {{β¨1, πβ©}} β§ π’ = {β¨1, πβ©}) β π = ({β¨1, πβ©}β1)) |
119 | 110 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π’ β {{β¨1, πβ©}} β§ π’ = {β¨1, πβ©}) β π’ = {β¨1, πβ©}) |
120 | 119 | fveq1d 6845 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π’ β {{β¨1, πβ©}} β§ π’ = {β¨1, πβ©}) β (π’β1) = ({β¨1, πβ©}β1)) |
121 | 118, 120 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π’ β {{β¨1, πβ©}} β§ π’ = {β¨1, πβ©}) β π = (π’β1)) |
122 | 121 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π’ β {{β¨1, πβ©}} β§ π’ = {β¨1, πβ©}) β (π β β β (π’β1) β β)) |
123 | 116, 122 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π’ β {{β¨1, πβ©}} β§ π’ = {β¨1, πβ©}) β (π’β1) β β) |
124 | 114, 123,
34 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π’ β {{β¨1, πβ©}} β§ π’ = {β¨1, πβ©}) β Ξ£π β {1} (π’βπ) = (π’β1)) |
125 | 120, 117 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π’ β {{β¨1, πβ©}} β§ π’ = {β¨1, πβ©}) β (π’β1) = π) |
126 | 124, 125 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β {{β¨1, πβ©}} β§ π’ = {β¨1, πβ©}) β Ξ£π β {1} (π’βπ) = π) |
127 | 113, 126 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β {{β¨1, πβ©}} β§ π’ = {β¨1, πβ©}) β Ξ£π β (1...(πΎ + 1))(π’βπ) = π) |
128 | 127 | 3expa 1119 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π’ β {{β¨1, πβ©}}) β§ π’ = {β¨1, πβ©}) β Ξ£π β (1...(πΎ + 1))(π’βπ) = π) |
129 | 110, 128 | mpdan 686 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β {{β¨1, πβ©}}) β Ξ£π β (1...(πΎ + 1))(π’βπ) = π) |
130 | 109, 129 | jca 513 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β {{β¨1, πβ©}}) β (π’:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(π’βπ) = π)) |
131 | 130, 91 | sylibr 233 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β {{β¨1, πβ©}}) β π’ β {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)}) |
132 | 131 | ex 414 |
. . . . . . . . . . 11
β’ (π β (π’ β {{β¨1, πβ©}} β π’ β {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)})) |
133 | 13, 15, 14, 132 | ssrd 3950 |
. . . . . . . . . 10
β’ (π β {{β¨1, πβ©}} β {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)}) |
134 | 97, 133 | eqssd 3962 |
. . . . . . . . 9
β’ (π β {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)} = {{β¨1, πβ©}}) |
135 | 12, 134 | eqtrd 2773 |
. . . . . . . 8
β’ (π β π΄ = {{β¨1, πβ©}}) |
136 | | eqss 3960 |
. . . . . . . . . 10
β’ (π΄ = {{β¨1, πβ©}} β (π΄ β {{β¨1, πβ©}} β§ {{β¨1, πβ©}} β π΄)) |
137 | 136 | biimpi 215 |
. . . . . . . . 9
β’ (π΄ = {{β¨1, πβ©}} β (π΄ β {{β¨1, πβ©}} β§ {{β¨1, πβ©}} β π΄)) |
138 | 137 | simpld 496 |
. . . . . . . 8
β’ (π΄ = {{β¨1, πβ©}} β π΄ β {{β¨1, πβ©}}) |
139 | 135, 138 | syl 17 |
. . . . . . 7
β’ (π β π΄ β {{β¨1, πβ©}}) |
140 | | fss 6686 |
. . . . . . 7
β’ ((πΊ:π΅βΆπ΄ β§ π΄ β {{β¨1, πβ©}}) β πΊ:π΅βΆ{{β¨1, πβ©}}) |
141 | 11, 139, 140 | syl2anc 585 |
. . . . . 6
β’ (π β πΊ:π΅βΆ{{β¨1, πβ©}}) |
142 | 141 | adantr 482 |
. . . . 5
β’ ((π β§ π β π΄) β πΊ:π΅βΆ{{β¨1, πβ©}}) |
143 | 9 | ffvelcdmda 7036 |
. . . . 5
β’ ((π β§ π β π΄) β (πΉβπ) β π΅) |
144 | | fvconst 7111 |
. . . . 5
β’ ((πΊ:π΅βΆ{{β¨1, πβ©}} β§ (πΉβπ) β π΅) β (πΊβ(πΉβπ)) = {β¨1, πβ©}) |
145 | 142, 143,
144 | syl2anc 585 |
. . . 4
β’ ((π β§ π β π΄) β (πΊβ(πΉβπ)) = {β¨1, πβ©}) |
146 | 135 | eleq2d 2820 |
. . . . . . . 8
β’ (π β (π β π΄ β π β {{β¨1, πβ©}})) |
147 | 146 | biimpd 228 |
. . . . . . 7
β’ (π β (π β π΄ β π β {{β¨1, πβ©}})) |
148 | 147 | imp 408 |
. . . . . 6
β’ ((π β§ π β π΄) β π β {{β¨1, πβ©}}) |
149 | | vex 3448 |
. . . . . . 7
β’ π β V |
150 | 149 | elsn 4602 |
. . . . . 6
β’ (π β {{β¨1, πβ©}} β π = {β¨1, πβ©}) |
151 | 148, 150 | sylib 217 |
. . . . 5
β’ ((π β§ π β π΄) β π = {β¨1, πβ©}) |
152 | 151 | eqcomd 2739 |
. . . 4
β’ ((π β§ π β π΄) β {β¨1, πβ©} = π) |
153 | 145, 152 | eqtrd 2773 |
. . 3
β’ ((π β§ π β π΄) β (πΊβ(πΉβπ)) = π) |
154 | 153 | ralrimiva 3140 |
. 2
β’ (π β βπ β π΄ (πΊβ(πΉβπ)) = π) |
155 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β π β π΅) |
156 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²ππ |
157 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²ππ΅ |
158 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²π{β
} |
159 | 8 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β π΅) β π΅ = {π β£ (π:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))}) |
160 | 159 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β π΅) β (π β π΅ β π β {π β£ (π:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))})) |
161 | 160 | biimpd 228 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β π΅) β (π β π΅ β π β {π β£ (π:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))})) |
162 | 161 | syldbl2 840 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π΅) β π β {π β£ (π:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))}) |
163 | | vex 3448 |
. . . . . . . . . . . . . . . . . . 19
β’ π β V |
164 | | feq1 6650 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (π:(1...πΎ)βΆ(1...(π + πΎ)) β π:(1...πΎ)βΆ(1...(π + πΎ)))) |
165 | | fveq1 6842 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (πβπ₯) = (πβπ₯)) |
166 | | fveq1 6842 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (πβπ¦) = (πβπ¦)) |
167 | 165, 166 | breq12d 5119 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β ((πβπ₯) < (πβπ¦) β (πβπ₯) < (πβπ¦))) |
168 | 167 | imbi2d 341 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((π₯ < π¦ β (πβπ₯) < (πβπ¦)) β (π₯ < π¦ β (πβπ₯) < (πβπ¦)))) |
169 | 168 | 2ralbidv 3209 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)) β βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))) |
170 | 164, 169 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((π:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦))) β (π:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦))))) |
171 | 163, 170 | elab 3631 |
. . . . . . . . . . . . . . . . . 18
β’ (π β {π β£ (π:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))} β (π:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))) |
172 | 162, 171 | sylib 217 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π΅) β (π:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))) |
173 | 172 | simpld 496 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π΅) β π:(1...πΎ)βΆ(1...(π + πΎ))) |
174 | | 0lt1 11682 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 0 <
1 |
175 | 174 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β 0 < 1) |
176 | 2, 175 | eqbrtrd 5128 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΎ < 1) |
177 | 5 | nn0zd 12530 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β πΎ β β€) |
178 | | fzn 13463 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((1
β β€ β§ πΎ
β β€) β (πΎ
< 1 β (1...πΎ) =
β
)) |
179 | 67, 177, 178 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (πΎ < 1 β (1...πΎ) = β
)) |
180 | 176, 179 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...πΎ) = β
) |
181 | 180 | feq2d 6655 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π:(1...πΎ)βΆ(1...(π + πΎ)) β π:β
βΆ(1...(π + πΎ)))) |
182 | 181 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π΅) β (π:(1...πΎ)βΆ(1...(π + πΎ)) β π:β
βΆ(1...(π + πΎ)))) |
183 | 173, 182 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΅) β π:β
βΆ(1...(π + πΎ))) |
184 | | f0bi 6726 |
. . . . . . . . . . . . . . 15
β’ (π:β
βΆ(1...(π + πΎ)) β π = β
) |
185 | 183, 184 | sylib 217 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΅) β π = β
) |
186 | | velsn 4603 |
. . . . . . . . . . . . . 14
β’ (π β {β
} β π = β
) |
187 | 185, 186 | sylibr 233 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅) β π β {β
}) |
188 | 187 | ex 414 |
. . . . . . . . . . . 12
β’ (π β (π β π΅ β π β {β
})) |
189 | | f0 6724 |
. . . . . . . . . . . . . . . . . . . 20
β’
β
:β
βΆ(1...(π + πΎ)) |
190 | 189 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
β
:β
βΆ(1...(π + πΎ))) |
191 | 180 | feq2d 6655 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (β
:(1...πΎ)βΆ(1...(π + πΎ)) β β
:β
βΆ(1...(π + πΎ)))) |
192 | 190, 191 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β
:(1...πΎ)βΆ(1...(π + πΎ))) |
193 | | ral0 4471 |
. . . . . . . . . . . . . . . . . . . 20
β’
βπ₯ β
β
βπ¦ β
(1...πΎ)(π₯ < π¦ β (β
βπ₯) < (β
βπ¦)) |
194 | 193 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β βπ₯ β β
βπ¦ β (1...πΎ)(π₯ < π¦ β (β
βπ₯) < (β
βπ¦))) |
195 | | biidd 262 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β (1...πΎ)) β (βπ¦ β (1...πΎ)(π₯ < π¦ β (β
βπ₯) < (β
βπ¦)) β βπ¦ β (1...πΎ)(π₯ < π¦ β (β
βπ₯) < (β
βπ¦)))) |
196 | 180, 195 | raleqbidva 3320 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (β
βπ₯) < (β
βπ¦)) β βπ₯ β β
βπ¦ β (1...πΎ)(π₯ < π¦ β (β
βπ₯) < (β
βπ¦)))) |
197 | 194, 196 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
β’ (π β βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (β
βπ₯) < (β
βπ¦))) |
198 | 192, 197 | jca 513 |
. . . . . . . . . . . . . . . . 17
β’ (π β (β
:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (β
βπ₯) < (β
βπ¦)))) |
199 | | 0ex 5265 |
. . . . . . . . . . . . . . . . . 18
β’ β
β V |
200 | | feq1 6650 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = β
β (π:(1...πΎ)βΆ(1...(π + πΎ)) β β
:(1...πΎ)βΆ(1...(π + πΎ)))) |
201 | | fveq1 6842 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = β
β (πβπ₯) = (β
βπ₯)) |
202 | | fveq1 6842 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = β
β (πβπ¦) = (β
βπ¦)) |
203 | 201, 202 | breq12d 5119 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = β
β ((πβπ₯) < (πβπ¦) β (β
βπ₯) < (β
βπ¦))) |
204 | 203 | imbi2d 341 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = β
β ((π₯ < π¦ β (πβπ₯) < (πβπ¦)) β (π₯ < π¦ β (β
βπ₯) < (β
βπ¦)))) |
205 | 204 | 2ralbidv 3209 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = β
β (βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)) β βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (β
βπ₯) < (β
βπ¦)))) |
206 | 200, 205 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = β
β ((π:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦))) β (β
:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (β
βπ₯) < (β
βπ¦))))) |
207 | 206 | elabg 3629 |
. . . . . . . . . . . . . . . . . 18
β’ (β
β V β (β
β {π β£ (π:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))} β (β
:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (β
βπ₯) < (β
βπ¦))))) |
208 | 199, 207 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ (β
β {π β£ (π:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))} β (β
:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (β
βπ₯) < (β
βπ¦)))) |
209 | 198, 208 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ (π β β
β {π β£ (π:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))}) |
210 | 8 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β π΅ = {π β£ (π:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))}) |
211 | 209, 210 | eleqtrrd 2837 |
. . . . . . . . . . . . . . 15
β’ (π β β
β π΅) |
212 | 211 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β {β
}) β β
β
π΅) |
213 | | elsni 4604 |
. . . . . . . . . . . . . . . 16
β’ (π β {β
} β π = β
) |
214 | 213 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β {β
}) β π = β
) |
215 | 214 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β {β
}) β (π β π΅ β β
β π΅)) |
216 | 212, 215 | mpbird 257 |
. . . . . . . . . . . . 13
β’ ((π β§ π β {β
}) β π β π΅) |
217 | 216 | ex 414 |
. . . . . . . . . . . 12
β’ (π β (π β {β
} β π β π΅)) |
218 | 188, 217 | impbid 211 |
. . . . . . . . . . 11
β’ (π β (π β π΅ β π β {β
})) |
219 | 156, 157,
158, 218 | eqrd 3964 |
. . . . . . . . . 10
β’ (π β π΅ = {β
}) |
220 | 219 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β π΅ = {β
}) |
221 | 155, 220 | eleqtrd 2836 |
. . . . . . . 8
β’ ((π β§ π β π΅) β π β {β
}) |
222 | 163 | elsn 4602 |
. . . . . . . 8
β’ (π β {β
} β π = β
) |
223 | 221, 222 | sylib 217 |
. . . . . . 7
β’ ((π β§ π β π΅) β π = β
) |
224 | 223 | fveq2d 6847 |
. . . . . 6
β’ ((π β§ π β π΅) β (πΊβπ) = (πΊββ
)) |
225 | 224 | fveq2d 6847 |
. . . . 5
β’ ((π β§ π β π΅) β (πΉβ(πΊβπ)) = (πΉβ(πΊββ
))) |
226 | 180 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β (1...πΎ) = β
) |
227 | 226 | mpteq1d 5201 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) = (π β β
β¦ (π + Ξ£π β (1...π)(πβπ)))) |
228 | | mpt0 6644 |
. . . . . . . . . . 11
β’ (π β β
β¦ (π + Ξ£π β (1...π)(πβπ))) = β
|
229 | 228 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β (π β β
β¦ (π + Ξ£π β (1...π)(πβπ))) = β
) |
230 | 227, 229 | eqtrd 2773 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) = β
) |
231 | | fzfid 13884 |
. . . . . . . . . . . 12
β’ (π β (1...πΎ) β Fin) |
232 | 231 | mptexd 7175 |
. . . . . . . . . . 11
β’ (π β (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) β V) |
233 | | elsng 4601 |
. . . . . . . . . . 11
β’ ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) β V β ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) β {β
} β (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) = β
)) |
234 | 232, 233 | syl 17 |
. . . . . . . . . 10
β’ (π β ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) β {β
} β (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) = β
)) |
235 | 234 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) β {β
} β (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) = β
)) |
236 | 230, 235 | mpbird 257 |
. . . . . . . 8
β’ ((π β§ π β π΄) β (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) β {β
}) |
237 | 236, 6 | fmptd 7063 |
. . . . . . 7
β’ (π β πΉ:π΄βΆ{β
}) |
238 | 237 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π΅) β πΉ:π΄βΆ{β
}) |
239 | | ffvelcdm 7033 |
. . . . . . . 8
β’ ((πΊ:π΅βΆπ΄ β§ β
β π΅) β (πΊββ
) β π΄) |
240 | 11, 211, 239 | syl2anc 585 |
. . . . . . 7
β’ (π β (πΊββ
) β π΄) |
241 | 240 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π΅) β (πΊββ
) β π΄) |
242 | | fvconst 7111 |
. . . . . 6
β’ ((πΉ:π΄βΆ{β
} β§ (πΊββ
) β π΄) β (πΉβ(πΊββ
)) = β
) |
243 | 238, 241,
242 | syl2anc 585 |
. . . . 5
β’ ((π β§ π β π΅) β (πΉβ(πΊββ
)) = β
) |
244 | 225, 243 | eqtrd 2773 |
. . . 4
β’ ((π β§ π β π΅) β (πΉβ(πΊβπ)) = β
) |
245 | 223 | eqcomd 2739 |
. . . 4
β’ ((π β§ π β π΅) β β
= π) |
246 | 244, 245 | eqtrd 2773 |
. . 3
β’ ((π β§ π β π΅) β (πΉβ(πΊβπ)) = π) |
247 | 246 | ralrimiva 3140 |
. 2
β’ (π β βπ β π΅ (πΉβ(πΊβπ)) = π) |
248 | 9, 11, 154, 247 | 2fvidf1od 7245 |
1
β’ (π β πΉ:π΄β1-1-ontoβπ΅) |