Metamath Proof Explorer


Theorem 2ffzoeq

Description: Two functions over a half-open range of nonnegative 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, 1-Jul-2018)

Ref Expression
Assertion 2ffzoeq ( ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) ) → ( 𝐹 = 𝑃 ↔ ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ) )

Proof

Step Hyp Ref Expression
1 eqeq1 ( 𝐹 = 𝑃 → ( 𝐹 = ∅ ↔ 𝑃 = ∅ ) )
2 1 anbi1d ( 𝐹 = 𝑃 → ( ( 𝐹 = ∅ ∧ 𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) ↔ ( 𝑃 = ∅ ∧ 𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) ) )
3 f0bi ( 𝑃 : ∅ ⟶ 𝑌𝑃 = ∅ )
4 ffn ( 𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌𝑃 Fn ( 0 ..^ 𝑁 ) )
5 ffn ( 𝑃 : ∅ ⟶ 𝑌𝑃 Fn ∅ )
6 fndmu ( ( 𝑃 Fn ( 0 ..^ 𝑁 ) ∧ 𝑃 Fn ∅ ) → ( 0 ..^ 𝑁 ) = ∅ )
7 0z 0 ∈ ℤ
8 nn0z ( 𝑁 ∈ ℕ0𝑁 ∈ ℤ )
9 8 adantl ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
10 fzon ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ≤ 0 ↔ ( 0 ..^ 𝑁 ) = ∅ ) )
11 7 9 10 sylancr ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝑁 ≤ 0 ↔ ( 0 ..^ 𝑁 ) = ∅ ) )
12 nn0ge0 ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
13 0red ( 𝑁 ∈ ℕ0 → 0 ∈ ℝ )
14 nn0re ( 𝑁 ∈ ℕ0𝑁 ∈ ℝ )
15 13 14 letri3d ( 𝑁 ∈ ℕ0 → ( 0 = 𝑁 ↔ ( 0 ≤ 𝑁𝑁 ≤ 0 ) ) )
16 15 biimprd ( 𝑁 ∈ ℕ0 → ( ( 0 ≤ 𝑁𝑁 ≤ 0 ) → 0 = 𝑁 ) )
17 12 16 mpand ( 𝑁 ∈ ℕ0 → ( 𝑁 ≤ 0 → 0 = 𝑁 ) )
18 17 adantl ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝑁 ≤ 0 → 0 = 𝑁 ) )
19 11 18 sylbird ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( ( 0 ..^ 𝑁 ) = ∅ → 0 = 𝑁 ) )
20 6 19 syl5com ( ( 𝑃 Fn ( 0 ..^ 𝑁 ) ∧ 𝑃 Fn ∅ ) → ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → 0 = 𝑁 ) )
21 20 ex ( 𝑃 Fn ( 0 ..^ 𝑁 ) → ( 𝑃 Fn ∅ → ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → 0 = 𝑁 ) ) )
22 4 5 21 syl2imc ( 𝑃 : ∅ ⟶ 𝑌 → ( 𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 → ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → 0 = 𝑁 ) ) )
23 3 22 sylbir ( 𝑃 = ∅ → ( 𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 → ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → 0 = 𝑁 ) ) )
24 23 imp ( ( 𝑃 = ∅ ∧ 𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) → ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → 0 = 𝑁 ) )
25 2 24 syl6bi ( 𝐹 = 𝑃 → ( ( 𝐹 = ∅ ∧ 𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) → ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → 0 = 𝑁 ) ) )
26 25 com3l ( ( 𝐹 = ∅ ∧ 𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) → ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝐹 = 𝑃 → 0 = 𝑁 ) ) )
27 26 a1i ( 𝑀 = 0 → ( ( 𝐹 = ∅ ∧ 𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) → ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝐹 = 𝑃 → 0 = 𝑁 ) ) ) )
28 oveq2 ( 𝑀 = 0 → ( 0 ..^ 𝑀 ) = ( 0 ..^ 0 ) )
29 fzo0 ( 0 ..^ 0 ) = ∅
30 28 29 eqtrdi ( 𝑀 = 0 → ( 0 ..^ 𝑀 ) = ∅ )
31 30 feq2d ( 𝑀 = 0 → ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝐹 : ∅ ⟶ 𝑋 ) )
32 f0bi ( 𝐹 : ∅ ⟶ 𝑋𝐹 = ∅ )
33 31 32 bitrdi ( 𝑀 = 0 → ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝐹 = ∅ ) )
34 33 anbi1d ( 𝑀 = 0 → ( ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) ↔ ( 𝐹 = ∅ ∧ 𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) ) )
35 eqeq1 ( 𝑀 = 0 → ( 𝑀 = 𝑁 ↔ 0 = 𝑁 ) )
36 35 imbi2d ( 𝑀 = 0 → ( ( 𝐹 = 𝑃𝑀 = 𝑁 ) ↔ ( 𝐹 = 𝑃 → 0 = 𝑁 ) ) )
37 36 imbi2d ( 𝑀 = 0 → ( ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝐹 = 𝑃𝑀 = 𝑁 ) ) ↔ ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝐹 = 𝑃 → 0 = 𝑁 ) ) ) )
38 27 34 37 3imtr4d ( 𝑀 = 0 → ( ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) → ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝐹 = 𝑃𝑀 = 𝑁 ) ) ) )
39 38 com3l ( ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) → ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝑀 = 0 → ( 𝐹 = 𝑃𝑀 = 𝑁 ) ) ) )
40 39 impcom ( ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) ) → ( 𝑀 = 0 → ( 𝐹 = 𝑃𝑀 = 𝑁 ) ) )
41 40 impcom ( ( 𝑀 = 0 ∧ ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) ) ) → ( 𝐹 = 𝑃𝑀 = 𝑁 ) )
42 28 feq2d ( 𝑀 = 0 → ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝐹 : ( 0 ..^ 0 ) ⟶ 𝑋 ) )
43 29 feq2i ( 𝐹 : ( 0 ..^ 0 ) ⟶ 𝑋𝐹 : ∅ ⟶ 𝑋 )
44 43 32 bitri ( 𝐹 : ( 0 ..^ 0 ) ⟶ 𝑋𝐹 = ∅ )
45 42 44 bitrdi ( 𝑀 = 0 → ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝐹 = ∅ ) )
46 45 adantr ( ( 𝑀 = 0 ∧ 𝑀 = 𝑁 ) → ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝐹 = ∅ ) )
47 eqeq1 ( 𝑀 = 𝑁 → ( 𝑀 = 0 ↔ 𝑁 = 0 ) )
48 47 biimpac ( ( 𝑀 = 0 ∧ 𝑀 = 𝑁 ) → 𝑁 = 0 )
49 oveq2 ( 𝑁 = 0 → ( 0 ..^ 𝑁 ) = ( 0 ..^ 0 ) )
50 49 feq2d ( 𝑁 = 0 → ( 𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌𝑃 : ( 0 ..^ 0 ) ⟶ 𝑌 ) )
51 29 feq2i ( 𝑃 : ( 0 ..^ 0 ) ⟶ 𝑌𝑃 : ∅ ⟶ 𝑌 )
52 51 3 bitri ( 𝑃 : ( 0 ..^ 0 ) ⟶ 𝑌𝑃 = ∅ )
53 50 52 bitrdi ( 𝑁 = 0 → ( 𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌𝑃 = ∅ ) )
54 48 53 syl ( ( 𝑀 = 0 ∧ 𝑀 = 𝑁 ) → ( 𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌𝑃 = ∅ ) )
55 46 54 anbi12d ( ( 𝑀 = 0 ∧ 𝑀 = 𝑁 ) → ( ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) ↔ ( 𝐹 = ∅ ∧ 𝑃 = ∅ ) ) )
56 eqtr3 ( ( 𝐹 = ∅ ∧ 𝑃 = ∅ ) → 𝐹 = 𝑃 )
57 55 56 syl6bi ( ( 𝑀 = 0 ∧ 𝑀 = 𝑁 ) → ( ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) → 𝐹 = 𝑃 ) )
58 57 com12 ( ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) → ( ( 𝑀 = 0 ∧ 𝑀 = 𝑁 ) → 𝐹 = 𝑃 ) )
59 58 expd ( ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) → ( 𝑀 = 0 → ( 𝑀 = 𝑁𝐹 = 𝑃 ) ) )
60 59 adantl ( ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) ) → ( 𝑀 = 0 → ( 𝑀 = 𝑁𝐹 = 𝑃 ) ) )
61 60 impcom ( ( 𝑀 = 0 ∧ ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) ) ) → ( 𝑀 = 𝑁𝐹 = 𝑃 ) )
62 41 61 impbid ( ( 𝑀 = 0 ∧ ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) ) ) → ( 𝐹 = 𝑃𝑀 = 𝑁 ) )
63 ral0 𝑖 ∈ ∅ ( 𝐹𝑖 ) = ( 𝑃𝑖 )
64 30 raleqdv ( 𝑀 = 0 → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ↔ ∀ 𝑖 ∈ ∅ ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) )
65 63 64 mpbiri ( 𝑀 = 0 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) )
66 65 biantrud ( 𝑀 = 0 → ( 𝑀 = 𝑁 ↔ ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ) )
67 66 adantr ( ( 𝑀 = 0 ∧ ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) ) ) → ( 𝑀 = 𝑁 ↔ ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ) )
68 62 67 bitrd ( ( 𝑀 = 0 ∧ ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) ) ) → ( 𝐹 = 𝑃 ↔ ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ) )
69 ffn ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝐹 Fn ( 0 ..^ 𝑀 ) )
70 69 4 anim12i ( ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) → ( 𝐹 Fn ( 0 ..^ 𝑀 ) ∧ 𝑃 Fn ( 0 ..^ 𝑁 ) ) )
71 70 adantl ( ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) ) → ( 𝐹 Fn ( 0 ..^ 𝑀 ) ∧ 𝑃 Fn ( 0 ..^ 𝑁 ) ) )
72 71 adantl ( ( ¬ 𝑀 = 0 ∧ ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) ) ) → ( 𝐹 Fn ( 0 ..^ 𝑀 ) ∧ 𝑃 Fn ( 0 ..^ 𝑁 ) ) )
73 eqfnfv2 ( ( 𝐹 Fn ( 0 ..^ 𝑀 ) ∧ 𝑃 Fn ( 0 ..^ 𝑁 ) ) → ( 𝐹 = 𝑃 ↔ ( ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ) )
74 72 73 syl ( ( ¬ 𝑀 = 0 ∧ ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) ) ) → ( 𝐹 = 𝑃 ↔ ( ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ) )
75 df-ne ( 𝑀 ≠ 0 ↔ ¬ 𝑀 = 0 )
76 elnnne0 ( 𝑀 ∈ ℕ ↔ ( 𝑀 ∈ ℕ0𝑀 ≠ 0 ) )
77 0zd ( 𝑀 ∈ ℕ → 0 ∈ ℤ )
78 nnz ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
79 nngt0 ( 𝑀 ∈ ℕ → 0 < 𝑀 )
80 77 78 79 3jca ( 𝑀 ∈ ℕ → ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀 ) )
81 80 adantr ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀 ) )
82 fzoopth ( ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀 ) → ( ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) ↔ ( 0 = 0 ∧ 𝑀 = 𝑁 ) ) )
83 81 82 syl ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) ↔ ( 0 = 0 ∧ 𝑀 = 𝑁 ) ) )
84 simpr ( ( 0 = 0 ∧ 𝑀 = 𝑁 ) → 𝑀 = 𝑁 )
85 83 84 syl6bi ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) → 𝑀 = 𝑁 ) )
86 85 anim1d ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) → ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ) )
87 oveq2 ( 𝑀 = 𝑁 → ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) )
88 87 anim1i ( ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) → ( ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) )
89 86 88 impbid1 ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ↔ ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ) )
90 89 ex ( 𝑀 ∈ ℕ → ( 𝑁 ∈ ℕ0 → ( ( ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ↔ ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ) ) )
91 76 90 sylbir ( ( 𝑀 ∈ ℕ0𝑀 ≠ 0 ) → ( 𝑁 ∈ ℕ0 → ( ( ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ↔ ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ) ) )
92 91 impancom ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝑀 ≠ 0 → ( ( ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ↔ ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ) ) )
93 75 92 syl5bir ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( ¬ 𝑀 = 0 → ( ( ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ↔ ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ) ) )
94 93 adantr ( ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) ) → ( ¬ 𝑀 = 0 → ( ( ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ↔ ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ) ) )
95 94 impcom ( ( ¬ 𝑀 = 0 ∧ ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) ) ) → ( ( ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ↔ ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ) )
96 74 95 bitrd ( ( ¬ 𝑀 = 0 ∧ ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) ) ) → ( 𝐹 = 𝑃 ↔ ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ) )
97 68 96 pm2.61ian ( ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) ∧ ( 𝐹 : ( 0 ..^ 𝑀 ) ⟶ 𝑋𝑃 : ( 0 ..^ 𝑁 ) ⟶ 𝑌 ) ) → ( 𝐹 = 𝑃 ↔ ( 𝑀 = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝐹𝑖 ) = ( 𝑃𝑖 ) ) ) )