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 ∈ Fin → A = ∅ ∨ A ∈ ℕ ∧ ∃ f f : 1 … A ⟶ 1-1 onto A

Proof

Step Hyp Ref Expression
1 hashcl ⊢ A ∈ Fin → A ∈ ℕ 0
2 elnn0 ⊢ A ∈ ℕ 0 ↔ A ∈ ℕ ∨ A = 0
3 1 2 sylib ⊢ A ∈ Fin → A ∈ ℕ ∨ A = 0
4 3 orcomd ⊢ A ∈ Fin → A = 0 ∨ A ∈ ℕ
5 hasheq0 ⊢ A ∈ Fin → A = 0 ↔ A = ∅
6 isfinite4 ⊢ A ∈ Fin ↔ 1 … A ≈ A
7 bren ⊢ 1 … A ≈ A ↔ ∃ f f : 1 … A ⟶ 1-1 onto A
8 6 7 sylbb ⊢ A ∈ Fin → ∃ f f : 1 … A ⟶ 1-1 onto A
9 8 biantrud ⊢ A ∈ Fin → A ∈ ℕ ↔ A ∈ ℕ ∧ ∃ f f : 1 … A ⟶ 1-1 onto A
10 5 9 orbi12d ⊢ A ∈ Fin → A = 0 ∨ A ∈ ℕ ↔ A = ∅ ∨ A ∈ ℕ ∧ ∃ f f : 1 … A ⟶ 1-1 onto A
11 4 10 mpbid ⊢ A ∈ Fin → A = ∅ ∨ A ∈ ℕ ∧ ∃ f f : 1 … A ⟶ 1-1 onto A