ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  2ffzeq GIF version

Theorem 2ffzeq 9305
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.)
Assertion
Ref Expression
2ffzeq ((𝑀 ∈ ℕ0𝐹:(0...𝑀)⟶𝑋𝑃:(0...𝑁)⟶𝑌) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0...𝑀)(𝐹𝑖) = (𝑃𝑖))))
Distinct variable groups:   𝑖,𝐹   𝑖,𝑀   𝑃,𝑖
Allowed substitution hints:   𝑁(𝑖)   𝑋(𝑖)   𝑌(𝑖)

Proof of Theorem 2ffzeq
StepHypRef Expression
1 ffn 5098 . . . . 5 (𝐹:(0...𝑀)⟶𝑋𝐹 Fn (0...𝑀))
2 ffn 5098 . . . . 5 (𝑃:(0...𝑁)⟶𝑌𝑃 Fn (0...𝑁))
31, 2anim12i 331 . . . 4 ((𝐹:(0...𝑀)⟶𝑋𝑃:(0...𝑁)⟶𝑌) → (𝐹 Fn (0...𝑀) ∧ 𝑃 Fn (0...𝑁)))
433adant1 957 . . 3 ((𝑀 ∈ ℕ0𝐹:(0...𝑀)⟶𝑋𝑃:(0...𝑁)⟶𝑌) → (𝐹 Fn (0...𝑀) ∧ 𝑃 Fn (0...𝑁)))
5 eqfnfv2 5320 . . 3 ((𝐹 Fn (0...𝑀) ∧ 𝑃 Fn (0...𝑁)) → (𝐹 = 𝑃 ↔ ((0...𝑀) = (0...𝑁) ∧ ∀𝑖 ∈ (0...𝑀)(𝐹𝑖) = (𝑃𝑖))))
64, 5syl 14 . 2 ((𝑀 ∈ ℕ0𝐹:(0...𝑀)⟶𝑋𝑃:(0...𝑁)⟶𝑌) → (𝐹 = 𝑃 ↔ ((0...𝑀) = (0...𝑁) ∧ ∀𝑖 ∈ (0...𝑀)(𝐹𝑖) = (𝑃𝑖))))
7 elnn0uz 8814 . . . . . . 7 (𝑀 ∈ ℕ0𝑀 ∈ (ℤ‘0))
8 fzopth 9232 . . . . . . 7 (𝑀 ∈ (ℤ‘0) → ((0...𝑀) = (0...𝑁) ↔ (0 = 0 ∧ 𝑀 = 𝑁)))
97, 8sylbi 119 . . . . . 6 (𝑀 ∈ ℕ0 → ((0...𝑀) = (0...𝑁) ↔ (0 = 0 ∧ 𝑀 = 𝑁)))
10 simpr 108 . . . . . 6 ((0 = 0 ∧ 𝑀 = 𝑁) → 𝑀 = 𝑁)
119, 10syl6bi 161 . . . . 5 (𝑀 ∈ ℕ0 → ((0...𝑀) = (0...𝑁) → 𝑀 = 𝑁))
1211anim1d 329 . . . 4 (𝑀 ∈ ℕ0 → (((0...𝑀) = (0...𝑁) ∧ ∀𝑖 ∈ (0...𝑀)(𝐹𝑖) = (𝑃𝑖)) → (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0...𝑀)(𝐹𝑖) = (𝑃𝑖))))
13 oveq2 5573 . . . . 5 (𝑀 = 𝑁 → (0...𝑀) = (0...𝑁))
1413anim1i 333 . . . 4 ((𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0...𝑀)(𝐹𝑖) = (𝑃𝑖)) → ((0...𝑀) = (0...𝑁) ∧ ∀𝑖 ∈ (0...𝑀)(𝐹𝑖) = (𝑃𝑖)))
1512, 14impbid1 140 . . 3 (𝑀 ∈ ℕ0 → (((0...𝑀) = (0...𝑁) ∧ ∀𝑖 ∈ (0...𝑀)(𝐹𝑖) = (𝑃𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0...𝑀)(𝐹𝑖) = (𝑃𝑖))))
16153ad2ant1 960 . 2 ((𝑀 ∈ ℕ0𝐹:(0...𝑀)⟶𝑋𝑃:(0...𝑁)⟶𝑌) → (((0...𝑀) = (0...𝑁) ∧ ∀𝑖 ∈ (0...𝑀)(𝐹𝑖) = (𝑃𝑖)) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0...𝑀)(𝐹𝑖) = (𝑃𝑖))))
176, 16bitrd 186 1 ((𝑀 ∈ ℕ0𝐹:(0...𝑀)⟶𝑋𝑃:(0...𝑁)⟶𝑌) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0...𝑀)(𝐹𝑖) = (𝑃𝑖))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  w3a 920   = wceq 1285  wcel 1434  wral 2353   Fn wfn 4948  wf 4949  cfv 4953  (class class class)co 5565  0cc0 7120  0cn0 8432  cuz 8777  ...cfz 9182
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3917  ax-pow 3969  ax-pr 3993  ax-un 4217  ax-setind 4309  ax-cnex 7206  ax-resscn 7207  ax-1cn 7208  ax-1re 7209  ax-icn 7210  ax-addcl 7211  ax-addrcl 7212  ax-mulcl 7213  ax-addcom 7215  ax-addass 7217  ax-distr 7219  ax-i2m1 7220  ax-0lt1 7221  ax-0id 7223  ax-rnegex 7224  ax-cnre 7226  ax-pre-ltirr 7227  ax-pre-ltwlin 7228  ax-pre-lttrn 7229  ax-pre-apti 7230  ax-pre-ltadd 7231
This theorem depends on definitions:  df-bi 115  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-nel 2345  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2362  df-v 2613  df-sbc 2826  df-csb 2919  df-dif 2985  df-un 2987  df-in 2989  df-ss 2996  df-pw 3403  df-sn 3423  df-pr 3424  df-op 3426  df-uni 3623  df-int 3658  df-br 3807  df-opab 3861  df-mpt 3862  df-id 4077  df-xp 4398  df-rel 4399  df-cnv 4400  df-co 4401  df-dm 4402  df-rn 4403  df-res 4404  df-ima 4405  df-iota 4918  df-fun 4955  df-fn 4956  df-f 4957  df-fv 4961  df-riota 5521  df-ov 5568  df-oprab 5569  df-mpt2 5570  df-pnf 7294  df-mnf 7295  df-xr 7296  df-ltxr 7297  df-le 7298  df-sub 7425  df-neg 7426  df-inn 8184  df-n0 8433  df-z 8510  df-uz 8778  df-fz 9183
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator