0fz1

Description: Two ways to say a finite 1-based sequence is empty. (Contributed by Paul Chapman, 26-Oct-2012)

		Ref	Expression
	Assertion	0fz1	$⊢ (N \in ℕ_{0} \land F Fn (1 \dots N)) \to (F = \emptyset \leftrightarrow N = 0)$

Step	Hyp	Ref	Expression
1		fn0	$⊢ F Fn \emptyset \leftrightarrow F = \emptyset$
2		fndmu	$⊢ (F Fn (1 \dots N) \land F Fn \emptyset) \to (1 \dots N) = \emptyset$
3	1 2	sylan2br	$⊢ (F Fn (1 \dots N) \land F = \emptyset) \to (1 \dots N) = \emptyset$
4	3	ex	$⊢ F Fn (1 \dots N) \to (F = \emptyset \to (1 \dots N) = \emptyset)$
5		fneq2	$⊢ (1 \dots N) = \emptyset \to (F Fn (1 \dots N) \leftrightarrow F Fn \emptyset)$
6	5 1	bitrdi	$⊢ (1 \dots N) = \emptyset \to (F Fn (1 \dots N) \leftrightarrow F = \emptyset)$
7	6	biimpcd	$⊢ F Fn (1 \dots N) \to ((1 \dots N) = \emptyset \to F = \emptyset)$
8	4 7	impbid	$⊢ F Fn (1 \dots N) \to (F = \emptyset \leftrightarrow (1 \dots N) = \emptyset)$
9		fz1n	$⊢ N \in ℕ_{0} \to ((1 \dots N) = \emptyset \leftrightarrow N = 0)$
10	8 9	sylan9bbr	$⊢ (N \in ℕ_{0} \land F Fn (1 \dots N)) \to (F = \emptyset \leftrightarrow N = 0)$

Metamath Proof Explorer