# Metamath Proof Explorer

## 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 ℕ\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\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 {ℕ}_{0}$
2 elnn0 ${⊢}\left|{A}\right|\in {ℕ}_{0}↔\left(\left|{A}\right|\in ℕ\vee \left|{A}\right|=0\right)$
3 1 2 sylib ${⊢}{A}\in \mathrm{Fin}\to \left(\left|{A}\right|\in ℕ\vee \left|{A}\right|=0\right)$
4 3 orcomd ${⊢}{A}\in \mathrm{Fin}\to \left(\left|{A}\right|=0\vee \left|{A}\right|\in ℕ\right)$
5 hasheq0 ${⊢}{A}\in \mathrm{Fin}\to \left(\left|{A}\right|=0↔{A}=\varnothing \right)$
6 isfinite4 ${⊢}{A}\in \mathrm{Fin}↔\left(1\dots \left|{A}\right|\right)\approx {A}$
7 bren ${⊢}\left(1\dots \left|{A}\right|\right)\approx {A}↔\exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}$
8 6 7 sylbb ${⊢}{A}\in \mathrm{Fin}\to \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\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 ℕ↔\left(\left|{A}\right|\in ℕ\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\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 ℕ\right)↔\left({A}=\varnothing \vee \left(\left|{A}\right|\in ℕ\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\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 ℕ\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)$