Step | Hyp | Ref
| Expression |
1 | | elex 3466 |
. 2
β’ (π΄ β π β π΄ β V) |
2 | | eldif 3925 |
. . 3
β’ (π΄ β (V β Fin) β
(π΄ β V β§ Β¬
π΄ β
Fin)) |
3 | | df-hash 14238 |
. . . . . . 7
β’ β― =
(((rec((π₯ β V β¦
(π₯ + 1)), 0) βΎ
Ο) β card) βͺ ((V β Fin) Γ
{+β})) |
4 | 3 | reseq1i 5938 |
. . . . . 6
β’ (β―
βΎ (V β Fin)) = ((((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ Ο) β card)
βͺ ((V β Fin) Γ {+β})) βΎ (V β
Fin)) |
5 | | resundir 5957 |
. . . . . 6
β’
((((rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) β card) βͺ ((V β Fin) Γ {+β}))
βΎ (V β Fin)) = ((((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ Ο) β card)
βΎ (V β Fin)) βͺ (((V β Fin) Γ {+β}) βΎ (V
β Fin))) |
6 | | disjdif 4436 |
. . . . . . . . 9
β’ (Fin
β© (V β Fin)) = β
|
7 | | eqid 2737 |
. . . . . . . . . . 11
β’
(rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) = (rec((π₯
β V β¦ (π₯ + 1)),
0) βΎ Ο) |
8 | | eqid 2737 |
. . . . . . . . . . 11
β’
((rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) β card) = ((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ Ο) β
card) |
9 | 7, 8 | hashkf 14239 |
. . . . . . . . . 10
β’
((rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) β card):FinβΆβ0 |
10 | | ffn 6673 |
. . . . . . . . . 10
β’
(((rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) β card):FinβΆβ0 β
((rec((π₯ β V β¦
(π₯ + 1)), 0) βΎ
Ο) β card) Fn Fin) |
11 | | fnresdisj 6626 |
. . . . . . . . . 10
β’
(((rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) β card) Fn Fin β ((Fin β© (V β Fin)) =
β
β (((rec((π₯
β V β¦ (π₯ + 1)),
0) βΎ Ο) β card) βΎ (V β Fin)) =
β
)) |
12 | 9, 10, 11 | mp2b 10 |
. . . . . . . . 9
β’ ((Fin
β© (V β Fin)) = β
β (((rec((π₯ β V β¦ (π₯ + 1)), 0) βΎ Ο) β card)
βΎ (V β Fin)) = β
) |
13 | 6, 12 | mpbi 229 |
. . . . . . . 8
β’
(((rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) β card) βΎ (V β Fin)) =
β
|
14 | | pnfex 11215 |
. . . . . . . . . 10
β’ +β
β V |
15 | 14 | fconst 6733 |
. . . . . . . . 9
β’ ((V
β Fin) Γ {+β}):(V β
Fin)βΆ{+β} |
16 | | ffn 6673 |
. . . . . . . . 9
β’ (((V
β Fin) Γ {+β}):(V β Fin)βΆ{+β} β ((V
β Fin) Γ {+β}) Fn (V β Fin)) |
17 | | fnresdm 6625 |
. . . . . . . . 9
β’ (((V
β Fin) Γ {+β}) Fn (V β Fin) β (((V β Fin)
Γ {+β}) βΎ (V β Fin)) = ((V β Fin) Γ
{+β})) |
18 | 15, 16, 17 | mp2b 10 |
. . . . . . . 8
β’ (((V
β Fin) Γ {+β}) βΎ (V β Fin)) = ((V β Fin)
Γ {+β}) |
19 | 13, 18 | uneq12i 4126 |
. . . . . . 7
β’
((((rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) β card) βΎ (V β Fin)) βͺ (((V β Fin)
Γ {+β}) βΎ (V β Fin))) = (β
βͺ ((V β Fin)
Γ {+β})) |
20 | | uncom 4118 |
. . . . . . 7
β’ (β
βͺ ((V β Fin) Γ {+β})) = (((V β Fin) Γ
{+β}) βͺ β
) |
21 | | un0 4355 |
. . . . . . 7
β’ (((V
β Fin) Γ {+β}) βͺ β
) = ((V β Fin) Γ
{+β}) |
22 | 19, 20, 21 | 3eqtri 2769 |
. . . . . 6
β’
((((rec((π₯ β V
β¦ (π₯ + 1)), 0)
βΎ Ο) β card) βΎ (V β Fin)) βͺ (((V β Fin)
Γ {+β}) βΎ (V β Fin))) = ((V β Fin) Γ
{+β}) |
23 | 4, 5, 22 | 3eqtri 2769 |
. . . . 5
β’ (β―
βΎ (V β Fin)) = ((V β Fin) Γ
{+β}) |
24 | 23 | fveq1i 6848 |
. . . 4
β’ ((β―
βΎ (V β Fin))βπ΄) = (((V β Fin) Γ
{+β})βπ΄) |
25 | | fvres 6866 |
. . . 4
β’ (π΄ β (V β Fin) β
((β― βΎ (V β Fin))βπ΄) = (β―βπ΄)) |
26 | 14 | fvconst2 7158 |
. . . 4
β’ (π΄ β (V β Fin) β
(((V β Fin) Γ {+β})βπ΄) = +β) |
27 | 24, 25, 26 | 3eqtr3a 2801 |
. . 3
β’ (π΄ β (V β Fin) β
(β―βπ΄) =
+β) |
28 | 2, 27 | sylbir 234 |
. 2
β’ ((π΄ β V β§ Β¬ π΄ β Fin) β
(β―βπ΄) =
+β) |
29 | 1, 28 | sylan 581 |
1
β’ ((π΄ β π β§ Β¬ π΄ β Fin) β (β―βπ΄) = +β) |