Theorem 0fz1

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

	Ref	Expression
Assertion	0fz1	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 Fn ( 1 ... 𝑁 ) ) → ( 𝐹 = ∅ ↔ 𝑁 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		fn0	⊢ ( 𝐹 Fn ∅ ↔ 𝐹 = ∅ )
2		fndmu	⊢ ( ( 𝐹 Fn ( 1 ... 𝑁 ) ∧ 𝐹 Fn ∅ ) → ( 1 ... 𝑁 ) = ∅ )
3	1 2	sylan2br	⊢ ( ( 𝐹 Fn ( 1 ... 𝑁 ) ∧ 𝐹 = ∅ ) → ( 1 ... 𝑁 ) = ∅ )
4	3	ex	⊢ ( 𝐹 Fn ( 1 ... 𝑁 ) → ( 𝐹 = ∅ → ( 1 ... 𝑁 ) = ∅ ) )
5		fneq2	⊢ ( ( 1 ... 𝑁 ) = ∅ → ( 𝐹 Fn ( 1 ... 𝑁 ) ↔ 𝐹 Fn ∅ ) )
6	5 1	bitrdi	⊢ ( ( 1 ... 𝑁 ) = ∅ → ( 𝐹 Fn ( 1 ... 𝑁 ) ↔ 𝐹 = ∅ ) )
7	6	biimpcd	⊢ ( 𝐹 Fn ( 1 ... 𝑁 ) → ( ( 1 ... 𝑁 ) = ∅ → 𝐹 = ∅ ) )
8	4 7	impbid	⊢ ( 𝐹 Fn ( 1 ... 𝑁 ) → ( 𝐹 = ∅ ↔ ( 1 ... 𝑁 ) = ∅ ) )
9		fz1n	⊢ ( 𝑁 ∈ ℕ0 → ( ( 1 ... 𝑁 ) = ∅ ↔ 𝑁 = 0 ) )
10	8 9	sylan9bbr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 Fn ( 1 ... 𝑁 ) ) → ( 𝐹 = ∅ ↔ 𝑁 = 0 ) )