Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . 5
β’
{β¨π₯, π¦β© β£ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€)))} = {β¨π₯, π¦β© β£ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€)))} |
2 | | breq1 5109 |
. . . . . 6
β’ (β = π₯ β (β finSupp 0 β π₯ finSupp 0)) |
3 | 2 | cbvrabv 3416 |
. . . . 5
β’ {β β (β0
βm πΌ)
β£ β finSupp 0} =
{π₯ β
(β0 βm πΌ) β£ π₯ finSupp 0} |
4 | | ltbwe.w |
. . . . 5
β’ (π β π We πΌ) |
5 | | nn0uz 12810 |
. . . . . 6
β’
β0 = (β€β₯β0) |
6 | | ltweuz 13872 |
. . . . . . 7
β’ < We
(β€β₯β0) |
7 | | weeq2 5623 |
. . . . . . 7
β’
(β0 = (β€β₯β0) β ( < We
β0 β < We
(β€β₯β0))) |
8 | 6, 7 | mpbiri 258 |
. . . . . 6
β’
(β0 = (β€β₯β0) β < We
β0) |
9 | 5, 8 | mp1i 13 |
. . . . 5
β’ (π β < We
β0) |
10 | | 0nn0 12433 |
. . . . . 6
β’ 0 β
β0 |
11 | | ne0i 4295 |
. . . . . 6
β’ (0 β
β0 β β0 β β
) |
12 | 10, 11 | mp1i 13 |
. . . . 5
β’ (π β β0 β
β
) |
13 | | eqid 2733 |
. . . . 5
β’
OrdIso(π, πΌ) = OrdIso(π, πΌ) |
14 | | 0z 12515 |
. . . . . . 7
β’ 0 β
β€ |
15 | | hashgval2 14284 |
. . . . . . 7
β’ (β―
βΎ Ο) = (rec((π₯
β V β¦ (π₯ + 1)),
0) βΎ Ο) |
16 | 14, 15 | om2uzoi 13866 |
. . . . . 6
β’ (β―
βΎ Ο) = OrdIso( < ,
(β€β₯β0)) |
17 | | oieq2 9454 |
. . . . . . 7
β’
(β0 = (β€β₯β0) β OrdIso(
< , β0) = OrdIso( < ,
(β€β₯β0))) |
18 | 5, 17 | ax-mp 5 |
. . . . . 6
β’ OrdIso(
< , β0) = OrdIso( < ,
(β€β₯β0)) |
19 | 16, 18 | eqtr4i 2764 |
. . . . 5
β’ (β―
βΎ Ο) = OrdIso( < , β0) |
20 | | peano1 7826 |
. . . . . . 7
β’ β
β Ο |
21 | | fvres 6862 |
. . . . . . 7
β’ (β
β Ο β ((β― βΎ Ο)ββ
) =
(β―ββ
)) |
22 | 20, 21 | ax-mp 5 |
. . . . . 6
β’ ((β―
βΎ Ο)ββ
) = (β―ββ
) |
23 | | hash0 14273 |
. . . . . 6
β’
(β―ββ
) = 0 |
24 | 22, 23 | eqtr2i 2762 |
. . . . 5
β’ 0 =
((β― βΎ Ο)ββ
) |
25 | 1, 3, 4, 9, 12, 13, 19, 24 | wemapwe 9638 |
. . . 4
β’ (π β {β¨π₯, π¦β© β£ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€)))} We {β β (β0
βm πΌ)
β£ β finSupp
0}) |
26 | | ltbval.d |
. . . . . 6
β’ π· = {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} |
27 | | elmapfun 8807 |
. . . . . . . . . 10
β’ (β β (β0
βm πΌ)
β Fun β) |
28 | 27 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ β β (β0
βm πΌ))
β Fun β) |
29 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ β β (β0
βm πΌ))
β β β
(β0 βm πΌ)) |
30 | | c0ex 11154 |
. . . . . . . . . 10
β’ 0 β
V |
31 | 30 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ β β (β0
βm πΌ))
β 0 β V) |
32 | | funisfsupp 9314 |
. . . . . . . . 9
β’ ((Fun
β β§ β β (β0
βm πΌ) β§
0 β V) β (β
finSupp 0 β (β supp 0)
β Fin)) |
33 | 28, 29, 31, 32 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ β β (β0
βm πΌ))
β (β finSupp 0 β
(β supp 0) β
Fin)) |
34 | | ltbval.i |
. . . . . . . . 9
β’ (π β πΌ β π) |
35 | | elmapi 8790 |
. . . . . . . . 9
β’ (β β (β0
βm πΌ)
β β:πΌβΆβ0) |
36 | | fcdmnn0supp 12474 |
. . . . . . . . . 10
β’ ((πΌ β π β§ β:πΌβΆβ0) β (β supp 0) = (β‘β β β)) |
37 | 36 | eleq1d 2819 |
. . . . . . . . 9
β’ ((πΌ β π β§ β:πΌβΆβ0) β ((β supp 0) β Fin β (β‘β β β) β
Fin)) |
38 | 34, 35, 37 | syl2an 597 |
. . . . . . . 8
β’ ((π β§ β β (β0
βm πΌ))
β ((β supp 0) β
Fin β (β‘β β β) β
Fin)) |
39 | 33, 38 | bitr2d 280 |
. . . . . . 7
β’ ((π β§ β β (β0
βm πΌ))
β ((β‘β β β) β Fin β β finSupp 0)) |
40 | 39 | rabbidva 3413 |
. . . . . 6
β’ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} = {β β (β0
βm πΌ)
β£ β finSupp
0}) |
41 | 26, 40 | eqtrid 2785 |
. . . . 5
β’ (π β π· = {β β (β0
βm πΌ)
β£ β finSupp
0}) |
42 | | weeq2 5623 |
. . . . 5
β’ (π· = {β β (β0
βm πΌ)
β£ β finSupp 0} β
({β¨π₯, π¦β© β£ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€)))} We π· β {β¨π₯, π¦β© β£ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€)))} We {β β (β0
βm πΌ)
β£ β finSupp
0})) |
43 | 41, 42 | syl 17 |
. . . 4
β’ (π β ({β¨π₯, π¦β© β£ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€)))} We π· β {β¨π₯, π¦β© β£ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€)))} We {β β (β0
βm πΌ)
β£ β finSupp
0})) |
44 | 25, 43 | mpbird 257 |
. . 3
β’ (π β {β¨π₯, π¦β© β£ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€)))} We π·) |
45 | | weinxp 5717 |
. . 3
β’
({β¨π₯, π¦β© β£ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€)))} We π· β ({β¨π₯, π¦β© β£ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€)))} β© (π· Γ π·)) We π·) |
46 | 44, 45 | sylib 217 |
. 2
β’ (π β ({β¨π₯, π¦β© β£ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€)))} β© (π· Γ π·)) We π·) |
47 | | ltbval.c |
. . . . 5
β’ πΆ = (π <bag πΌ) |
48 | | ltbval.t |
. . . . 5
β’ (π β π β π) |
49 | 47, 26, 34, 48 | ltbval 21460 |
. . . 4
β’ (π β πΆ = {β¨π₯, π¦β© β£ ({π₯, π¦} β π· β§ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€))))}) |
50 | | df-xp 5640 |
. . . . . . 7
β’ (π· Γ π·) = {β¨π₯, π¦β© β£ (π₯ β π· β§ π¦ β π·)} |
51 | | vex 3448 |
. . . . . . . . 9
β’ π₯ β V |
52 | | vex 3448 |
. . . . . . . . 9
β’ π¦ β V |
53 | 51, 52 | prss 4781 |
. . . . . . . 8
β’ ((π₯ β π· β§ π¦ β π·) β {π₯, π¦} β π·) |
54 | 53 | opabbii 5173 |
. . . . . . 7
β’
{β¨π₯, π¦β© β£ (π₯ β π· β§ π¦ β π·)} = {β¨π₯, π¦β© β£ {π₯, π¦} β π·} |
55 | 50, 54 | eqtr2i 2762 |
. . . . . 6
β’
{β¨π₯, π¦β© β£ {π₯, π¦} β π·} = (π· Γ π·) |
56 | 55 | ineq1i 4169 |
. . . . 5
β’
({β¨π₯, π¦β© β£ {π₯, π¦} β π·} β© {β¨π₯, π¦β© β£ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€)))}) = ((π· Γ π·) β© {β¨π₯, π¦β© β£ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€)))}) |
57 | | inopab 5786 |
. . . . 5
β’
({β¨π₯, π¦β© β£ {π₯, π¦} β π·} β© {β¨π₯, π¦β© β£ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€)))}) = {β¨π₯, π¦β© β£ ({π₯, π¦} β π· β§ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€))))} |
58 | | incom 4162 |
. . . . 5
β’ ((π· Γ π·) β© {β¨π₯, π¦β© β£ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€)))}) = ({β¨π₯, π¦β© β£ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€)))} β© (π· Γ π·)) |
59 | 56, 57, 58 | 3eqtr3i 2769 |
. . . 4
β’
{β¨π₯, π¦β© β£ ({π₯, π¦} β π· β§ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€))))} = ({β¨π₯, π¦β© β£ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€)))} β© (π· Γ π·)) |
60 | 49, 59 | eqtrdi 2789 |
. . 3
β’ (π β πΆ = ({β¨π₯, π¦β© β£ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€)))} β© (π· Γ π·))) |
61 | | weeq1 5622 |
. . 3
β’ (πΆ = ({β¨π₯, π¦β© β£ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€)))} β© (π· Γ π·)) β (πΆ We π· β ({β¨π₯, π¦β© β£ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€)))} β© (π· Γ π·)) We π·)) |
62 | 60, 61 | syl 17 |
. 2
β’ (π β (πΆ We π· β ({β¨π₯, π¦β© β£ βπ§ β πΌ ((π₯βπ§) < (π¦βπ§) β§ βπ€ β πΌ (π§ππ€ β (π₯βπ€) = (π¦βπ€)))} β© (π· Γ π·)) We π·)) |
63 | 46, 62 | mpbird 257 |
1
β’ (π β πΆ We π·) |