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 ⊢ G = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω
Assertion hashginv ⊢ A ∈ Fin → G -1 ⁡ A = card ⁡ A

Proof

Step Hyp Ref Expression
1 hashgval.1 ⊢ G = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω
2 ficardom ⊢ A ∈ Fin → card ⁡ A ∈ ω
3 1 hashgval ⊢ A ∈ Fin → G ⁡ card ⁡ A = A
4 1 hashgf1o ⊢ G : ω ⟶ 1-1 onto ℕ 0
5 f1ocnvfv ⊢ G : ω ⟶ 1-1 onto ℕ 0 ∧ card ⁡ A ∈ ω → G ⁡ card ⁡ A = A → G -1 ⁡ A = card ⁡ A
6 4 5 mpan ⊢ card ⁡ A ∈ ω → G ⁡ card ⁡ A = A → G -1 ⁡ A = card ⁡ A
7 2 3 6 sylc ⊢ A ∈ Fin → G -1 ⁡ A = card ⁡ A