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 
|- ( ( N e. NN0 /\ F Fn ( 1 ... N ) ) -> ( F = (/) <-> N = 0 ) )

Proof

Step Hyp Ref Expression
1 fn0 
 |-  ( F Fn (/) <-> F = (/) )
2 fndmu 
 |-  ( ( F Fn ( 1 ... N ) /\ F Fn (/) ) -> ( 1 ... N ) = (/) )
3 1 2 sylan2br 
 |-  ( ( F Fn ( 1 ... N ) /\ F = (/) ) -> ( 1 ... N ) = (/) )
4 3 ex 
 |-  ( F Fn ( 1 ... N ) -> ( F = (/) -> ( 1 ... N ) = (/) ) )
5 fneq2 
 |-  ( ( 1 ... N ) = (/) -> ( F Fn ( 1 ... N ) <-> F Fn (/) ) )
6 5 1 bitrdi 
 |-  ( ( 1 ... N ) = (/) -> ( F Fn ( 1 ... N ) <-> F = (/) ) )
7 6 biimpcd 
 |-  ( F Fn ( 1 ... N ) -> ( ( 1 ... N ) = (/) -> F = (/) ) )
8 4 7 impbid 
 |-  ( F Fn ( 1 ... N ) -> ( F = (/) <-> ( 1 ... N ) = (/) ) )
9 fz1n 
 |-  ( N e. NN0 -> ( ( 1 ... N ) = (/) <-> N = 0 ) )
10 8 9 sylan9bbr 
 |-  ( ( N e. NN0 /\ F Fn ( 1 ... N ) ) -> ( F = (/) <-> N = 0 ) )