Step | Hyp | Ref
| Expression |
1 | | resundir 5957 |
. . . . . 6
β’
((((rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) β card) βͺ ((V β Fin) Γ {+β}))
βΎ Fin) = ((((rec((π₯
β V β¦ (π₯ + 1)),
0) βΎ Ο) β card) βΎ Fin) βͺ (((V β Fin) Γ
{+β}) βΎ Fin)) |
2 | | eqid 2737 |
. . . . . . . . . 10
β’
(rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) = (rec((π₯
β V β¦ (π₯ + 1)),
0) βΎ Ο) |
3 | | eqid 2737 |
. . . . . . . . . 10
β’
((rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) β card) = ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ Ο) β
card) |
4 | 2, 3 | hashkf 14239 |
. . . . . . . . 9
β’
((rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) β card):FinβΆβ0 |
5 | | ffn 6673 |
. . . . . . . . 9
β’
(((rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) β card):FinβΆβ0 β
((rec((π₯ β V β¦
(π₯ + 1)), 0) βΎ
Ο) β card) Fn Fin) |
6 | | fnresdm 6625 |
. . . . . . . . 9
β’
(((rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) β card) Fn Fin β (((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ Ο) β card)
βΎ Fin) = ((rec((π₯
β V β¦ (π₯ + 1)),
0) βΎ Ο) β card)) |
7 | 4, 5, 6 | mp2b 10 |
. . . . . . . 8
β’
(((rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) β card) βΎ Fin) = ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ Ο) β
card) |
8 | | disjdifr 4437 |
. . . . . . . . 9
β’ ((V
β Fin) β© Fin) = β
|
9 | | pnfex 11215 |
. . . . . . . . . . 11
β’ +β
β V |
10 | 9 | fconst 6733 |
. . . . . . . . . 10
β’ ((V
β Fin) Γ {+β}):(V β
Fin)βΆ{+β} |
11 | | ffn 6673 |
. . . . . . . . . 10
β’ (((V
β Fin) Γ {+β}):(V β Fin)βΆ{+β} β ((V
β Fin) Γ {+β}) Fn (V β Fin)) |
12 | | fnresdisj 6626 |
. . . . . . . . . 10
β’ (((V
β Fin) Γ {+β}) Fn (V β Fin) β (((V β Fin)
β© Fin) = β
β (((V β Fin) Γ {+β}) βΎ Fin)
= β
)) |
13 | 10, 11, 12 | mp2b 10 |
. . . . . . . . 9
β’ (((V
β Fin) β© Fin) = β
β (((V β Fin) Γ {+β})
βΎ Fin) = β
) |
14 | 8, 13 | mpbi 229 |
. . . . . . . 8
β’ (((V
β Fin) Γ {+β}) βΎ Fin) = β
|
15 | 7, 14 | uneq12i 4126 |
. . . . . . 7
β’
((((rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) β card) βΎ Fin) βͺ (((V β Fin) Γ
{+β}) βΎ Fin)) = (((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ Ο) β card)
βͺ β
) |
16 | | un0 4355 |
. . . . . . 7
β’
(((rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) β card) βͺ β
) = ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ Ο) β
card) |
17 | 15, 16 | eqtri 2765 |
. . . . . 6
β’
((((rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) β card) βΎ Fin) βͺ (((V β Fin) Γ
{+β}) βΎ Fin)) = ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ Ο) β
card) |
18 | 1, 17 | eqtri 2765 |
. . . . 5
β’
((((rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) β card) βͺ ((V β Fin) Γ {+β}))
βΎ Fin) = ((rec((π₯
β V β¦ (π₯ + 1)),
0) βΎ Ο) β card) |
19 | | df-hash 14238 |
. . . . . 6
β’ β― =
(((rec((π₯ β V β¦
(π₯ + 1)), 0) βΎ
Ο) β card) βͺ ((V β Fin) Γ
{+β})) |
20 | 19 | reseq1i 5938 |
. . . . 5
β’ (β―
βΎ Fin) = ((((rec((π₯
β V β¦ (π₯ + 1)),
0) βΎ Ο) β card) βͺ ((V β Fin) Γ {+β}))
βΎ Fin) |
21 | | hashgval.1 |
. . . . . 6
β’ πΊ = (rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ Ο) |
22 | 21 | coeq1i 5820 |
. . . . 5
β’ (πΊ β card) = ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ Ο)
β card) |
23 | 18, 20, 22 | 3eqtr4i 2775 |
. . . 4
β’ (β―
βΎ Fin) = (πΊ β
card) |
24 | 23 | fveq1i 6848 |
. . 3
β’ ((β―
βΎ Fin)βπ΄) =
((πΊ β
card)βπ΄) |
25 | | cardf2 9886 |
. . . . 5
β’
card:{π₯ β£
βπ¦ β On π¦ β π₯}βΆOn |
26 | | ffun 6676 |
. . . . 5
β’
(card:{π₯ β£
βπ¦ β On π¦ β π₯}βΆOn β Fun card) |
27 | 25, 26 | ax-mp 5 |
. . . 4
β’ Fun
card |
28 | | finnum 9891 |
. . . 4
β’ (π΄ β Fin β π΄ β dom
card) |
29 | | fvco 6944 |
. . . 4
β’ ((Fun
card β§ π΄ β dom
card) β ((πΊ β
card)βπ΄) = (πΊβ(cardβπ΄))) |
30 | 27, 28, 29 | sylancr 588 |
. . 3
β’ (π΄ β Fin β ((πΊ β card)βπ΄) = (πΊβ(cardβπ΄))) |
31 | 24, 30 | eqtrid 2789 |
. 2
β’ (π΄ β Fin β ((β―
βΎ Fin)βπ΄) =
(πΊβ(cardβπ΄))) |
32 | | fvres 6866 |
. 2
β’ (π΄ β Fin β ((β―
βΎ Fin)βπ΄) =
(β―βπ΄)) |
33 | 31, 32 | eqtr3d 2779 |
1
β’ (π΄ β Fin β (πΊβ(cardβπ΄)) = (β―βπ΄)) |