Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . 3
⊢
(rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) = (rec((𝑥
∈ V ↦ (𝑥 + 1)),
0) ↾ ω) |
2 | 1 | hashgval 13778 |
. 2
⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) = (♯‘𝐴)) |
3 | | ficardom 9456 |
. . 3
⊢ (𝐴 ∈ Fin →
(card‘𝐴) ∈
ω) |
4 | 1 | hashgf1o 13423 |
. . . . 5
⊢
(rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω):ω–1-1-onto→ℕ0 |
5 | | f1of 6612 |
. . . . 5
⊢
((rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω):ω–1-1-onto→ℕ0 → (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω):ω⟶ℕ0) |
6 | 4, 5 | ax-mp 5 |
. . . 4
⊢
(rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω):ω⟶ℕ0 |
7 | 6 | ffvelrni 6854 |
. . 3
⊢
((card‘𝐴)
∈ ω → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) ∈
ℕ0) |
8 | 3, 7 | syl 17 |
. 2
⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾
ω)‘(card‘𝐴)) ∈
ℕ0) |
9 | 2, 8 | eqeltrrd 2834 |
1
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℕ0) |