Step | Hyp | Ref
| Expression |
1 | | resundir 5569 |
. . . . . 6
⊢
((((rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) ∘ card) ∪ ((V ∖ Fin) × {+∞}))
↾ Fin) = ((((rec((𝑥
∈ V ↦ (𝑥 + 1)),
0) ↾ ω) ∘ card) ↾ Fin) ∪ (((V ∖ Fin) ×
{+∞}) ↾ Fin)) |
2 | | eqid 2760 |
. . . . . . . . . 10
⊢
(rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) = (rec((𝑥
∈ V ↦ (𝑥 + 1)),
0) ↾ ω) |
3 | | eqid 2760 |
. . . . . . . . . 10
⊢
((rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) ∘ card) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ∘
card) |
4 | 2, 3 | hashkf 13313 |
. . . . . . . . 9
⊢
((rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) ∘ card):Fin⟶ℕ0 |
5 | | ffn 6206 |
. . . . . . . . 9
⊢
(((rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) ∘ card):Fin⟶ℕ0 →
((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω) ∘ card) Fn Fin) |
6 | | fnresdm 6161 |
. . . . . . . . 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 | | incom 3948 |
. . . . . . . . . 10
⊢ ((V
∖ Fin) ∩ Fin) = (Fin ∩ (V ∖ Fin)) |
9 | | disjdif 4184 |
. . . . . . . . . 10
⊢ (Fin
∩ (V ∖ Fin)) = ∅ |
10 | 8, 9 | eqtri 2782 |
. . . . . . . . 9
⊢ ((V
∖ Fin) ∩ Fin) = ∅ |
11 | | pnfex 10285 |
. . . . . . . . . . 11
⊢ +∞
∈ V |
12 | 11 | fconst 6252 |
. . . . . . . . . 10
⊢ ((V
∖ Fin) × {+∞}):(V ∖
Fin)⟶{+∞} |
13 | | ffn 6206 |
. . . . . . . . . 10
⊢ (((V
∖ Fin) × {+∞}):(V ∖ Fin)⟶{+∞} → ((V
∖ Fin) × {+∞}) Fn (V ∖ Fin)) |
14 | | fnresdisj 6162 |
. . . . . . . . . 10
⊢ (((V
∖ Fin) × {+∞}) Fn (V ∖ Fin) → (((V ∖ Fin)
∩ Fin) = ∅ ↔ (((V ∖ Fin) × {+∞}) ↾ Fin)
= ∅)) |
15 | 12, 13, 14 | mp2b 10 |
. . . . . . . . 9
⊢ (((V
∖ Fin) ∩ Fin) = ∅ ↔ (((V ∖ Fin) × {+∞})
↾ Fin) = ∅) |
16 | 10, 15 | mpbi 220 |
. . . . . . . 8
⊢ (((V
∖ Fin) × {+∞}) ↾ Fin) = ∅ |
17 | 7, 16 | uneq12i 3908 |
. . . . . . 7
⊢
((((rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) ∘ card) ↾ Fin) ∪ (((V ∖ Fin) ×
{+∞}) ↾ Fin)) = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ∘ card)
∪ ∅) |
18 | | un0 4110 |
. . . . . . 7
⊢
(((rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) ∘ card) ∪ ∅) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ∘
card) |
19 | 17, 18 | eqtri 2782 |
. . . . . 6
⊢
((((rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) ∘ card) ↾ Fin) ∪ (((V ∖ Fin) ×
{+∞}) ↾ Fin)) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ∘
card) |
20 | 1, 19 | eqtri 2782 |
. . . . 5
⊢
((((rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) ∘ card) ∪ ((V ∖ Fin) × {+∞}))
↾ Fin) = ((rec((𝑥
∈ V ↦ (𝑥 + 1)),
0) ↾ ω) ∘ card) |
21 | | df-hash 13312 |
. . . . . 6
⊢ ♯ =
(((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω) ∘ card) ∪ ((V ∖ Fin) ×
{+∞})) |
22 | 21 | reseq1i 5547 |
. . . . 5
⊢ (♯
↾ Fin) = ((((rec((𝑥
∈ V ↦ (𝑥 + 1)),
0) ↾ ω) ∘ card) ∪ ((V ∖ Fin) × {+∞}))
↾ Fin) |
23 | | hashgval.1 |
. . . . . 6
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) |
24 | 23 | coeq1i 5437 |
. . . . 5
⊢ (𝐺 ∘ card) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
∘ card) |
25 | 20, 22, 24 | 3eqtr4i 2792 |
. . . 4
⊢ (♯
↾ Fin) = (𝐺 ∘
card) |
26 | 25 | fveq1i 6353 |
. . 3
⊢ ((♯
↾ Fin)‘𝐴) =
((𝐺 ∘
card)‘𝐴) |
27 | | cardf2 8959 |
. . . . 5
⊢
card:{𝑥 ∣
∃𝑦 ∈ On 𝑦 ≈ 𝑥}⟶On |
28 | | ffun 6209 |
. . . . 5
⊢
(card:{𝑥 ∣
∃𝑦 ∈ On 𝑦 ≈ 𝑥}⟶On → Fun card) |
29 | 27, 28 | ax-mp 5 |
. . . 4
⊢ Fun
card |
30 | | finnum 8964 |
. . . 4
⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom
card) |
31 | | fvco 6436 |
. . . 4
⊢ ((Fun
card ∧ 𝐴 ∈ dom
card) → ((𝐺 ∘
card)‘𝐴) = (𝐺‘(card‘𝐴))) |
32 | 29, 30, 31 | sylancr 698 |
. . 3
⊢ (𝐴 ∈ Fin → ((𝐺 ∘ card)‘𝐴) = (𝐺‘(card‘𝐴))) |
33 | 26, 32 | syl5eq 2806 |
. 2
⊢ (𝐴 ∈ Fin → ((♯
↾ Fin)‘𝐴) =
(𝐺‘(card‘𝐴))) |
34 | | fvres 6368 |
. 2
⊢ (𝐴 ∈ Fin → ((♯
↾ Fin)‘𝐴) =
(♯‘𝐴)) |
35 | 33, 34 | eqtr3d 2796 |
1
⊢ (𝐴 ∈ Fin → (𝐺‘(card‘𝐴)) = (♯‘𝐴)) |