Theorem fz1f1o

Description: A lemma for working with finite sums. (Contributed by Mario Carneiro, 22-Apr-2014)

	Ref	Expression
Assertion	fz1f1o	$$⊢A\in \mathrm{Fin}\to \left(A=\varnothing \vee \left(\left|A\right|\in \mathbb{N}\wedge \exists ff:\left(1\dots \left|A\right|\right)\underset{1-1\; onto}{⟶}A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hashcl	$$⊢A\in \mathrm{Fin}\to \left|A\right|\in {\mathbb{N}}_0$$
2		elnn0	$$⊢\left|A\right|\in {\mathbb{N}}_0\leftrightarrow \left(\left|A\right|\in \mathbb{N}\vee \left|A\right|=0\right)$$
3	1 2	sylib	$$⊢A\in \mathrm{Fin}\to \left(\left|A\right|\in \mathbb{N}\vee \left|A\right|=0\right)$$
4	3	orcomd	$$⊢A\in \mathrm{Fin}\to \left(\left|A\right|=0\vee \left|A\right|\in \mathbb{N}\right)$$
5		hasheq0	$$⊢A\in \mathrm{Fin}\to \left(\left|A\right|=0\leftrightarrow A=\varnothing \right)$$
6		isfinite4	$$⊢A\in \mathrm{Fin}\leftrightarrow \left(1\dots \left|A\right|\right)\approx A$$
7		bren	$$⊢\left(1\dots \left|A\right|\right)\approx A\leftrightarrow \exists ff:\left(1\dots \left|A\right|\right)\underset{1-1\; onto}{⟶}A$$
8	6 7	sylbb	$$⊢A\in \mathrm{Fin}\to \exists ff:\left(1\dots \left|A\right|\right)\underset{1-1\; onto}{⟶}A$$
9	8	biantrud	$$⊢A\in \mathrm{Fin}\to \left(\left|A\right|\in \mathbb{N}\leftrightarrow \left(\left|A\right|\in \mathbb{N}\wedge \exists ff:\left(1\dots \left|A\right|\right)\underset{1-1\; onto}{⟶}A\right)\right)$$
10	5 9	orbi12d	$$⊢A\in \mathrm{Fin}\to \left(\left(\left|A\right|=0\vee \left|A\right|\in \mathbb{N}\right)\leftrightarrow \left(A=\varnothing \vee \left(\left|A\right|\in \mathbb{N}\wedge \exists ff:\left(1\dots \left|A\right|\right)\underset{1-1\; onto}{⟶}A\right)\right)\right)$$
11	4 10	mpbid	$$⊢A\in \mathrm{Fin}\to \left(A=\varnothing \vee \left(\left|A\right|\in \mathbb{N}\wedge \exists ff:\left(1\dots \left|A\right|\right)\underset{1-1\; onto}{⟶}A\right)\right)$$