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	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑀 ) ⟶ 𝑋 ∧ 𝑃 : ( 0 ... 𝑁 ) ⟶ 𝑌 ) → ( 𝐹 = 𝑃 ↔ ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝐹 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑖 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ffn	⊢ ( 𝐹 : ( 0 ... 𝑀 ) ⟶ 𝑋 → 𝐹 Fn ( 0 ... 𝑀 ) )
2		ffn	⊢ ( 𝑃 : ( 0 ... 𝑁 ) ⟶ 𝑌 → 𝑃 Fn ( 0 ... 𝑁 ) )
3	1 2	anim12i	⊢ ( ( 𝐹 : ( 0 ... 𝑀 ) ⟶ 𝑋 ∧ 𝑃 : ( 0 ... 𝑁 ) ⟶ 𝑌 ) → ( 𝐹 Fn ( 0 ... 𝑀 ) ∧ 𝑃 Fn ( 0 ... 𝑁 ) ) )
4	3	3adant1	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑀 ) ⟶ 𝑋 ∧ 𝑃 : ( 0 ... 𝑁 ) ⟶ 𝑌 ) → ( 𝐹 Fn ( 0 ... 𝑀 ) ∧ 𝑃 Fn ( 0 ... 𝑁 ) ) )
5		eqfnfv2	⊢ ( ( 𝐹 Fn ( 0 ... 𝑀 ) ∧ 𝑃 Fn ( 0 ... 𝑁 ) ) → ( 𝐹 = 𝑃 ↔ ( ( 0 ... 𝑀 ) = ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝐹 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑖 ) ) ) )
6	4 5	syl	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑀 ) ⟶ 𝑋 ∧ 𝑃 : ( 0 ... 𝑁 ) ⟶ 𝑌 ) → ( 𝐹 = 𝑃 ↔ ( ( 0 ... 𝑀 ) = ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝐹 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑖 ) ) ) )
7		elnn0uz	⊢ ( 𝑀 ∈ ℕ0 ↔ 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
8		fzopth	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → ( ( 0 ... 𝑀 ) = ( 0 ... 𝑁 ) ↔ ( 0 = 0 ∧ 𝑀 = 𝑁 ) ) )
9	7 8	sylbi	⊢ ( 𝑀 ∈ ℕ0 → ( ( 0 ... 𝑀 ) = ( 0 ... 𝑁 ) ↔ ( 0 = 0 ∧ 𝑀 = 𝑁 ) ) )
10		simpr	⊢ ( ( 0 = 0 ∧ 𝑀 = 𝑁 ) → 𝑀 = 𝑁 )
11	9 10	syl6bi	⊢ ( 𝑀 ∈ ℕ0 → ( ( 0 ... 𝑀 ) = ( 0 ... 𝑁 ) → 𝑀 = 𝑁 ) )
12	11	anim1d	⊢ ( 𝑀 ∈ ℕ0 → ( ( ( 0 ... 𝑀 ) = ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝐹 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑖 ) ) → ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝐹 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑖 ) ) ) )
13		oveq2	⊢ ( 𝑀 = 𝑁 → ( 0 ... 𝑀 ) = ( 0 ... 𝑁 ) )
14	13	anim1i	⊢ ( ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝐹 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑖 ) ) → ( ( 0 ... 𝑀 ) = ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝐹 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑖 ) ) )
15	12 14	impbid1	⊢ ( 𝑀 ∈ ℕ0 → ( ( ( 0 ... 𝑀 ) = ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝐹 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑖 ) ) ↔ ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝐹 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑖 ) ) ) )
16	15	3ad2ant1	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑀 ) ⟶ 𝑋 ∧ 𝑃 : ( 0 ... 𝑁 ) ⟶ 𝑌 ) → ( ( ( 0 ... 𝑀 ) = ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝐹 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑖 ) ) ↔ ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝐹 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑖 ) ) ) )
17	6 16	bitrd	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑀 ) ⟶ 𝑋 ∧ 𝑃 : ( 0 ... 𝑁 ) ⟶ 𝑌 ) → ( 𝐹 = 𝑃 ↔ ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝐹 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑖 ) ) ) )