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