fz1f1o

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

		Ref	Expression
	Assertion	fz1f1o	$⊢ A \in Fin \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$

Step	Hyp	Ref	Expression
1		hashcl	$⊢ A \in Fin \to \|A\| \in ℕ_{0}$
2		elnn0	$⊢ \|A\| \in ℕ_{0} \leftrightarrow (\|A\| \in ℕ \lor \|A\| = 0)$
3	1 2	sylib	$⊢ A \in Fin \to (\|A\| \in ℕ \lor \|A\| = 0)$
4	3	orcomd	$⊢ A \in Fin \to (\|A\| = 0 \lor \|A\| \in ℕ)$
5		hasheq0	$⊢ A \in Fin \to (\|A\| = 0 \leftrightarrow A = \emptyset)$
6		isfinite4	$⊢ A \in Fin \leftrightarrow (1 \dots \|A\|) \approx A$
7		bren	$⊢ (1 \dots \|A\|) \approx A \leftrightarrow \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
8	6 7	sylbb	$⊢ A \in Fin \to \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
9	8	biantrud	$⊢ A \in Fin \to (\|A\| \in ℕ \leftrightarrow (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
10	5 9	orbi12d	$⊢ A \in Fin \to ((\|A\| = 0 \lor \|A\| \in ℕ) \leftrightarrow (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)))$
11	4 10	mpbid	$⊢ A \in Fin \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$

Metamath Proof Explorer