Metamath Proof Explorer

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 1 3ad2ant1 
 |-  ( ( ph /\ ( x e. C /\ y e. ( A \ C ) ) /\ ( F ` x ) = ( F ` y ) ) -> C C_ A )
10 difssd 
 |-  ( ph -> ( A \ C ) C_ A )
11 10 3ad2ant1 
 |-  ( ( ph /\ ( x e. C /\ y e. ( A \ C ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( A \ C ) C_ A )
12 2 3ad2ant1 
 |-  ( ( ph /\ ( x e. C /\ y e. ( A \ C ) ) /\ ( F ` x ) = ( F ` y ) ) -> F : A --> B )
13 5 3ad2ant1 
 |-  ( ( ph /\ ( x e. C /\ y e. ( A \ C ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( ( F " C ) i^i ( F " ( A \ C ) ) ) = (/) )
14 simp2l 
 |-  ( ( ph /\ ( x e. C /\ y e. ( A \ C ) ) /\ ( F ` x ) = ( F ` y ) ) -> x e. C )
15 simp2r 
 |-  ( ( ph /\ ( x e. C /\ y e. ( A \ C ) ) /\ ( F ` x ) = ( F ` y ) ) -> y e. ( A \ C ) )
16 simp3 
 |-  ( ( ph /\ ( x e. C /\ y e. ( A \ C ) ) /\ ( F ` x ) = ( F ` y ) ) -> ( F ` x ) = ( F ` y ) )
17 9 11 12 13 14 15 16 f1resrcmplf1dlem 
 |-  ( ( ph /\ ( x e. C /\ y e. ( A \ C ) ) /\ ( F ` x ) = ( F ` y ) ) -> x = y )
18 17 3exp 
 |-  ( ph -> ( ( x e. C /\ y e. ( A \ C ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
19 10 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( A \ C ) /\ y e. C ) /\ ( F ` x ) = ( F ` y ) ) -> ( A \ C ) C_ A )
20 1 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( A \ C ) /\ y e. C ) /\ ( F ` x ) = ( F ` y ) ) -> C C_ A )
21 2 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( A \ C ) /\ y e. C ) /\ ( F ` x ) = ( F ` y ) ) -> F : A --> B )
22 incom 
 |-  ( ( F " C ) i^i ( F " ( A \ C ) ) ) = ( ( F " ( A \ C ) ) i^i ( F " C ) )
23 22 5 eqtr3id 
 |-  ( ph -> ( ( F " ( A \ C ) ) i^i ( F " C ) ) = (/) )
24 23 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( A \ C ) /\ y e. C ) /\ ( F ` x ) = ( F ` y ) ) -> ( ( F " ( A \ C ) ) i^i ( F " C ) ) = (/) )
25 simp2l 
 |-  ( ( ph /\ ( x e. ( A \ C ) /\ y e. C ) /\ ( F ` x ) = ( F ` y ) ) -> x e. ( A \ C ) )
26 simp2r 
 |-  ( ( ph /\ ( x e. ( A \ C ) /\ y e. C ) /\ ( F ` x ) = ( F ` y ) ) -> y e. C )
27 simp3 
 |-  ( ( ph /\ ( x e. ( A \ C ) /\ y e. C ) /\ ( F ` x ) = ( F ` y ) ) -> ( F ` x ) = ( F ` y ) )
28 19 20 21 24 25 26 27 f1resrcmplf1dlem 
 |-  ( ( ph /\ ( x e. ( A \ C ) /\ y e. C ) /\ ( F ` x ) = ( F ` y ) ) -> x = y )
29 28 3exp 
 |-  ( ph -> ( ( x e. ( A \ C ) /\ y e. C ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
30 f1resveqaeq 
 |-  ( ( ( F |` ( A \ C ) ) : ( A \ C ) -1-1-> B /\ ( x e. ( A \ C ) /\ y e. ( A \ C ) ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
31 4 30 sylan 
 |-  ( ( ph /\ ( x e. ( A \ C ) /\ y e. ( A \ C ) ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
32 31 ex 
 |-  ( ph -> ( ( x e. ( A \ C ) /\ y e. ( A \ C ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
33 8 18 29 32 prsrcmpltd 
 |-  ( ph -> ( ( x e. A /\ y e. A ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
34 33 ralrimivv 
 |-  ( ph -> A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) )
35 dff13 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
36 2 34 35 sylanbrc 
 |-  ( ph -> F : A -1-1-> B )