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