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

Theorem fvinim0ffz 9168
Description: The function values for the borders of a finite interval of integers, which is the domain of the function, are not in the image of the interior of the interval iff the intersection of the images of the interior and the borders is empty. (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 5-Feb-2021.)
Assertion
Ref Expression
fvinim0ffz ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ ↔ ((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹𝐾) ∉ (𝐹 “ (1..^𝐾)))))

Proof of Theorem fvinim0ffz
Dummy variable 𝑣 is distinct from all other variables.
StepHypRef Expression
1 ffn 5071 . . . . . 6 (𝐹:(0...𝐾)⟶𝑉𝐹 Fn (0...𝐾))
21adantr 265 . . . . 5 ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → 𝐹 Fn (0...𝐾))
3 0nn0 8224 . . . . . . 7 0 ∈ ℕ0
43a1i 9 . . . . . 6 ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → 0 ∈ ℕ0)
5 simpr 107 . . . . . 6 ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → 𝐾 ∈ ℕ0)
6 nn0ge0 8234 . . . . . . 7 (𝐾 ∈ ℕ0 → 0 ≤ 𝐾)
76adantl 266 . . . . . 6 ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → 0 ≤ 𝐾)
8 elfz2nn0 9045 . . . . . 6 (0 ∈ (0...𝐾) ↔ (0 ∈ ℕ0𝐾 ∈ ℕ0 ∧ 0 ≤ 𝐾))
94, 5, 7, 8syl3anbrc 1097 . . . . 5 ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → 0 ∈ (0...𝐾))
10 id 19 . . . . . . 7 (𝐾 ∈ ℕ0𝐾 ∈ ℕ0)
11 nn0re 8218 . . . . . . . 8 (𝐾 ∈ ℕ0𝐾 ∈ ℝ)
1211leidd 7550 . . . . . . 7 (𝐾 ∈ ℕ0𝐾𝐾)
13 elfz2nn0 9045 . . . . . . 7 (𝐾 ∈ (0...𝐾) ↔ (𝐾 ∈ ℕ0𝐾 ∈ ℕ0𝐾𝐾))
1410, 10, 12, 13syl3anbrc 1097 . . . . . 6 (𝐾 ∈ ℕ0𝐾 ∈ (0...𝐾))
1514adantl 266 . . . . 5 ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → 𝐾 ∈ (0...𝐾))
16 fnimapr 5258 . . . . 5 ((𝐹 Fn (0...𝐾) ∧ 0 ∈ (0...𝐾) ∧ 𝐾 ∈ (0...𝐾)) → (𝐹 “ {0, 𝐾}) = {(𝐹‘0), (𝐹𝐾)})
172, 9, 15, 16syl3anc 1144 . . . 4 ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (𝐹 “ {0, 𝐾}) = {(𝐹‘0), (𝐹𝐾)})
1817ineq1d 3162 . . 3 ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → ((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ({(𝐹‘0), (𝐹𝐾)} ∩ (𝐹 “ (1..^𝐾))))
1918eqeq1d 2062 . 2 ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ ↔ ({(𝐹‘0), (𝐹𝐾)} ∩ (𝐹 “ (1..^𝐾))) = ∅))
20 disj 3293 . . 3 (({(𝐹‘0), (𝐹𝐾)} ∩ (𝐹 “ (1..^𝐾))) = ∅ ↔ ∀𝑣 ∈ {(𝐹‘0), (𝐹𝐾)} ¬ 𝑣 ∈ (𝐹 “ (1..^𝐾)))
21 simpl 106 . . . . 5 ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → 𝐹:(0...𝐾)⟶𝑉)
2221, 9ffvelrnd 5328 . . . 4 ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (𝐹‘0) ∈ 𝑉)
2321, 15ffvelrnd 5328 . . . 4 ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (𝐹𝐾) ∈ 𝑉)
24 eleq1 2114 . . . . . . 7 (𝑣 = (𝐹‘0) → (𝑣 ∈ (𝐹 “ (1..^𝐾)) ↔ (𝐹‘0) ∈ (𝐹 “ (1..^𝐾))))
2524notbid 600 . . . . . 6 (𝑣 = (𝐹‘0) → (¬ 𝑣 ∈ (𝐹 “ (1..^𝐾)) ↔ ¬ (𝐹‘0) ∈ (𝐹 “ (1..^𝐾))))
26 df-nel 2313 . . . . . 6 ((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ↔ ¬ (𝐹‘0) ∈ (𝐹 “ (1..^𝐾)))
2725, 26syl6bbr 191 . . . . 5 (𝑣 = (𝐹‘0) → (¬ 𝑣 ∈ (𝐹 “ (1..^𝐾)) ↔ (𝐹‘0) ∉ (𝐹 “ (1..^𝐾))))
28 eleq1 2114 . . . . . . 7 (𝑣 = (𝐹𝐾) → (𝑣 ∈ (𝐹 “ (1..^𝐾)) ↔ (𝐹𝐾) ∈ (𝐹 “ (1..^𝐾))))
2928notbid 600 . . . . . 6 (𝑣 = (𝐹𝐾) → (¬ 𝑣 ∈ (𝐹 “ (1..^𝐾)) ↔ ¬ (𝐹𝐾) ∈ (𝐹 “ (1..^𝐾))))
30 df-nel 2313 . . . . . 6 ((𝐹𝐾) ∉ (𝐹 “ (1..^𝐾)) ↔ ¬ (𝐹𝐾) ∈ (𝐹 “ (1..^𝐾)))
3129, 30syl6bbr 191 . . . . 5 (𝑣 = (𝐹𝐾) → (¬ 𝑣 ∈ (𝐹 “ (1..^𝐾)) ↔ (𝐹𝐾) ∉ (𝐹 “ (1..^𝐾))))
3227, 31ralprg 3446 . . . 4 (((𝐹‘0) ∈ 𝑉 ∧ (𝐹𝐾) ∈ 𝑉) → (∀𝑣 ∈ {(𝐹‘0), (𝐹𝐾)} ¬ 𝑣 ∈ (𝐹 “ (1..^𝐾)) ↔ ((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹𝐾) ∉ (𝐹 “ (1..^𝐾)))))
3322, 23, 32syl2anc 397 . . 3 ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (∀𝑣 ∈ {(𝐹‘0), (𝐹𝐾)} ¬ 𝑣 ∈ (𝐹 “ (1..^𝐾)) ↔ ((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹𝐾) ∉ (𝐹 “ (1..^𝐾)))))
3420, 33syl5bb 185 . 2 ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (({(𝐹‘0), (𝐹𝐾)} ∩ (𝐹 “ (1..^𝐾))) = ∅ ↔ ((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹𝐾) ∉ (𝐹 “ (1..^𝐾)))))
3519, 34bitrd 181 1 ((𝐹:(0...𝐾)⟶𝑉𝐾 ∈ ℕ0) → (((𝐹 “ {0, 𝐾}) ∩ (𝐹 “ (1..^𝐾))) = ∅ ↔ ((𝐹‘0) ∉ (𝐹 “ (1..^𝐾)) ∧ (𝐹𝐾) ∉ (𝐹 “ (1..^𝐾)))))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 101  wb 102   = wceq 1257  wcel 1407  wnel 2312  wral 2321  cin 2941  c0 3249  {cpr 3401   class class class wbr 3789  cima 4373   Fn wfn 4922  wf 4923  cfv 4927  (class class class)co 5537  0cc0 6917  1c1 6918  cle 7090  0cn0 8209  ...cfz 8946  ..^cfzo 9071
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 552  ax-in2 553  ax-io 638  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-10 1410  ax-11 1411  ax-i12 1412  ax-bndl 1413  ax-4 1414  ax-13 1418  ax-14 1419  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036  ax-coll 3897  ax-sep 3900  ax-nul 3908  ax-pow 3952  ax-pr 3969  ax-un 4195  ax-setind 4287  ax-iinf 4336  ax-cnex 7003  ax-resscn 7004  ax-1cn 7005  ax-1re 7006  ax-icn 7007  ax-addcl 7008  ax-addrcl 7009  ax-mulcl 7010  ax-addcom 7012  ax-addass 7014  ax-distr 7016  ax-i2m1 7017  ax-0id 7020  ax-rnegex 7021  ax-cnre 7023  ax-pre-ltirr 7024  ax-pre-ltwlin 7025  ax-pre-lttrn 7026  ax-pre-ltadd 7028
This theorem depends on definitions:  df-bi 114  df-dc 752  df-3or 895  df-3an 896  df-tru 1260  df-fal 1263  df-nf 1364  df-sb 1660  df-eu 1917  df-mo 1918  df-clab 2041  df-cleq 2047  df-clel 2050  df-nfc 2181  df-ne 2219  df-nel 2313  df-ral 2326  df-rex 2327  df-reu 2328  df-rab 2330  df-v 2574  df-sbc 2785  df-csb 2878  df-dif 2945  df-un 2947  df-in 2949  df-ss 2956  df-nul 3250  df-pw 3386  df-sn 3406  df-pr 3407  df-op 3409  df-uni 3606  df-int 3641  df-iun 3684  df-br 3790  df-opab 3844  df-mpt 3845  df-tr 3880  df-eprel 4051  df-id 4055  df-po 4058  df-iso 4059  df-iord 4128  df-on 4130  df-suc 4133  df-iom 4339  df-xp 4376  df-rel 4377  df-cnv 4378  df-co 4379  df-dm 4380  df-rn 4381  df-res 4382  df-ima 4383  df-iota 4892  df-fun 4929  df-fn 4930  df-f 4931  df-f1 4932  df-fo 4933  df-f1o 4934  df-fv 4935  df-riota 5493  df-ov 5540  df-oprab 5541  df-mpt2 5542  df-1st 5792  df-2nd 5793  df-recs 5948  df-irdg 5985  df-1o 6029  df-2o 6030  df-oadd 6033  df-omul 6034  df-er 6134  df-ec 6136  df-qs 6140  df-ni 6430  df-pli 6431  df-mi 6432  df-lti 6433  df-plpq 6470  df-mpq 6471  df-enq 6473  df-nqqs 6474  df-plqqs 6475  df-mqqs 6476  df-1nqqs 6477  df-rq 6478  df-ltnqqs 6479  df-enq0 6550  df-nq0 6551  df-0nq0 6552  df-plq0 6553  df-mq0 6554  df-inp 6592  df-i1p 6593  df-iplp 6594  df-iltp 6596  df-enr 6839  df-nr 6840  df-ltr 6843  df-0r 6844  df-1r 6845  df-0 6924  df-1 6925  df-r 6927  df-lt 6930  df-pnf 7091  df-mnf 7092  df-xr 7093  df-ltxr 7094  df-le 7095  df-sub 7217  df-neg 7218  df-inn 7961  df-n0 8210  df-z 8273  df-uz 8540  df-fz 8947
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator