# 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 ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left(\left|{A}\right|=\left|{B}\right|↔{A}\approx {B}\right)$

### Proof

Step Hyp Ref Expression
1 fveq2 ${⊢}\left|{A}\right|=\left|{B}\right|\to {\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)}^{-1}\left(\left|{A}\right|\right)={\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)}^{-1}\left(\left|{B}\right|\right)$
2 eqid ${⊢}{\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}={\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}$
3 2 hashginv ${⊢}{A}\in \mathrm{Fin}\to {\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)}^{-1}\left(\left|{A}\right|\right)=\mathrm{card}\left({A}\right)$
4 2 hashginv ${⊢}{B}\in \mathrm{Fin}\to {\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)}^{-1}\left(\left|{B}\right|\right)=\mathrm{card}\left({B}\right)$
5 3 4 eqeqan12d ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left({\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)}^{-1}\left(\left|{A}\right|\right)={\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)}^{-1}\left(\left|{B}\right|\right)↔\mathrm{card}\left({A}\right)=\mathrm{card}\left({B}\right)\right)$
6 1 5 syl5ib ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left(\left|{A}\right|=\left|{B}\right|\to \mathrm{card}\left({A}\right)=\mathrm{card}\left({B}\right)\right)$
7 fveq2 ${⊢}\mathrm{card}\left({A}\right)=\mathrm{card}\left({B}\right)\to \left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{card}\left({A}\right)\right)=\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{card}\left({B}\right)\right)$
8 2 hashgval ${⊢}{A}\in \mathrm{Fin}\to \left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{card}\left({A}\right)\right)=\left|{A}\right|$
9 2 hashgval ${⊢}{B}\in \mathrm{Fin}\to \left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{card}\left({B}\right)\right)=\left|{B}\right|$
10 8 9 eqeqan12d ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left(\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{card}\left({A}\right)\right)=\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{card}\left({B}\right)\right)↔\left|{A}\right|=\left|{B}\right|\right)$
11 7 10 syl5ib ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left(\mathrm{card}\left({A}\right)=\mathrm{card}\left({B}\right)\to \left|{A}\right|=\left|{B}\right|\right)$
12 6 11 impbid ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left(\left|{A}\right|=\left|{B}\right|↔\mathrm{card}\left({A}\right)=\mathrm{card}\left({B}\right)\right)$
13 finnum ${⊢}{A}\in \mathrm{Fin}\to {A}\in \mathrm{dom}\mathrm{card}$
14 finnum ${⊢}{B}\in \mathrm{Fin}\to {B}\in \mathrm{dom}\mathrm{card}$
15 carden2 ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge {B}\in \mathrm{dom}\mathrm{card}\right)\to \left(\mathrm{card}\left({A}\right)=\mathrm{card}\left({B}\right)↔{A}\approx {B}\right)$
16 13 14 15 syl2an ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left(\mathrm{card}\left({A}\right)=\mathrm{card}\left({B}\right)↔{A}\approx {B}\right)$
17 12 16 bitrd ${⊢}\left({A}\in \mathrm{Fin}\wedge {B}\in \mathrm{Fin}\right)\to \left(\left|{A}\right|=\left|{B}\right|↔{A}\approx {B}\right)$