Theorem f1resrcmplf1d

Description: If a function's restriction to a subclass of its domain and its restriction to the relative complement of that subclass are both one-to-one, and if the ranges of those two restrictions are disjoint, then the function is itself one-to-one. (Contributed by BTernaryTau, 28-Sep-2023)

	Ref	Expression
Hypotheses	f1resrcmplf1d.1	$$⊢\phi \to C\subseteq A$$
	f1resrcmplf1d.2	$$⊢\phi \to F:A⟶B$$
	f1resrcmplf1d.3	$$⊢\phi \to \left({F\upharpoonright }_C\right):C\underset{1-1}{⟶}B$$
	f1resrcmplf1d.4	$$⊢\phi \to \left({F\upharpoonright }_{\left(A\setminus C\right)}\right):A\setminus C\underset{1-1}{⟶}B$$
	f1resrcmplf1d.5	$$⊢\phi \to F\left[C\right]\cap F\left[A\setminus C\right]=\varnothing$$
Assertion	f1resrcmplf1d	$$⊢\phi \to F:A\underset{1-1}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		f1resrcmplf1d.1	$$⊢\phi \to C\subseteq A$$
2		f1resrcmplf1d.2	$$⊢\phi \to F:A⟶B$$
3		f1resrcmplf1d.3	$$⊢\phi \to \left({F\upharpoonright }_C\right):C\underset{1-1}{⟶}B$$
4		f1resrcmplf1d.4	$$⊢\phi \to \left({F\upharpoonright }_{\left(A\setminus C\right)}\right):A\setminus C\underset{1-1}{⟶}B$$
5		f1resrcmplf1d.5	$$⊢\phi \to F\left[C\right]\cap F\left[A\setminus C\right]=\varnothing$$
6		f1resveqaeq	$$⊢\left(\left({F\upharpoonright }_C\right):C\underset{1-1}{⟶}B\wedge \left(x\in C\wedge y\in C\right)\right)\to \left(F\left(x\right)=F\left(y\right)\to x=y\right)$$
7	3 6	sylan	$$⊢\left(\phi \wedge \left(x\in C\wedge y\in C\right)\right)\to \left(F\left(x\right)=F\left(y\right)\to x=y\right)$$
8	7	ex	$$⊢\phi \to \left(\left(x\in C\wedge y\in C\right)\to \left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)$$
9		difssd	$$⊢\phi \to A\setminus C\subseteq A$$
10	1 9 2 5	f1resrcmplf1dlem	$$⊢\phi \to \left(\left(x\in C\wedge y\in \left(A\setminus C\right)\right)\to \left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)$$
11		incom	$$⊢F\left[C\right]\cap F\left[A\setminus C\right]=F\left[A\setminus C\right]\cap F\left[C\right]$$
12	11 5	syl5eqr	$$⊢\phi \to F\left[A\setminus C\right]\cap F\left[C\right]=\varnothing$$
13	9 1 2 12	f1resrcmplf1dlem	$$⊢\phi \to \left(\left(x\in \left(A\setminus C\right)\wedge y\in C\right)\to \left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)$$
14		f1resveqaeq	$$⊢\left(\left({F\upharpoonright }_{\left(A\setminus C\right)}\right):A\setminus C\underset{1-1}{⟶}B\wedge \left(x\in \left(A\setminus C\right)\wedge y\in \left(A\setminus C\right)\right)\right)\to \left(F\left(x\right)=F\left(y\right)\to x=y\right)$$
15	4 14	sylan	$$⊢\left(\phi \wedge \left(x\in \left(A\setminus C\right)\wedge y\in \left(A\setminus C\right)\right)\right)\to \left(F\left(x\right)=F\left(y\right)\to x=y\right)$$
16	15	ex	$$⊢\phi \to \left(\left(x\in \left(A\setminus C\right)\wedge y\in \left(A\setminus C\right)\right)\to \left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)$$
17	8 10 13 16	prsrcmpltd	$$⊢\phi \to \left(\left(x\in A\wedge y\in A\right)\to \left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)$$
18	17	ralrimivv	$$⊢\phi \to \forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)$$
19		dff13	$$⊢F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)$$
20	2 18 19	sylanbrc	$$⊢\phi \to F:A\underset{1-1}{⟶}B$$