# Metamath Proof Explorer

## Theorem fz1f1o

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

Ref Expression
Assertion fz1f1o ( 𝐴 ∈ Fin → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) )

### Proof

Step Hyp Ref Expression
1 hashcl ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
2 elnn0 ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ↔ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∨ ( ♯ ‘ 𝐴 ) = 0 ) )
3 1 2 sylib ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∨ ( ♯ ‘ 𝐴 ) = 0 ) )
4 3 orcomd ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) = 0 ∨ ( ♯ ‘ 𝐴 ) ∈ ℕ ) )
5 hasheq0 ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) = 0 ↔ 𝐴 = ∅ ) )
6 isfinite4 ( 𝐴 ∈ Fin ↔ ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 )
7 bren ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ≈ 𝐴 ↔ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 )
8 6 7 sylbb ( 𝐴 ∈ Fin → ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 )
9 8 biantrud ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) )
10 5 9 orbi12d ( 𝐴 ∈ Fin → ( ( ( ♯ ‘ 𝐴 ) = 0 ∨ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ↔ ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) ) )
11 4 10 mpbid ( 𝐴 ∈ Fin → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) )