# 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 e. Fin -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )`

### Proof

Step Hyp Ref Expression
1 hashcl
` |-  ( A e. Fin -> ( # ` A ) e. NN0 )`
2 elnn0
` |-  ( ( # ` A ) e. NN0 <-> ( ( # ` A ) e. NN \/ ( # ` A ) = 0 ) )`
3 1 2 sylib
` |-  ( A e. Fin -> ( ( # ` A ) e. NN \/ ( # ` A ) = 0 ) )`
4 3 orcomd
` |-  ( A e. Fin -> ( ( # ` A ) = 0 \/ ( # ` A ) e. NN ) )`
5 hasheq0
` |-  ( A e. Fin -> ( ( # ` A ) = 0 <-> A = (/) ) )`
6 isfinite4
` |-  ( A e. Fin <-> ( 1 ... ( # ` A ) ) ~~ A )`
7 bren
` |-  ( ( 1 ... ( # ` A ) ) ~~ A <-> E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A )`
8 6 7 sylbb
` |-  ( A e. Fin -> E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A )`
9 8 biantrud
` |-  ( A e. Fin -> ( ( # ` A ) e. NN <-> ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )`
10 5 9 orbi12d
` |-  ( A e. Fin -> ( ( ( # ` A ) = 0 \/ ( # ` A ) e. NN ) <-> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) ) )`
11 4 10 mpbid
` |-  ( A e. Fin -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )`