Step | Hyp | Ref
| Expression |
1 | | elfznn 13476 |
. . . . . . . 8
β’ (π₯ β (1...sup((β‘πΊ β (π...π)), β, < )) β π₯ β
β) |
2 | 1 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (π₯ β (1...sup((β‘πΊ β (π...π)), β, < )) β π₯ β
β)) |
3 | | cnvimass 6034 |
. . . . . . . . 9
β’ (β‘πΊ β (π...π)) β dom πΊ |
4 | | isercoll.g |
. . . . . . . . . 10
β’ (π β πΊ:ββΆπ) |
5 | 4 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (β€β₯β(πΊβ1))) β πΊ:ββΆπ) |
6 | 3, 5 | fssdm 6689 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (β‘πΊ β (π...π)) β β) |
7 | 6 | sseld 3944 |
. . . . . . 7
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (π₯ β (β‘πΊ β (π...π)) β π₯ β β)) |
8 | | id 22 |
. . . . . . . . . . 11
β’ (π₯ β β β π₯ β
β) |
9 | | nnuz 12811 |
. . . . . . . . . . 11
β’ β =
(β€β₯β1) |
10 | 8, 9 | eleqtrdi 2844 |
. . . . . . . . . 10
β’ (π₯ β β β π₯ β
(β€β₯β1)) |
11 | | ltso 11240 |
. . . . . . . . . . . . . 14
β’ < Or
β |
12 | 11 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β€β₯β(πΊβ1))) β < Or
β) |
13 | | fzfid 13884 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (π...π) β Fin) |
14 | | ffun 6672 |
. . . . . . . . . . . . . . . . 17
β’ (πΊ:ββΆπ β Fun πΊ) |
15 | | funimacnv 6583 |
. . . . . . . . . . . . . . . . 17
β’ (Fun
πΊ β (πΊ β (β‘πΊ β (π...π))) = ((π...π) β© ran πΊ)) |
16 | 5, 14, 15 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (πΊ β (β‘πΊ β (π...π))) = ((π...π) β© ran πΊ)) |
17 | | inss1 4189 |
. . . . . . . . . . . . . . . 16
β’ ((π...π) β© ran πΊ) β (π...π) |
18 | 16, 17 | eqsstrdi 3999 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (πΊ β (β‘πΊ β (π...π))) β (π...π)) |
19 | 13, 18 | ssfid 9214 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (πΊ β (β‘πΊ β (π...π))) β Fin) |
20 | | ssid 3967 |
. . . . . . . . . . . . . . . . . . . . 21
β’ β
β β |
21 | | isercoll.z |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π =
(β€β₯βπ) |
22 | | isercoll.m |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β β€) |
23 | | isercoll.i |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β) β (πΊβπ) < (πΊβ(π + 1))) |
24 | 21, 22, 4, 23 | isercolllem1 15555 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ β β β)
β (πΊ βΎ β)
Isom < , < (β, (πΊ β β))) |
25 | 20, 24 | mpan2 690 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (πΊ βΎ β) Isom < , < (β,
(πΊ β
β))) |
26 | | ffn 6669 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πΊ:ββΆπ β πΊ Fn β) |
27 | | fnresdm 6621 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πΊ Fn β β (πΊ βΎ β) = πΊ) |
28 | | isoeq1 7263 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΊ βΎ β) = πΊ β ((πΊ βΎ β) Isom < , < (β,
(πΊ β β)) β
πΊ Isom < , <
(β, (πΊ β
β)))) |
29 | 4, 26, 27, 28 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((πΊ βΎ β) Isom < , < (β,
(πΊ β β)) β
πΊ Isom < , <
(β, (πΊ β
β)))) |
30 | 25, 29 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΊ Isom < , < (β, (πΊ β
β))) |
31 | | isof1o 7269 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΊ Isom < , < (β,
(πΊ β β)) β
πΊ:ββ1-1-ontoβ(πΊ β β)) |
32 | | f1ocnv 6797 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΊ:ββ1-1-ontoβ(πΊ β β) β β‘πΊ:(πΊ β β)β1-1-ontoββ) |
33 | | f1ofun 6787 |
. . . . . . . . . . . . . . . . . . 19
β’ (β‘πΊ:(πΊ β β)β1-1-ontoββ β Fun β‘πΊ) |
34 | 30, 31, 32, 33 | 4syl 19 |
. . . . . . . . . . . . . . . . . 18
β’ (π β Fun β‘πΊ) |
35 | | df-f1 6502 |
. . . . . . . . . . . . . . . . . 18
β’ (πΊ:ββ1-1βπ β (πΊ:ββΆπ β§ Fun β‘πΊ)) |
36 | 4, 34, 35 | sylanbrc 584 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΊ:ββ1-1βπ) |
37 | 36 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯β(πΊβ1))) β πΊ:ββ1-1βπ) |
38 | | nnex 12164 |
. . . . . . . . . . . . . . . . 17
β’ β
β V |
39 | | ssexg 5281 |
. . . . . . . . . . . . . . . . 17
β’ (((β‘πΊ β (π...π)) β β β§ β β V)
β (β‘πΊ β (π...π)) β V) |
40 | 6, 38, 39 | sylancl 587 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (β‘πΊ β (π...π)) β V) |
41 | | f1imaeng 8957 |
. . . . . . . . . . . . . . . 16
β’ ((πΊ:ββ1-1βπ β§ (β‘πΊ β (π...π)) β β β§ (β‘πΊ β (π...π)) β V) β (πΊ β (β‘πΊ β (π...π))) β (β‘πΊ β (π...π))) |
42 | 37, 6, 40, 41 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (πΊ β (β‘πΊ β (π...π))) β (β‘πΊ β (π...π))) |
43 | 42 | ensymd 8948 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (β‘πΊ β (π...π)) β (πΊ β (β‘πΊ β (π...π)))) |
44 | | enfii 9136 |
. . . . . . . . . . . . . 14
β’ (((πΊ β (β‘πΊ β (π...π))) β Fin β§ (β‘πΊ β (π...π)) β (πΊ β (β‘πΊ β (π...π)))) β (β‘πΊ β (π...π)) β Fin) |
45 | 19, 43, 44 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (β‘πΊ β (π...π)) β Fin) |
46 | | 1nn 12169 |
. . . . . . . . . . . . . . . 16
β’ 1 β
β |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (β€β₯β(πΊβ1))) β 1 β
β) |
48 | | ffvelcdm 7033 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΊ:ββΆπ β§ 1 β β) β
(πΊβ1) β π) |
49 | 4, 46, 48 | sylancl 587 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (πΊβ1) β π) |
50 | 49, 21 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . 17
β’ (π β (πΊβ1) β
(β€β₯βπ)) |
51 | 50 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (πΊβ1) β
(β€β₯βπ)) |
52 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯β(πΊβ1))) β π β
(β€β₯β(πΊβ1))) |
53 | | elfzuzb 13441 |
. . . . . . . . . . . . . . . 16
β’ ((πΊβ1) β (π...π) β ((πΊβ1) β
(β€β₯βπ) β§ π β (β€β₯β(πΊβ1)))) |
54 | 51, 52, 53 | sylanbrc 584 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (πΊβ1) β (π...π)) |
55 | 5 | ffnd 6670 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯β(πΊβ1))) β πΊ Fn β) |
56 | | elpreima 7009 |
. . . . . . . . . . . . . . . 16
β’ (πΊ Fn β β (1 β
(β‘πΊ β (π...π)) β (1 β β β§ (πΊβ1) β (π...π)))) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (1 β
(β‘πΊ β (π...π)) β (1 β β β§ (πΊβ1) β (π...π)))) |
58 | 47, 54, 57 | mpbir2and 712 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (β€β₯β(πΊβ1))) β 1 β
(β‘πΊ β (π...π))) |
59 | 58 | ne0d 4296 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (β‘πΊ β (π...π)) β β
) |
60 | | nnssre 12162 |
. . . . . . . . . . . . . 14
β’ β
β β |
61 | 6, 60 | sstrdi 3957 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (β‘πΊ β (π...π)) β β) |
62 | | fisupcl 9410 |
. . . . . . . . . . . . 13
β’ (( <
Or β β§ ((β‘πΊ β (π...π)) β Fin β§ (β‘πΊ β (π...π)) β β
β§ (β‘πΊ β (π...π)) β β)) β sup((β‘πΊ β (π...π)), β, < ) β (β‘πΊ β (π...π))) |
63 | 12, 45, 59, 61, 62 | syl13anc 1373 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β€β₯β(πΊβ1))) β sup((β‘πΊ β (π...π)), β, < ) β (β‘πΊ β (π...π))) |
64 | 6, 63 | sseldd 3946 |
. . . . . . . . . . 11
β’ ((π β§ π β (β€β₯β(πΊβ1))) β sup((β‘πΊ β (π...π)), β, < ) β
β) |
65 | 64 | nnzd 12531 |
. . . . . . . . . 10
β’ ((π β§ π β (β€β₯β(πΊβ1))) β sup((β‘πΊ β (π...π)), β, < ) β
β€) |
66 | | elfz5 13439 |
. . . . . . . . . 10
β’ ((π₯ β
(β€β₯β1) β§ sup((β‘πΊ β (π...π)), β, < ) β β€) β
(π₯ β (1...sup((β‘πΊ β (π...π)), β, < )) β π₯ β€ sup((β‘πΊ β (π...π)), β, < ))) |
67 | 10, 65, 66 | syl2anr 598 |
. . . . . . . . 9
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β (π₯ β (1...sup((β‘πΊ β (π...π)), β, < )) β π₯ β€ sup((β‘πΊ β (π...π)), β, < ))) |
68 | | elpreima 7009 |
. . . . . . . . . . . . . . . . 17
β’ (πΊ Fn β β (sup((β‘πΊ β (π...π)), β, < ) β (β‘πΊ β (π...π)) β (sup((β‘πΊ β (π...π)), β, < ) β β β§
(πΊβsup((β‘πΊ β (π...π)), β, < )) β (π...π)))) |
69 | 55, 68 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (sup((β‘πΊ β (π...π)), β, < ) β (β‘πΊ β (π...π)) β (sup((β‘πΊ β (π...π)), β, < ) β β β§
(πΊβsup((β‘πΊ β (π...π)), β, < )) β (π...π)))) |
70 | 63, 69 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (sup((β‘πΊ β (π...π)), β, < ) β β β§
(πΊβsup((β‘πΊ β (π...π)), β, < )) β (π...π))) |
71 | | elfzle2 13451 |
. . . . . . . . . . . . . . 15
β’ ((πΊβsup((β‘πΊ β (π...π)), β, < )) β (π...π) β (πΊβsup((β‘πΊ β (π...π)), β, < )) β€ π) |
72 | 70, 71 | simpl2im 505 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (πΊβsup((β‘πΊ β (π...π)), β, < )) β€ π) |
73 | 72 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β (πΊβsup((β‘πΊ β (π...π)), β, < )) β€ π) |
74 | | uzssz 12789 |
. . . . . . . . . . . . . . . . 17
β’
(β€β₯βπ) β β€ |
75 | 21, 74 | eqsstri 3979 |
. . . . . . . . . . . . . . . 16
β’ π β
β€ |
76 | | zssre 12511 |
. . . . . . . . . . . . . . . 16
β’ β€
β β |
77 | 75, 76 | sstri 3954 |
. . . . . . . . . . . . . . 15
β’ π β
β |
78 | 5 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β (πΊβπ₯) β π) |
79 | 77, 78 | sselid 3943 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β (πΊβπ₯) β β) |
80 | 5, 64 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (πΊβsup((β‘πΊ β (π...π)), β, < )) β π) |
81 | 80 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β (πΊβsup((β‘πΊ β (π...π)), β, < )) β π) |
82 | 77, 81 | sselid 3943 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β (πΊβsup((β‘πΊ β (π...π)), β, < )) β
β) |
83 | | eluzelz 12778 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β(πΊβ1)) β π β β€) |
84 | 83 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β π β
β€) |
85 | 76, 84 | sselid 3943 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β π β
β) |
86 | | letr 11254 |
. . . . . . . . . . . . . 14
β’ (((πΊβπ₯) β β β§ (πΊβsup((β‘πΊ β (π...π)), β, < )) β β β§
π β β) β
(((πΊβπ₯) β€ (πΊβsup((β‘πΊ β (π...π)), β, < )) β§ (πΊβsup((β‘πΊ β (π...π)), β, < )) β€ π) β (πΊβπ₯) β€ π)) |
87 | 79, 82, 85, 86 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β (((πΊβπ₯) β€ (πΊβsup((β‘πΊ β (π...π)), β, < )) β§ (πΊβsup((β‘πΊ β (π...π)), β, < )) β€ π) β (πΊβπ₯) β€ π)) |
88 | 73, 87 | mpan2d 693 |
. . . . . . . . . . . 12
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β ((πΊβπ₯) β€ (πΊβsup((β‘πΊ β (π...π)), β, < )) β (πΊβπ₯) β€ π)) |
89 | 30 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β πΊ Isom < , < (β,
(πΊ β
β))) |
90 | 60 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β β
β β) |
91 | | ressxr 11204 |
. . . . . . . . . . . . . 14
β’ β
β β* |
92 | 90, 91 | sstrdi 3957 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β β
β β*) |
93 | | imassrn 6025 |
. . . . . . . . . . . . . . . 16
β’ (πΊ β β) β ran
πΊ |
94 | 4 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β πΊ:ββΆπ) |
95 | 94 | frnd 6677 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β ran
πΊ β π) |
96 | 93, 95 | sstrid 3956 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β (πΊ β β) β π) |
97 | 96, 77 | sstrdi 3957 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β (πΊ β β) β
β) |
98 | 97, 91 | sstrdi 3957 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β (πΊ β β) β
β*) |
99 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β π₯ β
β) |
100 | 64 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β
sup((β‘πΊ β (π...π)), β, < ) β
β) |
101 | | leisorel 14365 |
. . . . . . . . . . . . 13
β’ ((πΊ Isom < , < (β,
(πΊ β β)) β§
(β β β* β§ (πΊ β β) β
β*) β§ (π₯ β β β§ sup((β‘πΊ β (π...π)), β, < ) β β)) β
(π₯ β€ sup((β‘πΊ β (π...π)), β, < ) β (πΊβπ₯) β€ (πΊβsup((β‘πΊ β (π...π)), β, < )))) |
102 | 89, 92, 98, 99, 100, 101 | syl122anc 1380 |
. . . . . . . . . . . 12
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β (π₯ β€ sup((β‘πΊ β (π...π)), β, < ) β (πΊβπ₯) β€ (πΊβsup((β‘πΊ β (π...π)), β, < )))) |
103 | 78, 21 | eleqtrdi 2844 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β (πΊβπ₯) β (β€β₯βπ)) |
104 | | elfz5 13439 |
. . . . . . . . . . . . 13
β’ (((πΊβπ₯) β (β€β₯βπ) β§ π β β€) β ((πΊβπ₯) β (π...π) β (πΊβπ₯) β€ π)) |
105 | 103, 84, 104 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β ((πΊβπ₯) β (π...π) β (πΊβπ₯) β€ π)) |
106 | 88, 102, 105 | 3imtr4d 294 |
. . . . . . . . . . 11
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β (π₯ β€ sup((β‘πΊ β (π...π)), β, < ) β (πΊβπ₯) β (π...π))) |
107 | | elpreima 7009 |
. . . . . . . . . . . . 13
β’ (πΊ Fn β β (π₯ β (β‘πΊ β (π...π)) β (π₯ β β β§ (πΊβπ₯) β (π...π)))) |
108 | 107 | baibd 541 |
. . . . . . . . . . . 12
β’ ((πΊ Fn β β§ π₯ β β) β (π₯ β (β‘πΊ β (π...π)) β (πΊβπ₯) β (π...π))) |
109 | 55, 108 | sylan 581 |
. . . . . . . . . . 11
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β (π₯ β (β‘πΊ β (π...π)) β (πΊβπ₯) β (π...π))) |
110 | 106, 109 | sylibrd 259 |
. . . . . . . . . 10
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β (π₯ β€ sup((β‘πΊ β (π...π)), β, < ) β π₯ β (β‘πΊ β (π...π)))) |
111 | | fimaxre2 12105 |
. . . . . . . . . . . . 13
β’ (((β‘πΊ β (π...π)) β β β§ (β‘πΊ β (π...π)) β Fin) β βπ₯ β β βπ¦ β (β‘πΊ β (π...π))π¦ β€ π₯) |
112 | 61, 45, 111 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β€β₯β(πΊβ1))) β βπ₯ β β βπ¦ β (β‘πΊ β (π...π))π¦ β€ π₯) |
113 | | suprub 12121 |
. . . . . . . . . . . . 13
β’ ((((β‘πΊ β (π...π)) β β β§ (β‘πΊ β (π...π)) β β
β§ βπ₯ β β βπ¦ β (β‘πΊ β (π...π))π¦ β€ π₯) β§ π₯ β (β‘πΊ β (π...π))) β π₯ β€ sup((β‘πΊ β (π...π)), β, < )) |
114 | 113 | ex 414 |
. . . . . . . . . . . 12
β’ (((β‘πΊ β (π...π)) β β β§ (β‘πΊ β (π...π)) β β
β§ βπ₯ β β βπ¦ β (β‘πΊ β (π...π))π¦ β€ π₯) β (π₯ β (β‘πΊ β (π...π)) β π₯ β€ sup((β‘πΊ β (π...π)), β, < ))) |
115 | 61, 59, 112, 114 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (π₯ β (β‘πΊ β (π...π)) β π₯ β€ sup((β‘πΊ β (π...π)), β, < ))) |
116 | 115 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β (π₯ β (β‘πΊ β (π...π)) β π₯ β€ sup((β‘πΊ β (π...π)), β, < ))) |
117 | 110, 116 | impbid 211 |
. . . . . . . . 9
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β (π₯ β€ sup((β‘πΊ β (π...π)), β, < ) β π₯ β (β‘πΊ β (π...π)))) |
118 | 67, 117 | bitrd 279 |
. . . . . . . 8
β’ (((π β§ π β (β€β₯β(πΊβ1))) β§ π₯ β β) β (π₯ β (1...sup((β‘πΊ β (π...π)), β, < )) β π₯ β (β‘πΊ β (π...π)))) |
119 | 118 | ex 414 |
. . . . . . 7
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (π₯ β β β (π₯ β (1...sup((β‘πΊ β (π...π)), β, < )) β π₯ β (β‘πΊ β (π...π))))) |
120 | 2, 7, 119 | pm5.21ndd 381 |
. . . . . 6
β’ ((π β§ π β (β€β₯β(πΊβ1))) β (π₯ β (1...sup((β‘πΊ β (π...π)), β, < )) β π₯ β (β‘πΊ β (π...π)))) |
121 | 120 | eqrdv 2731 |
. . . . 5
β’ ((π β§ π β (β€β₯β(πΊβ1))) β
(1...sup((β‘πΊ β (π...π)), β, < )) = (β‘πΊ β (π...π))) |
122 | 121 | fveq2d 6847 |
. . . 4
β’ ((π β§ π β (β€β₯β(πΊβ1))) β
(β―β(1...sup((β‘πΊ β (π...π)), β, < ))) =
(β―β(β‘πΊ β (π...π)))) |
123 | 64 | nnnn0d 12478 |
. . . . 5
β’ ((π β§ π β (β€β₯β(πΊβ1))) β sup((β‘πΊ β (π...π)), β, < ) β
β0) |
124 | | hashfz1 14252 |
. . . . 5
β’
(sup((β‘πΊ β (π...π)), β, < ) β
β0 β (β―β(1...sup((β‘πΊ β (π...π)), β, < ))) = sup((β‘πΊ β (π...π)), β, < )) |
125 | 123, 124 | syl 17 |
. . . 4
β’ ((π β§ π β (β€β₯β(πΊβ1))) β
(β―β(1...sup((β‘πΊ β (π...π)), β, < ))) = sup((β‘πΊ β (π...π)), β, < )) |
126 | | hashen 14253 |
. . . . . 6
β’ (((β‘πΊ β (π...π)) β Fin β§ (πΊ β (β‘πΊ β (π...π))) β Fin) β
((β―β(β‘πΊ β (π...π))) = (β―β(πΊ β (β‘πΊ β (π...π)))) β (β‘πΊ β (π...π)) β (πΊ β (β‘πΊ β (π...π))))) |
127 | 45, 19, 126 | syl2anc 585 |
. . . . 5
β’ ((π β§ π β (β€β₯β(πΊβ1))) β
((β―β(β‘πΊ β (π...π))) = (β―β(πΊ β (β‘πΊ β (π...π)))) β (β‘πΊ β (π...π)) β (πΊ β (β‘πΊ β (π...π))))) |
128 | 43, 127 | mpbird 257 |
. . . 4
β’ ((π β§ π β (β€β₯β(πΊβ1))) β
(β―β(β‘πΊ β (π...π))) = (β―β(πΊ β (β‘πΊ β (π...π))))) |
129 | 122, 125,
128 | 3eqtr3d 2781 |
. . 3
β’ ((π β§ π β (β€β₯β(πΊβ1))) β sup((β‘πΊ β (π...π)), β, < ) = (β―β(πΊ β (β‘πΊ β (π...π))))) |
130 | 129 | oveq2d 7374 |
. 2
β’ ((π β§ π β (β€β₯β(πΊβ1))) β
(1...sup((β‘πΊ β (π...π)), β, < )) =
(1...(β―β(πΊ
β (β‘πΊ β (π...π)))))) |
131 | 130, 121 | eqtr3d 2775 |
1
β’ ((π β§ π β (β€β₯β(πΊβ1))) β
(1...(β―β(πΊ
β (β‘πΊ β (π...π))))) = (β‘πΊ β (π...π))) |