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

Metamath Proof Explorer

Theorem hashen

Description: Two finite sets have the same number of elements iff they are equinumerous. (Contributed by Paul Chapman, 22-Jun-2011) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Assertion hashen ⊢ A ∈ Fin ∧ B ∈ Fin → A = B ↔ A ≈ B

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ A = B → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω -1 ⁡ A = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω -1 ⁡ B
2 eqid ⊢ rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω
3 2 hashginv ⊢ A ∈ Fin → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω -1 ⁡ A = card ⁡ A
4 2 hashginv ⊢ B ∈ Fin → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω -1 ⁡ B = card ⁡ B
5 3 4 eqeqan12d ⊢ A ∈ Fin ∧ B ∈ Fin → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω -1 ⁡ A = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω -1 ⁡ B ↔ card ⁡ A = card ⁡ B
6 1 5 imbitrid ⊢ A ∈ Fin ∧ B ∈ Fin → A = B → card ⁡ A = card ⁡ B
7 fveq2 ⊢ card ⁡ A = card ⁡ B → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ A = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ B
8 2 hashgval ⊢ A ∈ Fin → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ A = A
9 2 hashgval ⊢ B ∈ Fin → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ B = B
10 8 9 eqeqan12d ⊢ A ∈ Fin ∧ B ∈ Fin → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ A = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ B ↔ A = B
11 7 10 imbitrid ⊢ A ∈ Fin ∧ B ∈ Fin → card ⁡ A = card ⁡ B → A = B
12 6 11 impbid ⊢ A ∈ Fin ∧ B ∈ Fin → A = B ↔ card ⁡ A = card ⁡ B
13 finnum ⊢ A ∈ Fin → A ∈ dom ⁡ card
14 finnum ⊢ B ∈ Fin → B ∈ dom ⁡ card
15 carden2 ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → card ⁡ A = card ⁡ B ↔ A ≈ B
16 13 14 15 syl2an ⊢ A ∈ Fin ∧ B ∈ Fin → card ⁡ A = card ⁡ B ↔ A ≈ B
17 12 16 bitrd ⊢ A ∈ Fin ∧ B ∈ Fin → A = B ↔ A ≈ B