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 ) ) )