This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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