Step | Hyp | Ref
| Expression |
1 | | df-rab 3407 |
. . 3
β’ {π¦ β π· β£ π¦ βr β€ πΉ} = {π¦ β£ (π¦ β π· β§ π¦ βr β€ πΉ)} |
2 | | psrbag.d |
. . . . . . . 8
β’ π· = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
3 | 2 | psrbagf 21336 |
. . . . . . 7
β’ (π¦ β π· β π¦:πΌβΆβ0) |
4 | 3 | a1i 11 |
. . . . . 6
β’ (πΉ β π· β (π¦ β π· β π¦:πΌβΆβ0)) |
5 | 4 | adantrd 493 |
. . . . 5
β’ (πΉ β π· β ((π¦ β π· β§ π¦ βr β€ πΉ) β π¦:πΌβΆβ0)) |
6 | | ss2ixp 8851 |
. . . . . . . . 9
β’
(βπ₯ β
πΌ (0...(πΉβπ₯)) β β0 β Xπ₯ β
πΌ (0...(πΉβπ₯)) β Xπ₯ β πΌ β0) |
7 | | fz0ssnn0 13542 |
. . . . . . . . . 10
β’
(0...(πΉβπ₯)) β
β0 |
8 | 7 | a1i 11 |
. . . . . . . . 9
β’ (π₯ β πΌ β (0...(πΉβπ₯)) β
β0) |
9 | 6, 8 | mprg 3067 |
. . . . . . . 8
β’ Xπ₯ β
πΌ (0...(πΉβπ₯)) β Xπ₯ β πΌ β0 |
10 | 9 | sseli 3941 |
. . . . . . 7
β’ (π¦ β Xπ₯ β
πΌ (0...(πΉβπ₯)) β π¦ β Xπ₯ β πΌ β0) |
11 | | vex 3448 |
. . . . . . . 8
β’ π¦ β V |
12 | 11 | elixpconst 8846 |
. . . . . . 7
β’ (π¦ β Xπ₯ β
πΌ β0
β π¦:πΌβΆβ0) |
13 | 10, 12 | sylib 217 |
. . . . . 6
β’ (π¦ β Xπ₯ β
πΌ (0...(πΉβπ₯)) β π¦:πΌβΆβ0) |
14 | 13 | a1i 11 |
. . . . 5
β’ (πΉ β π· β (π¦ β Xπ₯ β πΌ (0...(πΉβπ₯)) β π¦:πΌβΆβ0)) |
15 | | ffn 6669 |
. . . . . . . . 9
β’ (π¦:πΌβΆβ0 β π¦ Fn πΌ) |
16 | 15 | adantl 483 |
. . . . . . . 8
β’ ((πΉ β π· β§ π¦:πΌβΆβ0) β π¦ Fn πΌ) |
17 | 11 | elixp 8845 |
. . . . . . . . 9
β’ (π¦ β Xπ₯ β
πΌ (0...(πΉβπ₯)) β (π¦ Fn πΌ β§ βπ₯ β πΌ (π¦βπ₯) β (0...(πΉβπ₯)))) |
18 | 17 | baib 537 |
. . . . . . . 8
β’ (π¦ Fn πΌ β (π¦ β Xπ₯ β πΌ (0...(πΉβπ₯)) β βπ₯ β πΌ (π¦βπ₯) β (0...(πΉβπ₯)))) |
19 | 16, 18 | syl 17 |
. . . . . . 7
β’ ((πΉ β π· β§ π¦:πΌβΆβ0) β (π¦ β Xπ₯ β
πΌ (0...(πΉβπ₯)) β βπ₯ β πΌ (π¦βπ₯) β (0...(πΉβπ₯)))) |
20 | | ffvelcdm 7033 |
. . . . . . . . . . . 12
β’ ((π¦:πΌβΆβ0 β§ π₯ β πΌ) β (π¦βπ₯) β
β0) |
21 | 20 | adantll 713 |
. . . . . . . . . . 11
β’ (((πΉ β π· β§ π¦:πΌβΆβ0) β§ π₯ β πΌ) β (π¦βπ₯) β
β0) |
22 | | nn0uz 12810 |
. . . . . . . . . . 11
β’
β0 = (β€β₯β0) |
23 | 21, 22 | eleqtrdi 2844 |
. . . . . . . . . 10
β’ (((πΉ β π· β§ π¦:πΌβΆβ0) β§ π₯ β πΌ) β (π¦βπ₯) β
(β€β₯β0)) |
24 | 2 | psrbagf 21336 |
. . . . . . . . . . . . 13
β’ (πΉ β π· β πΉ:πΌβΆβ0) |
25 | 24 | adantr 482 |
. . . . . . . . . . . 12
β’ ((πΉ β π· β§ π¦:πΌβΆβ0) β πΉ:πΌβΆβ0) |
26 | 25 | ffvelcdmda 7036 |
. . . . . . . . . . 11
β’ (((πΉ β π· β§ π¦:πΌβΆβ0) β§ π₯ β πΌ) β (πΉβπ₯) β
β0) |
27 | 26 | nn0zd 12530 |
. . . . . . . . . 10
β’ (((πΉ β π· β§ π¦:πΌβΆβ0) β§ π₯ β πΌ) β (πΉβπ₯) β β€) |
28 | | elfz5 13439 |
. . . . . . . . . 10
β’ (((π¦βπ₯) β (β€β₯β0)
β§ (πΉβπ₯) β β€) β ((π¦βπ₯) β (0...(πΉβπ₯)) β (π¦βπ₯) β€ (πΉβπ₯))) |
29 | 23, 27, 28 | syl2anc 585 |
. . . . . . . . 9
β’ (((πΉ β π· β§ π¦:πΌβΆβ0) β§ π₯ β πΌ) β ((π¦βπ₯) β (0...(πΉβπ₯)) β (π¦βπ₯) β€ (πΉβπ₯))) |
30 | 29 | ralbidva 3169 |
. . . . . . . 8
β’ ((πΉ β π· β§ π¦:πΌβΆβ0) β
(βπ₯ β πΌ (π¦βπ₯) β (0...(πΉβπ₯)) β βπ₯ β πΌ (π¦βπ₯) β€ (πΉβπ₯))) |
31 | 24 | ffnd 6670 |
. . . . . . . . . 10
β’ (πΉ β π· β πΉ Fn πΌ) |
32 | 31 | adantr 482 |
. . . . . . . . 9
β’ ((πΉ β π· β§ π¦:πΌβΆβ0) β πΉ Fn πΌ) |
33 | 11 | a1i 11 |
. . . . . . . . 9
β’ ((πΉ β π· β§ π¦:πΌβΆβ0) β π¦ β V) |
34 | | simpl 484 |
. . . . . . . . 9
β’ ((πΉ β π· β§ π¦:πΌβΆβ0) β πΉ β π·) |
35 | | inidm 4179 |
. . . . . . . . 9
β’ (πΌ β© πΌ) = πΌ |
36 | | eqidd 2734 |
. . . . . . . . 9
β’ (((πΉ β π· β§ π¦:πΌβΆβ0) β§ π₯ β πΌ) β (π¦βπ₯) = (π¦βπ₯)) |
37 | | eqidd 2734 |
. . . . . . . . 9
β’ (((πΉ β π· β§ π¦:πΌβΆβ0) β§ π₯ β πΌ) β (πΉβπ₯) = (πΉβπ₯)) |
38 | 16, 32, 33, 34, 35, 36, 37 | ofrfvalg 7626 |
. . . . . . . 8
β’ ((πΉ β π· β§ π¦:πΌβΆβ0) β (π¦ βr β€ πΉ β βπ₯ β πΌ (π¦βπ₯) β€ (πΉβπ₯))) |
39 | 30, 38 | bitr4d 282 |
. . . . . . 7
β’ ((πΉ β π· β§ π¦:πΌβΆβ0) β
(βπ₯ β πΌ (π¦βπ₯) β (0...(πΉβπ₯)) β π¦ βr β€ πΉ)) |
40 | 2 | psrbaglecl 21344 |
. . . . . . . . 9
β’ ((πΉ β π· β§ π¦:πΌβΆβ0 β§ π¦ βr β€ πΉ) β π¦ β π·) |
41 | 40 | 3expia 1122 |
. . . . . . . 8
β’ ((πΉ β π· β§ π¦:πΌβΆβ0) β (π¦ βr β€ πΉ β π¦ β π·)) |
42 | 41 | pm4.71rd 564 |
. . . . . . 7
β’ ((πΉ β π· β§ π¦:πΌβΆβ0) β (π¦ βr β€ πΉ β (π¦ β π· β§ π¦ βr β€ πΉ))) |
43 | 19, 39, 42 | 3bitrrd 306 |
. . . . . 6
β’ ((πΉ β π· β§ π¦:πΌβΆβ0) β ((π¦ β π· β§ π¦ βr β€ πΉ) β π¦ β Xπ₯ β πΌ (0...(πΉβπ₯)))) |
44 | 43 | ex 414 |
. . . . 5
β’ (πΉ β π· β (π¦:πΌβΆβ0 β ((π¦ β π· β§ π¦ βr β€ πΉ) β π¦ β Xπ₯ β πΌ (0...(πΉβπ₯))))) |
45 | 5, 14, 44 | pm5.21ndd 381 |
. . . 4
β’ (πΉ β π· β ((π¦ β π· β§ π¦ βr β€ πΉ) β π¦ β Xπ₯ β πΌ (0...(πΉβπ₯)))) |
46 | 45 | abbi1dv 2869 |
. . 3
β’ (πΉ β π· β {π¦ β£ (π¦ β π· β§ π¦ βr β€ πΉ)} = Xπ₯ β πΌ (0...(πΉβπ₯))) |
47 | 1, 46 | eqtrid 2785 |
. 2
β’ (πΉ β π· β {π¦ β π· β£ π¦ βr β€ πΉ} = Xπ₯ β πΌ (0...(πΉβπ₯))) |
48 | | cnveq 5830 |
. . . . . . 7
β’ (π = πΉ β β‘π = β‘πΉ) |
49 | 48 | imaeq1d 6013 |
. . . . . 6
β’ (π = πΉ β (β‘π β β) = (β‘πΉ β β)) |
50 | 49 | eleq1d 2819 |
. . . . 5
β’ (π = πΉ β ((β‘π β β) β Fin β (β‘πΉ β β) β
Fin)) |
51 | 50, 2 | elrab2 3649 |
. . . 4
β’ (πΉ β π· β (πΉ β (β0
βm πΌ) β§
(β‘πΉ β β) β
Fin)) |
52 | 51 | simprbi 498 |
. . 3
β’ (πΉ β π· β (β‘πΉ β β) β
Fin) |
53 | | fzfid 13884 |
. . 3
β’ ((πΉ β π· β§ π₯ β πΌ) β (0...(πΉβπ₯)) β Fin) |
54 | | fcdmnn0suppg 12476 |
. . . . . . . . 9
β’ ((πΉ β π· β§ πΉ:πΌβΆβ0) β (πΉ supp 0) = (β‘πΉ β β)) |
55 | 24, 54 | mpdan 686 |
. . . . . . . 8
β’ (πΉ β π· β (πΉ supp 0) = (β‘πΉ β β)) |
56 | | eqimss 4001 |
. . . . . . . 8
β’ ((πΉ supp 0) = (β‘πΉ β β) β (πΉ supp 0) β (β‘πΉ β β)) |
57 | 55, 56 | syl 17 |
. . . . . . 7
β’ (πΉ β π· β (πΉ supp 0) β (β‘πΉ β β)) |
58 | | id 22 |
. . . . . . 7
β’ (πΉ β π· β πΉ β π·) |
59 | | c0ex 11154 |
. . . . . . . 8
β’ 0 β
V |
60 | 59 | a1i 11 |
. . . . . . 7
β’ (πΉ β π· β 0 β V) |
61 | 24, 57, 58, 60 | suppssrg 8129 |
. . . . . 6
β’ ((πΉ β π· β§ π₯ β (πΌ β (β‘πΉ β β))) β (πΉβπ₯) = 0) |
62 | 61 | oveq2d 7374 |
. . . . 5
β’ ((πΉ β π· β§ π₯ β (πΌ β (β‘πΉ β β))) β (0...(πΉβπ₯)) = (0...0)) |
63 | | fz0sn 13547 |
. . . . 5
β’ (0...0) =
{0} |
64 | 62, 63 | eqtrdi 2789 |
. . . 4
β’ ((πΉ β π· β§ π₯ β (πΌ β (β‘πΉ β β))) β (0...(πΉβπ₯)) = {0}) |
65 | | eqimss 4001 |
. . . 4
β’
((0...(πΉβπ₯)) = {0} β (0...(πΉβπ₯)) β {0}) |
66 | 64, 65 | syl 17 |
. . 3
β’ ((πΉ β π· β§ π₯ β (πΌ β (β‘πΉ β β))) β (0...(πΉβπ₯)) β {0}) |
67 | 52, 53, 66 | ixpfi2 9297 |
. 2
β’ (πΉ β π· β Xπ₯ β πΌ (0...(πΉβπ₯)) β Fin) |
68 | 47, 67 | eqeltrd 2834 |
1
β’ (πΉ β π· β {π¦ β π· β£ π¦ βr β€ πΉ} β Fin) |