This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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