This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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