Metamath Proof Explorer

Theorem 2ffzeq

Description: Two functions over 0-based finite set of sequential integers are equal if and only if their domains have the same length and the function values are the same at each position. (Contributed by Alexander van der Vekens, 30-Jun-2018)

Ref Expression
Assertion 2ffzeq 
|- ( ( M e. NN0 /\ F : ( 0 ... M ) --> X /\ P : ( 0 ... N ) --> Y ) -> ( F = P <-> ( M = N /\ A. i e. ( 0 ... M ) ( F ` i ) = ( P ` i ) ) ) )

Proof

Step Hyp Ref Expression
1 ffn 
 |-  ( F : ( 0 ... M ) --> X -> F Fn ( 0 ... M ) )
2 ffn 
 |-  ( P : ( 0 ... N ) --> Y -> P Fn ( 0 ... N ) )
3 1 2 anim12i 
 |-  ( ( F : ( 0 ... M ) --> X /\ P : ( 0 ... N ) --> Y ) -> ( F Fn ( 0 ... M ) /\ P Fn ( 0 ... N ) ) )
4 3 3adant1 
 |-  ( ( M e. NN0 /\ F : ( 0 ... M ) --> X /\ P : ( 0 ... N ) --> Y ) -> ( F Fn ( 0 ... M ) /\ P Fn ( 0 ... N ) ) )
5 eqfnfv2 
 |-  ( ( F Fn ( 0 ... M ) /\ P Fn ( 0 ... N ) ) -> ( F = P <-> ( ( 0 ... M ) = ( 0 ... N ) /\ A. i e. ( 0 ... M ) ( F ` i ) = ( P ` i ) ) ) )
6 4 5 syl 
 |-  ( ( M e. NN0 /\ F : ( 0 ... M ) --> X /\ P : ( 0 ... N ) --> Y ) -> ( F = P <-> ( ( 0 ... M ) = ( 0 ... N ) /\ A. i e. ( 0 ... M ) ( F ` i ) = ( P ` i ) ) ) )
7 elnn0uz 
 |-  ( M e. NN0 <-> M e. ( ZZ>= ` 0 ) )
8 fzopth 
 |-  ( M e. ( ZZ>= ` 0 ) -> ( ( 0 ... M ) = ( 0 ... N ) <-> ( 0 = 0 /\ M = N ) ) )
9 7 8 sylbi 
 |-  ( M e. NN0 -> ( ( 0 ... M ) = ( 0 ... N ) <-> ( 0 = 0 /\ M = N ) ) )
10 simpr 
 |-  ( ( 0 = 0 /\ M = N ) -> M = N )
11 9 10 syl6bi 
 |-  ( M e. NN0 -> ( ( 0 ... M ) = ( 0 ... N ) -> M = N ) )
12 11 anim1d 
 |-  ( M e. NN0 -> ( ( ( 0 ... M ) = ( 0 ... N ) /\ A. i e. ( 0 ... M ) ( F ` i ) = ( P ` i ) ) -> ( M = N /\ A. i e. ( 0 ... M ) ( F ` i ) = ( P ` i ) ) ) )
13 oveq2 
 |-  ( M = N -> ( 0 ... M ) = ( 0 ... N ) )
14 13 anim1i 
 |-  ( ( M = N /\ A. i e. ( 0 ... M ) ( F ` i ) = ( P ` i ) ) -> ( ( 0 ... M ) = ( 0 ... N ) /\ A. i e. ( 0 ... M ) ( F ` i ) = ( P ` i ) ) )
15 12 14 impbid1 
 |-  ( M e. NN0 -> ( ( ( 0 ... M ) = ( 0 ... N ) /\ A. i e. ( 0 ... M ) ( F ` i ) = ( P ` i ) ) <-> ( M = N /\ A. i e. ( 0 ... M ) ( F ` i ) = ( P ` i ) ) ) )
16 15 3ad2ant1 
 |-  ( ( M e. NN0 /\ F : ( 0 ... M ) --> X /\ P : ( 0 ... N ) --> Y ) -> ( ( ( 0 ... M ) = ( 0 ... N ) /\ A. i e. ( 0 ... M ) ( F ` i ) = ( P ` i ) ) <-> ( M = N /\ A. i e. ( 0 ... M ) ( F ` i ) = ( P ` i ) ) ) )
17 6 16 bitrd 
 |-  ( ( M e. NN0 /\ F : ( 0 ... M ) --> X /\ P : ( 0 ... N ) --> Y ) -> ( F = P <-> ( M = N /\ A. i e. ( 0 ... M ) ( F ` i ) = ( P ` i ) ) ) )