Step |
Hyp |
Ref |
Expression |
1 |
|
hashgval.1 |
⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) |
2 |
|
ficardom |
⊢ ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ∈ ω ) |
3 |
1
|
hashgval |
⊢ ( 𝐴 ∈ Fin → ( 𝐺 ‘ ( card ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) ) |
4 |
1
|
hashgf1o |
⊢ 𝐺 : ω –1-1-onto→ ℕ0 |
5 |
|
f1ocnvfv |
⊢ ( ( 𝐺 : ω –1-1-onto→ ℕ0 ∧ ( card ‘ 𝐴 ) ∈ ω ) → ( ( 𝐺 ‘ ( card ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) → ( ◡ 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) = ( card ‘ 𝐴 ) ) ) |
6 |
4 5
|
mpan |
⊢ ( ( card ‘ 𝐴 ) ∈ ω → ( ( 𝐺 ‘ ( card ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) → ( ◡ 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) = ( card ‘ 𝐴 ) ) ) |
7 |
2 3 6
|
sylc |
⊢ ( 𝐴 ∈ Fin → ( ◡ 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) = ( card ‘ 𝐴 ) ) |