Metamath Proof Explorer


Theorem hashginv

Description: The converse of G maps the size function's value to card . (Contributed by Paul Chapman, 22-Jun-2011) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Hypothesis hashgval.1 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
Assertion hashginv ( 𝐴 ∈ Fin → ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) = ( card ‘ 𝐴 ) )

Proof

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 ‘ 𝐴 ) )