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

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 biimtrdi ⊢ ( 𝐹 = 𝑃 → ( ( 𝐹 = ∅ ∧ 𝑃 : ( 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 biimtrdi ⊢ ( ( 𝑀 = 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 biimtrdi ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ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 biimtrrid ⊢ ( ( 𝑀 ∈ ℕ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 ..^ 𝑀 ) ( 𝐹 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑖 ) ) ) )