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) (Revised by Mingli Yuan, 15-Aug-2026)

	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 \mathrm{Fun}{\left({F\upharpoonright }_{\left(1\dots K\right)}\right)}^{-1}$$
	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 \mathrm{Fun}{\left({F\upharpoonright }_{\left(1\dots K\right)}\right)}^{-1}$$
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	2 6	fssresd	$$⊢\phi \to \left({F\upharpoonright }_{\left(1\dots K\right)}\right):\left(1\dots K\right)⟶V$$
8		df-f1	$$⊢\left({F\upharpoonright }_{\left(1\dots K\right)}\right):\left(1\dots K\right)\underset{1-1}{⟶}V\leftrightarrow \left(\left({F\upharpoonright }_{\left(1\dots K\right)}\right):\left(1\dots K\right)⟶V\wedge \mathrm{Fun}{\left({F\upharpoonright }_{\left(1\dots K\right)}\right)}^{-1}\right)$$
9	8	a1i	$$⊢\phi \to \left(\left({F\upharpoonright }_{\left(1\dots K\right)}\right):\left(1\dots K\right)\underset{1-1}{⟶}V\leftrightarrow \left(\left({F\upharpoonright }_{\left(1\dots K\right)}\right):\left(1\dots K\right)⟶V\wedge \mathrm{Fun}{\left({F\upharpoonright }_{\left(1\dots K\right)}\right)}^{-1}\right)\right)$$
10	7 3 9	mpbir2and	$$⊢\phi \to \left({F\upharpoonright }_{\left(1\dots K\right)}\right):\left(1\dots K\right)\underset{1-1}{⟶}V$$
11		0elfz	$$⊢K\in {\mathbb{N}}_0\to 0\in \left(0\dots K\right)$$
12		snssi	$$⊢0\in \left(0\dots K\right)\to \left\{0\right\}\subseteq \left(0\dots K\right)$$
13	1 11 12	3syl	$$⊢\phi \to \left\{0\right\}\subseteq \left(0\dots K\right)$$
14	2 13	fssresd	$$⊢\phi \to \left({F\upharpoonright }_{\left\{0\right\}}\right):\left\{0\right\}⟶V$$
15		eqidd	$$⊢\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(0\right)=\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(0\right)\to 0=0$$
16		0nn0	$$⊢0\in {\mathbb{N}}_0$$
17		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)$$
18		eqeq1	$$⊢x=0\to \left(x=y\leftrightarrow 0=y\right)$$
19	17 18	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)$$
20		fveq2	$$⊢y=0\to \left({F\upharpoonright }_{\left\{0\right\}}\right)\left(y\right)=\left({F\upharpoonright }_{\left\{0\right\}}\right)\left(0\right)$$
21	20	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)$$
22		eqeq2	$$⊢y=0\to \left(0=y\leftrightarrow 0=0\right)$$
23	21 22	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)$$
24	19 23	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)$$
25	16 16 24	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)$$
26	15 25	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)$$
27		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)$$
28	14 26 27	sylanblrc	$$⊢\phi \to \left({F\upharpoonright }_{\left\{0\right\}}\right):\left\{0\right\}\underset{1-1}{⟶}V$$
29		uncom	$$⊢\left(1\dots K\right)\cup \left\{0\right\}=\left\{0\right\}\cup \left(1\dots K\right)$$
30		fz0sn0fz1	$$⊢K\in {\mathbb{N}}_0\to \left(0\dots K\right)=\left\{0\right\}\cup \left(1\dots K\right)$$
31	1 30	syl	$$⊢\phi \to \left(0\dots K\right)=\left\{0\right\}\cup \left(1\dots K\right)$$
32	29 31	eqtr4id	$$⊢\phi \to \left(1\dots K\right)\cup \left\{0\right\}=\left(0\dots K\right)$$
33		0nelfz1	$$⊢0\notin \left(1\dots K\right)$$
34	33	neli	$$⊢\neg 0\in \left(1\dots K\right)$$
35		disjsn	$$⊢\left(1\dots K\right)\cap \left\{0\right\}=\varnothing \leftrightarrow \neg 0\in \left(1\dots K\right)$$
36	34 35	mpbir	$$⊢\left(1\dots K\right)\cap \left\{0\right\}=\varnothing$$
37		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)$$
38	5 36 37	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\}$$
39	32 38	sylib	$$⊢\phi \to \left(0\dots K\right)\setminus \left(1\dots K\right)=\left\{0\right\}$$
40	39	eqcomd	$$⊢\phi \to \left\{0\right\}=\left(0\dots K\right)\setminus \left(1\dots K\right)$$
41	40	reseq2d	$$⊢\phi \to {F\upharpoonright }_{\left\{0\right\}}={F\upharpoonright }_{\left(\left(0\dots K\right)\setminus \left(1\dots K\right)\right)}$$
42		eqidd	$$⊢\phi \to V=V$$
43	41 40 42	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)$$
44	28 43	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$$
45	40	imaeq2d	$$⊢\phi \to F\left[\left\{0\right\}\right]=F\left[\left(0\dots K\right)\setminus \left(1\dots K\right)\right]$$
46	45	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]$$
47		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]$$
48	47 4	eqtr3id	$$⊢\phi \to F\left[\left(1\dots K\right)\right]\cap F\left[\left\{0\right\}\right]=\varnothing$$
49	46 48	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$$
50	6 2 10 44 49	f1resrcmplf1d	$$⊢\phi \to F:\left(0\dots K\right)\underset{1-1}{⟶}V$$