Step | Hyp | Ref
| Expression |
1 | | resundir 5866 |
. . . . . 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 13898 |
. . . . . . . . 9
⊢
((rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) ∘ card):Fin⟶ℕ0 |
5 | | ffn 6545 |
. . . . . . . . 9
⊢
(((rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) ∘ card):Fin⟶ℕ0 →
((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω) ∘ card) Fn Fin) |
6 | | fnresdm 6496 |
. . . . . . . . 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 4387 |
. . . . . . . . 9
⊢ ((V
∖ Fin) ∩ Fin) = ∅ |
9 | | pnfex 10886 |
. . . . . . . . . . 11
⊢ +∞
∈ V |
10 | 9 | fconst 6605 |
. . . . . . . . . 10
⊢ ((V
∖ Fin) × {+∞}):(V ∖
Fin)⟶{+∞} |
11 | | ffn 6545 |
. . . . . . . . . 10
⊢ (((V
∖ Fin) × {+∞}):(V ∖ Fin)⟶{+∞} → ((V
∖ Fin) × {+∞}) Fn (V ∖ Fin)) |
12 | | fnresdisj 6497 |
. . . . . . . . . 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 233 |
. . . . . . . 8
⊢ (((V
∖ Fin) × {+∞}) ↾ Fin) = ∅ |
15 | 7, 14 | uneq12i 4075 |
. . . . . . 7
⊢
((((rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) ∘ card) ↾ Fin) ∪ (((V ∖ Fin) ×
{+∞}) ↾ Fin)) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ∘ card)
∪ ∅) |
16 | | un0 4305 |
. . . . . . 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 13897 |
. . . . . 6
⊢ ♯ =
(((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω) ∘ card) ∪ ((V ∖ Fin) ×
{+∞})) |
20 | 19 | reseq1i 5847 |
. . . . 5
⊢ (♯
↾ Fin) = ((((rec((𝑥
∈ V ↦ (𝑥 + 1)),
0) ↾ ω) ∘ card) ∪ ((V ∖ Fin) × {+∞}))
↾ Fin) |
21 | | hashgval.1 |
. . . . . 6
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) |
22 | 21 | coeq1i 5728 |
. . . . 5
⊢ (𝐺 ∘ card) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
∘ card) |
23 | 18, 20, 22 | 3eqtr4i 2775 |
. . . 4
⊢ (♯
↾ Fin) = (𝐺 ∘
card) |
24 | 23 | fveq1i 6718 |
. . 3
⊢ ((♯
↾ Fin)‘𝐴) =
((𝐺 ∘
card)‘𝐴) |
25 | | cardf2 9559 |
. . . . 5
⊢
card:{𝑥 ∣
∃𝑦 ∈ On 𝑦 ≈ 𝑥}⟶On |
26 | | ffun 6548 |
. . . . 5
⊢
(card:{𝑥 ∣
∃𝑦 ∈ On 𝑦 ≈ 𝑥}⟶On → Fun card) |
27 | 25, 26 | ax-mp 5 |
. . . 4
⊢ Fun
card |
28 | | finnum 9564 |
. . . 4
⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom
card) |
29 | | fvco 6809 |
. . . 4
⊢ ((Fun
card ∧ 𝐴 ∈ dom
card) → ((𝐺 ∘
card)‘𝐴) = (𝐺‘(card‘𝐴))) |
30 | 27, 28, 29 | sylancr 590 |
. . 3
⊢ (𝐴 ∈ Fin → ((𝐺 ∘ card)‘𝐴) = (𝐺‘(card‘𝐴))) |
31 | 24, 30 | eqtrid 2789 |
. 2
⊢ (𝐴 ∈ Fin → ((♯
↾ Fin)‘𝐴) =
(𝐺‘(card‘𝐴))) |
32 | | fvres 6736 |
. 2
⊢ (𝐴 ∈ Fin → ((♯
↾ Fin)‘𝐴) =
(♯‘𝐴)) |
33 | 31, 32 | eqtr3d 2779 |
1
⊢ (𝐴 ∈ Fin → (𝐺‘(card‘𝐴)) = (♯‘𝐴)) |