Theorem fvinim0ffz

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)

	Ref	Expression
Assertion	fvinim0ffz	$$⊢\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \leftrightarrow \left(F\left(0\right)\notin F\left[\left(1..^K\right)\right]\wedge F\left(K\right)\notin F\left[\left(1..^K\right)\right]\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ffn	$$⊢F:\left(0\dots K\right)⟶V\to FFn\left(0\dots K\right)$$
2	1	adantr	$$⊢\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to FFn\left(0\dots K\right)$$
3		0nn0	$$⊢0\in {\mathbb{N}}_0$$
4	3	a1i	$$⊢\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to 0\in {\mathbb{N}}_0$$
5		simpr	$$⊢\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to K\in {\mathbb{N}}_0$$
6		nn0ge0	$$⊢K\in {\mathbb{N}}_0\to 0\le K$$
7	6	adantl	$$⊢\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to 0\le K$$
8		elfz2nn0	$$⊢0\in \left(0\dots K\right)\leftrightarrow \left(0\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\wedge 0\le K\right)$$
9	4 5 7 8	syl3anbrc	$$⊢\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to 0\in \left(0\dots K\right)$$
10		id	$$⊢K\in {\mathbb{N}}_0\to K\in {\mathbb{N}}_0$$
11		nn0re	$$⊢K\in {\mathbb{N}}_0\to K\in ℝ$$
12	11	leidd	$$⊢K\in {\mathbb{N}}_0\to K\le K$$
13		elfz2nn0	$$⊢K\in \left(0\dots K\right)\leftrightarrow \left(K\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\wedge K\le K\right)$$
14	10 10 12 13	syl3anbrc	$$⊢K\in {\mathbb{N}}_0\to K\in \left(0\dots K\right)$$
15	14	adantl	$$⊢\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to K\in \left(0\dots K\right)$$
16		fnimapr	$$⊢\left(FFn\left(0\dots K\right)\wedge 0\in \left(0\dots K\right)\wedge K\in \left(0\dots K\right)\right)\to F\left[\left\{0,K\right\}\right]=\left\{F\left(0\right),F\left(K\right)\right\}$$
17	2 9 15 16	syl3anc	$$⊢\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to F\left[\left\{0,K\right\}\right]=\left\{F\left(0\right),F\left(K\right)\right\}$$
18	17	ineq1d	$$⊢\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\left\{F\left(0\right),F\left(K\right)\right\}\cap F\left[\left(1..^K\right)\right]$$
19	18	eqeq1d	$$⊢\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \leftrightarrow \left\{F\left(0\right),F\left(K\right)\right\}\cap F\left[\left(1..^K\right)\right]=\varnothing \right)$$
20		disj	$$⊢\left\{F\left(0\right),F\left(K\right)\right\}\cap F\left[\left(1..^K\right)\right]=\varnothing \leftrightarrow \forall v\in \left\{F\left(0\right),F\left(K\right)\right\}\neg v\in F\left[\left(1..^K\right)\right]$$
21		fvex	$$⊢F\left(0\right)\in \mathrm{V}$$
22		fvex	$$⊢F\left(K\right)\in \mathrm{V}$$
23		eleq1	$$⊢v=F\left(0\right)\to \left(v\in F\left[\left(1..^K\right)\right]\leftrightarrow F\left(0\right)\in F\left[\left(1..^K\right)\right]\right)$$
24	23	notbid	$$⊢v=F\left(0\right)\to \left(\neg v\in F\left[\left(1..^K\right)\right]\leftrightarrow \neg F\left(0\right)\in F\left[\left(1..^K\right)\right]\right)$$
25		df-nel	$$⊢F\left(0\right)\notin F\left[\left(1..^K\right)\right]\leftrightarrow \neg F\left(0\right)\in F\left[\left(1..^K\right)\right]$$
26	24 25	bitr4di	$$⊢v=F\left(0\right)\to \left(\neg v\in F\left[\left(1..^K\right)\right]\leftrightarrow F\left(0\right)\notin F\left[\left(1..^K\right)\right]\right)$$
27		eleq1	$$⊢v=F\left(K\right)\to \left(v\in F\left[\left(1..^K\right)\right]\leftrightarrow F\left(K\right)\in F\left[\left(1..^K\right)\right]\right)$$
28	27	notbid	$$⊢v=F\left(K\right)\to \left(\neg v\in F\left[\left(1..^K\right)\right]\leftrightarrow \neg F\left(K\right)\in F\left[\left(1..^K\right)\right]\right)$$
29		df-nel	$$⊢F\left(K\right)\notin F\left[\left(1..^K\right)\right]\leftrightarrow \neg F\left(K\right)\in F\left[\left(1..^K\right)\right]$$
30	28 29	bitr4di	$$⊢v=F\left(K\right)\to \left(\neg v\in F\left[\left(1..^K\right)\right]\leftrightarrow F\left(K\right)\notin F\left[\left(1..^K\right)\right]\right)$$
31	21 22 26 30	ralpr	$$⊢\forall v\in \left\{F\left(0\right),F\left(K\right)\right\}\neg v\in F\left[\left(1..^K\right)\right]\leftrightarrow \left(F\left(0\right)\notin F\left[\left(1..^K\right)\right]\wedge F\left(K\right)\notin F\left[\left(1..^K\right)\right]\right)$$
32	20 31	bitri	$$⊢\left\{F\left(0\right),F\left(K\right)\right\}\cap F\left[\left(1..^K\right)\right]=\varnothing \leftrightarrow \left(F\left(0\right)\notin F\left[\left(1..^K\right)\right]\wedge F\left(K\right)\notin F\left[\left(1..^K\right)\right]\right)$$
33	19 32	bitrdi	$$⊢\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \leftrightarrow \left(F\left(0\right)\notin F\left[\left(1..^K\right)\right]\wedge F\left(K\right)\notin F\left[\left(1..^K\right)\right]\right)\right)$$