Theorem hasheqf1o

Description: The size of two finite sets is equal if and only if there is a bijection mapping one of the sets onto the other. (Contributed by Alexander van der Vekens, 17-Dec-2017)

	Ref	Expression
Assertion	hasheqf1o	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left(\left|A\right|=\left|B\right|\leftrightarrow \exists ff:A\underset{1-1\; onto}{⟶}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		hashen	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left(\left|A\right|=\left|B\right|\leftrightarrow A\approx B\right)$$
2		bren	$$⊢A\approx B\leftrightarrow \exists ff:A\underset{1-1\; onto}{⟶}B$$
3	1 2	bitrdi	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left(\left|A\right|=\left|B\right|\leftrightarrow \exists ff:A\underset{1-1\; onto}{⟶}B\right)$$