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+10↾ω-1⁡A=rec⁡x∈V⟼x+10↾ω-1⁡B
2 eqid ⊢rec⁡x∈V⟼x+10↾ω=rec⁡x∈V⟼x+10↾ω
3 2 hashginv ⊢A∈Fin→rec⁡x∈V⟼x+10↾ω-1⁡A=card⁡A
4 2 hashginv ⊢B∈Fin→rec⁡x∈V⟼x+10↾ω-1⁡B=card⁡B
5 3 4 eqeqan12d ⊢A∈Fin∧B∈Fin→rec⁡x∈V⟼x+10↾ω-1⁡A=rec⁡x∈V⟼x+10↾ω-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+10↾ω⁡card⁡A=rec⁡x∈V⟼x+10↾ω⁡card⁡B
8 2 hashgval ⊢A∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡A=A
9 2 hashgval ⊢B∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡B=B
10 8 9 eqeqan12d ⊢A∈Fin∧B∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡A=rec⁡x∈V⟼x+10↾ω⁡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