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	|- ( ph -> C C_ A )
	f1resrcmplf1d.2	|- ( ph -> F : A --> B )
	f1resrcmplf1d.3	|- ( ph -> ( F |` C ) : C -1-1-> B )
	f1resrcmplf1d.4	|- ( ph -> ( F |` ( A \ C ) ) : ( A \ C ) -1-1-> B )
	f1resrcmplf1d.5	|- ( ph -> ( ( F " C ) i^i ( F " ( A \ C ) ) ) = (/) )
Assertion	f1resrcmplf1d	|- ( ph -> F : A -1-1-> B )

Proof

Step	Hyp	Ref	Expression
1		f1resrcmplf1d.1	|- ( ph -> C C_ A )
2		f1resrcmplf1d.2	|- ( ph -> F : A --> B )
3		f1resrcmplf1d.3	|- ( ph -> ( F |` C ) : C -1-1-> B )
4		f1resrcmplf1d.4	|- ( ph -> ( F |` ( A \ C ) ) : ( A \ C ) -1-1-> B )
5		f1resrcmplf1d.5	|- ( ph -> ( ( F " C ) i^i ( F " ( A \ C ) ) ) = (/) )
6		f1resveqaeq	|- ( ( ( F |` C ) : C -1-1-> B /\ ( x e. C /\ y e. C ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
7	3 6	sylan	|- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
8	7	ex	|- ( ph -> ( ( x e. C /\ y e. C ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
9		difssd	|- ( ph -> ( A \ C ) C_ A )
10	1 9 2 5	f1resrcmplf1dlem	|- ( ph -> ( ( x e. C /\ y e. ( A \ C ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
11		incom	|- ( ( F " C ) i^i ( F " ( A \ C ) ) ) = ( ( F " ( A \ C ) ) i^i ( F " C ) )
12	11 5	eqtr3id	|- ( ph -> ( ( F " ( A \ C ) ) i^i ( F " C ) ) = (/) )
13	9 1 2 12	f1resrcmplf1dlem	|- ( ph -> ( ( x e. ( A \ C ) /\ y e. C ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
14		f1resveqaeq	|- ( ( ( F |` ( A \ C ) ) : ( A \ C ) -1-1-> B /\ ( x e. ( A \ C ) /\ y e. ( A \ C ) ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
15	4 14	sylan	|- ( ( ph /\ ( x e. ( A \ C ) /\ y e. ( A \ C ) ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
16	15	ex	|- ( ph -> ( ( x e. ( A \ C ) /\ y e. ( A \ C ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
17	8 10 13 16	prsrcmpltd	|- ( ph -> ( ( x e. A /\ y e. A ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
18	17	ralrimivv	|- ( ph -> A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) )
19		dff13	|- ( F : A -1-1-> B <-> ( F : A --> B /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
20	2 18 19	sylanbrc	|- ( ph -> F : A -1-1-> B )