Theorem f1resfz0f1d

Description: If a function with a sequence of nonnegative integers (starting at 0) as its domain is one-to-one when 0 is removed, and if the range of that restriction does not contain the function's value at the removed integer, then the function is itself one-to-one. (Contributed by BTernaryTau, 4-Oct-2023)

	Ref	Expression
Hypotheses	f1resfz0f1d.1	$$⊢\phi \to K\in {\mathbb{N}}_0$$
	f1resfz0f1d.2	$$⊢\phi \to F:\left(0\dots K\right)⟶V$$
	f1resfz0f1d.3	$$⊢\phi \to \left({F\upharpoonright }_{\left(1\dots K\right)}\right):\left(1\dots K\right)\underset{1-1}{⟶}V$$
	f1resfz0f1d.4	$$⊢\phi \to F\left[\left\{0\right\}\right]\cap F\left[\left(1\dots K\right)\right]=\varnothing$$
Assertion	f1resfz0f1d	$$⊢\phi \to F:\left(0\dots K\right)\underset{1-1}{⟶}V$$

Proof

Step	Hyp	Ref	Expression
1		f1resfz0f1d.1	$$⊢\phi \to K\in {\mathbb{N}}_0$$
2		f1resfz0f1d.2	$$⊢\phi \to F:\left(0\dots K\right)⟶V$$
3		f1resfz0f1d.3	$$⊢\phi \to \left({F\upharpoonright }_{\left(1\dots K\right)}\right):\left(1\dots K\right)\underset{1-1}{⟶}V$$
4		f1resfz0f1d.4	$$⊢\phi \to F\left[\left\{0\right\}\right]\cap F\left[\left(1\dots K\right)\right]=\varnothing$$
5		fz1ssfz0	$$⊢\left(1\dots K\right)\subseteq \left(0\dots K\right)$$
6	5	a1i	$$⊢\phi \to \left(1\dots K\right)\subseteq \left(0\dots K\right)$$
7		0elfz	$$⊢K\in {\mathbb{N}}_0\to 0\in \left(0\dots K\right)$$
8		snssi	$$⊢0\in \left(0\dots K\right)\to \left\{0\right\}\subseteq \left(0\dots K\right)$$
9	1 7 8	3syl	$$⊢\phi \to \left\{0\right\}\subseteq \left(0\dots K\right)$$
10	2 9	fssresd	$$⊢\phi \to \left({F\upharpoonright }_{\left\{0\right\}}\right):\left\{0\right\}⟶V$$
11		eqidd	$$⊢\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(0\right)=\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(0\right)\to 0=0$$
12		0nn0	$$⊢0\in {\mathbb{N}}_0$$
13		fveqeq2	$$⊢x=0\to \left(\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(x\right)=\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(y\right)\leftrightarrow \left({F\upharpoonright }_{\left\{0\right\}}\right)\left(0\right)=\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(y\right)\right)$$
14		eqeq1	$$⊢x=0\to \left(x=y\leftrightarrow 0=y\right)$$
15	13 14	imbi12d	$$⊢x=0\to \left(\left(\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(x\right)=\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(y\right)\to x=y\right)\leftrightarrow \left(\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(0\right)=\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(y\right)\to 0=y\right)\right)$$
16		fveq2	$$⊢y=0\to \left({F\upharpoonright }_{\left\{0\right\}}\right)\left(y\right)=\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(0\right)$$
17	16	eqeq2d	$$⊢y=0\to \left(\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(0\right)=\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(y\right)\leftrightarrow \left({F\upharpoonright }_{\left\{0\right\}}\right)\left(0\right)=\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(0\right)\right)$$
18		eqeq2	$$⊢y=0\to \left(0=y\leftrightarrow 0=0\right)$$
19	17 18	imbi12d	$$⊢y=0\to \left(\left(\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(0\right)=\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(y\right)\to 0=y\right)\leftrightarrow \left(\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(0\right)=\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(0\right)\to 0=0\right)\right)$$
20	15 19	2ralsng	$$⊢\left(0\in {\mathbb{N}}_0\wedge 0\in {\mathbb{N}}_0\right)\to \left(\forall x\in \left\{0\right\}\forall y\in \left\{0\right\}\left(\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(x\right)=\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(y\right)\to x=y\right)\leftrightarrow \left(\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(0\right)=\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(0\right)\to 0=0\right)\right)$$
21	12 12 20	mp2an	$$⊢\forall x\in \left\{0\right\}\forall y\in \left\{0\right\}\left(\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(x\right)=\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(y\right)\to x=y\right)\leftrightarrow \left(\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(0\right)=\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(0\right)\to 0=0\right)$$
22	11 21	mpbir	$$⊢\forall x\in \left\{0\right\}\forall y\in \left\{0\right\}\left(\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(x\right)=\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(y\right)\to x=y\right)$$
23		dff13	$$⊢\left({F\upharpoonright }_{\left\{0\right\}}\right):\left\{0\right\}\underset{1-1}{⟶}V\leftrightarrow \left(\left({F\upharpoonright }_{\left\{0\right\}}\right):\left\{0\right\}⟶V\wedge \forall x\in \left\{0\right\}\forall y\in \left\{0\right\}\left(\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(x\right)=\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(y\right)\to x=y\right)\right)$$
24	10 22 23	sylanblrc	$$⊢\phi \to \left({F\upharpoonright }_{\left\{0\right\}}\right):\left\{0\right\}\underset{1-1}{⟶}V$$
25		uncom	$$⊢\left(1\dots K\right)\cup \left\{0\right\}=\left\{0\right\}\cup \left(1\dots K\right)$$
26		fz0sn0fz1	$$⊢K\in {\mathbb{N}}_0\to \left(0\dots K\right)=\left\{0\right\}\cup \left(1\dots K\right)$$
27	1 26	syl	$$⊢\phi \to \left(0\dots K\right)=\left\{0\right\}\cup \left(1\dots K\right)$$
28	25 27	eqtr4id	$$⊢\phi \to \left(1\dots K\right)\cup \left\{0\right\}=\left(0\dots K\right)$$
29		0nelfz1	$$⊢0\notin \left(1\dots K\right)$$
30	29	neli	$$⊢\neg 0\in \left(1\dots K\right)$$
31		disjsn	$$⊢\left(1\dots K\right)\cap \left\{0\right\}=\varnothing \leftrightarrow \neg 0\in \left(1\dots K\right)$$
32	30 31	mpbir	$$⊢\left(1\dots K\right)\cap \left\{0\right\}=\varnothing$$
33		uneqdifeq	$$⊢\left(\left(1\dots K\right)\subseteq \left(0\dots K\right)\wedge \left(1\dots K\right)\cap \left\{0\right\}=\varnothing \right)\to \left(\left(1\dots K\right)\cup \left\{0\right\}=\left(0\dots K\right)\leftrightarrow \left(0\dots K\right)\setminus \left(1\dots K\right)=\left\{0\right\}\right)$$
34	5 32 33	mp2an	$$⊢\left(1\dots K\right)\cup \left\{0\right\}=\left(0\dots K\right)\leftrightarrow \left(0\dots K\right)\setminus \left(1\dots K\right)=\left\{0\right\}$$
35	28 34	sylib	$$⊢\phi \to \left(0\dots K\right)\setminus \left(1\dots K\right)=\left\{0\right\}$$
36	35	eqcomd	$$⊢\phi \to \left\{0\right\}=\left(0\dots K\right)\setminus \left(1\dots K\right)$$
37	36	reseq2d	$$⊢\phi \to {F\upharpoonright }_{\left\{0\right\}}={F\upharpoonright }_{\left(\left(0\dots K\right)\setminus \left(1\dots K\right)\right)}$$
38		eqidd	$$⊢\phi \to V=V$$
39	37 36 38	f1eq123d	$$⊢\phi \to \left(\left({F\upharpoonright }_{\left\{0\right\}}\right):\left\{0\right\}\underset{1-1}{⟶}V\leftrightarrow \left({F\upharpoonright }_{\left(\left(0\dots K\right)\setminus \left(1\dots K\right)\right)}\right):\left(0\dots K\right)\setminus \left(1\dots K\right)\underset{1-1}{⟶}V\right)$$
40	24 39	mpbid	$$⊢\phi \to \left({F\upharpoonright }_{\left(\left(0\dots K\right)\setminus \left(1\dots K\right)\right)}\right):\left(0\dots K\right)\setminus \left(1\dots K\right)\underset{1-1}{⟶}V$$
41	36	imaeq2d	$$⊢\phi \to F\left[\left\{0\right\}\right]=F\left[\left(0\dots K\right)\setminus \left(1\dots K\right)\right]$$
42	41	ineq2d	$$⊢\phi \to F\left[\left(1\dots K\right)\right]\cap F\left[\left\{0\right\}\right]=F\left[\left(1\dots K\right)\right]\cap F\left[\left(0\dots K\right)\setminus \left(1\dots K\right)\right]$$
43		incom	$$⊢F\left[\left\{0\right\}\right]\cap F\left[\left(1\dots K\right)\right]=F\left[\left(1\dots K\right)\right]\cap F\left[\left\{0\right\}\right]$$
44	43 4	syl5eqr	$$⊢\phi \to F\left[\left(1\dots K\right)\right]\cap F\left[\left\{0\right\}\right]=\varnothing$$
45	42 44	eqtr3d	$$⊢\phi \to F\left[\left(1\dots K\right)\right]\cap F\left[\left(0\dots K\right)\setminus \left(1\dots K\right)\right]=\varnothing$$
46	6 2 3 40 45	f1resrcmplf1d	$$⊢\phi \to F:\left(0\dots K\right)\underset{1-1}{⟶}V$$