Metamath Proof Explorer

Theorem resf1extb

Description: Extension of an injection which is a restriction of a function. (Contributed by AV, 3-Oct-2025)

Ref Expression
Assertion resf1extb 
|- ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> ( ( ( F |` C ) : C -1-1-> B /\ ( F ` X ) e/ ( F " C ) ) <-> ( F |` ( C u. { X } ) ) : ( C u. { X } ) -1-1-> B ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> F : A --> B )
2 simp3 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> C C_ A )
3 eldifi 
 |-  ( X e. ( A \ C ) -> X e. A )
4 3 snssd 
 |-  ( X e. ( A \ C ) -> { X } C_ A )
5 4 3ad2ant2 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> { X } C_ A )
6 2 5 unssd 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> ( C u. { X } ) C_ A )
7 1 6 fssresd 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> ( F |` ( C u. { X } ) ) : ( C u. { X } ) --> B )
8 7 adantr 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( ( F |` C ) : C -1-1-> B /\ ( F ` X ) e/ ( F " C ) ) ) -> ( F |` ( C u. { X } ) ) : ( C u. { X } ) --> B )
9 elun 
 |-  ( y e. ( C u. { X } ) <-> ( y e. C \/ y e. { X } ) )
10 elun 
 |-  ( z e. ( C u. { X } ) <-> ( z e. C \/ z e. { X } ) )
11 9 10 anbi12i 
 |-  ( ( y e. ( C u. { X } ) /\ z e. ( C u. { X } ) ) <-> ( ( y e. C \/ y e. { X } ) /\ ( z e. C \/ z e. { X } ) ) )
12 dff14a 
 |-  ( ( F |` C ) : C -1-1-> B <-> ( ( F |` C ) : C --> B /\ A. w e. C A. x e. C ( w =/= x -> ( ( F |` C ) ` w ) =/= ( ( F |` C ) ` x ) ) ) )
13 neeq1 
 |-  ( w = y -> ( w =/= x <-> y =/= x ) )
14 fveq2 
 |-  ( w = y -> ( ( F |` C ) ` w ) = ( ( F |` C ) ` y ) )
15 14 neeq1d 
 |-  ( w = y -> ( ( ( F |` C ) ` w ) =/= ( ( F |` C ) ` x ) <-> ( ( F |` C ) ` y ) =/= ( ( F |` C ) ` x ) ) )
16 13 15 imbi12d 
 |-  ( w = y -> ( ( w =/= x -> ( ( F |` C ) ` w ) =/= ( ( F |` C ) ` x ) ) <-> ( y =/= x -> ( ( F |` C ) ` y ) =/= ( ( F |` C ) ` x ) ) ) )
17 neeq2 
 |-  ( x = z -> ( y =/= x <-> y =/= z ) )
18 fveq2 
 |-  ( x = z -> ( ( F |` C ) ` x ) = ( ( F |` C ) ` z ) )
19 18 neeq2d 
 |-  ( x = z -> ( ( ( F |` C ) ` y ) =/= ( ( F |` C ) ` x ) <-> ( ( F |` C ) ` y ) =/= ( ( F |` C ) ` z ) ) )
20 17 19 imbi12d 
 |-  ( x = z -> ( ( y =/= x -> ( ( F |` C ) ` y ) =/= ( ( F |` C ) ` x ) ) <-> ( y =/= z -> ( ( F |` C ) ` y ) =/= ( ( F |` C ) ` z ) ) ) )
21 16 20 rspc2v 
 |-  ( ( y e. C /\ z e. C ) -> ( A. w e. C A. x e. C ( w =/= x -> ( ( F |` C ) ` w ) =/= ( ( F |` C ) ` x ) ) -> ( y =/= z -> ( ( F |` C ) ` y ) =/= ( ( F |` C ) ` z ) ) ) )
22 simpl 
 |-  ( ( y e. C /\ z e. C ) -> y e. C )
23 22 fvresd 
 |-  ( ( y e. C /\ z e. C ) -> ( ( F |` C ) ` y ) = ( F ` y ) )
24 simpr 
 |-  ( ( y e. C /\ z e. C ) -> z e. C )
25 24 fvresd 
 |-  ( ( y e. C /\ z e. C ) -> ( ( F |` C ) ` z ) = ( F ` z ) )
26 23 25 neeq12d 
 |-  ( ( y e. C /\ z e. C ) -> ( ( ( F |` C ) ` y ) =/= ( ( F |` C ) ` z ) <-> ( F ` y ) =/= ( F ` z ) ) )
27 26 imbi2d 
 |-  ( ( y e. C /\ z e. C ) -> ( ( y =/= z -> ( ( F |` C ) ` y ) =/= ( ( F |` C ) ` z ) ) <-> ( y =/= z -> ( F ` y ) =/= ( F ` z ) ) ) )
28 27 bi23imp13 
 |-  ( ( ( y e. C /\ z e. C ) /\ ( y =/= z -> ( ( F |` C ) ` y ) =/= ( ( F |` C ) ` z ) ) /\ y =/= z ) -> ( F ` y ) =/= ( F ` z ) )
29 elun1 
 |-  ( y e. C -> y e. ( C u. { X } ) )
30 29 adantr 
 |-  ( ( y e. C /\ z e. C ) -> y e. ( C u. { X } ) )
31 30 fvresd 
 |-  ( ( y e. C /\ z e. C ) -> ( ( F |` ( C u. { X } ) ) ` y ) = ( F ` y ) )
32 elun1 
 |-  ( z e. C -> z e. ( C u. { X } ) )
33 32 adantl 
 |-  ( ( y e. C /\ z e. C ) -> z e. ( C u. { X } ) )
34 33 fvresd 
 |-  ( ( y e. C /\ z e. C ) -> ( ( F |` ( C u. { X } ) ) ` z ) = ( F ` z ) )
35 31 34 neeq12d 
 |-  ( ( y e. C /\ z e. C ) -> ( ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) <-> ( F ` y ) =/= ( F ` z ) ) )
36 35 3ad2ant1 
 |-  ( ( ( y e. C /\ z e. C ) /\ ( y =/= z -> ( ( F |` C ) ` y ) =/= ( ( F |` C ) ` z ) ) /\ y =/= z ) -> ( ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) <-> ( F ` y ) =/= ( F ` z ) ) )
37 28 36 mpbird 
 |-  ( ( ( y e. C /\ z e. C ) /\ ( y =/= z -> ( ( F |` C ) ` y ) =/= ( ( F |` C ) ` z ) ) /\ y =/= z ) -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) )
38 37 3exp 
 |-  ( ( y e. C /\ z e. C ) -> ( ( y =/= z -> ( ( F |` C ) ` y ) =/= ( ( F |` C ) ` z ) ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) )
39 21 38 syldc 
 |-  ( A. w e. C A. x e. C ( w =/= x -> ( ( F |` C ) ` w ) =/= ( ( F |` C ) ` x ) ) -> ( ( y e. C /\ z e. C ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) )
40 39 adantl 
 |-  ( ( ( F |` C ) : C --> B /\ A. w e. C A. x e. C ( w =/= x -> ( ( F |` C ) ` w ) =/= ( ( F |` C ) ` x ) ) ) -> ( ( y e. C /\ z e. C ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) )
41 40 a1i 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> ( ( ( F |` C ) : C --> B /\ A. w e. C A. x e. C ( w =/= x -> ( ( F |` C ) ` w ) =/= ( ( F |` C ) ` x ) ) ) -> ( ( y e. C /\ z e. C ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) ) )
42 12 41 biimtrid 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> ( ( F |` C ) : C -1-1-> B -> ( ( y e. C /\ z e. C ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) ) )
43 42 a1dd 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> ( ( F |` C ) : C -1-1-> B -> ( ( F ` X ) e/ ( F " C ) -> ( ( y e. C /\ z e. C ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) ) ) )
44 43 imp32 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( ( F |` C ) : C -1-1-> B /\ ( F ` X ) e/ ( F " C ) ) ) -> ( ( y e. C /\ z e. C ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) )
45 ffn 
 |-  ( F : A --> B -> F Fn A )
46 45 3ad2ant1 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> F Fn A )
47 46 2 fvelimabd 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> ( ( F ` X ) e. ( F " C ) <-> E. x e. C ( F ` x ) = ( F ` X ) ) )
48 47 notbid 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> ( -. ( F ` X ) e. ( F " C ) <-> -. E. x e. C ( F ` x ) = ( F ` X ) ) )
49 df-nel 
 |-  ( ( F ` X ) e/ ( F " C ) <-> -. ( F ` X ) e. ( F " C ) )
50 ralnex 
 |-  ( A. x e. C -. ( F ` x ) = ( F ` X ) <-> -. E. x e. C ( F ` x ) = ( F ` X ) )
51 48 49 50 3bitr4g 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> ( ( F ` X ) e/ ( F " C ) <-> A. x e. C -. ( F ` x ) = ( F ` X ) ) )
52 df-ne 
 |-  ( ( F ` x ) =/= ( F ` X ) <-> -. ( F ` x ) = ( F ` X ) )
53 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
54 53 neeq1d 
 |-  ( x = z -> ( ( F ` x ) =/= ( F ` X ) <-> ( F ` z ) =/= ( F ` X ) ) )
55 52 54 bitr3id 
 |-  ( x = z -> ( -. ( F ` x ) = ( F ` X ) <-> ( F ` z ) =/= ( F ` X ) ) )
56 55 rspcv 
 |-  ( z e. C -> ( A. x e. C -. ( F ` x ) = ( F ` X ) -> ( F ` z ) =/= ( F ` X ) ) )
57 56 ad2antll 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. { X } /\ z e. C ) ) -> ( A. x e. C -. ( F ` x ) = ( F ` X ) -> ( F ` z ) =/= ( F ` X ) ) )
58 32 ad2antll 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. { X } /\ z e. C ) ) -> z e. ( C u. { X } ) )
59 58 fvresd 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. { X } /\ z e. C ) ) -> ( ( F |` ( C u. { X } ) ) ` z ) = ( F ` z ) )
60 59 eqcomd 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. { X } /\ z e. C ) ) -> ( F ` z ) = ( ( F |` ( C u. { X } ) ) ` z ) )
61 elsni 
 |-  ( y e. { X } -> y = X )
62 61 eqcomd 
 |-  ( y e. { X } -> X = y )
63 62 ad2antrl 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. { X } /\ z e. C ) ) -> X = y )
64 63 fveq2d 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. { X } /\ z e. C ) ) -> ( F ` X ) = ( F ` y ) )
65 elun2 
 |-  ( y e. { X } -> y e. ( C u. { X } ) )
66 65 ad2antrl 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. { X } /\ z e. C ) ) -> y e. ( C u. { X } ) )
67 66 fvresd 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. { X } /\ z e. C ) ) -> ( ( F |` ( C u. { X } ) ) ` y ) = ( F ` y ) )
68 64 67 eqtr4d 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. { X } /\ z e. C ) ) -> ( F ` X ) = ( ( F |` ( C u. { X } ) ) ` y ) )
69 60 68 neeq12d 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. { X } /\ z e. C ) ) -> ( ( F ` z ) =/= ( F ` X ) <-> ( ( F |` ( C u. { X } ) ) ` z ) =/= ( ( F |` ( C u. { X } ) ) ` y ) ) )
70 69 biimpa 
 |-  ( ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. { X } /\ z e. C ) ) /\ ( F ` z ) =/= ( F ` X ) ) -> ( ( F |` ( C u. { X } ) ) ` z ) =/= ( ( F |` ( C u. { X } ) ) ` y ) )
71 70 necomd 
 |-  ( ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. { X } /\ z e. C ) ) /\ ( F ` z ) =/= ( F ` X ) ) -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) )
72 71 a1d 
 |-  ( ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. { X } /\ z e. C ) ) /\ ( F ` z ) =/= ( F ` X ) ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) )
73 72 ex 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. { X } /\ z e. C ) ) -> ( ( F ` z ) =/= ( F ` X ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) )
74 57 73 syld 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. { X } /\ z e. C ) ) -> ( A. x e. C -. ( F ` x ) = ( F ` X ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) )
75 74 a1d 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. { X } /\ z e. C ) ) -> ( ( F |` C ) : C -1-1-> B -> ( A. x e. C -. ( F ` x ) = ( F ` X ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) ) )
76 75 ex 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> ( ( y e. { X } /\ z e. C ) -> ( ( F |` C ) : C -1-1-> B -> ( A. x e. C -. ( F ` x ) = ( F ` X ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) ) ) )
77 76 com24 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> ( A. x e. C -. ( F ` x ) = ( F ` X ) -> ( ( F |` C ) : C -1-1-> B -> ( ( y e. { X } /\ z e. C ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) ) ) )
78 51 77 sylbid 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> ( ( F ` X ) e/ ( F " C ) -> ( ( F |` C ) : C -1-1-> B -> ( ( y e. { X } /\ z e. C ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) ) ) )
79 78 impcomd 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> ( ( ( F |` C ) : C -1-1-> B /\ ( F ` X ) e/ ( F " C ) ) -> ( ( y e. { X } /\ z e. C ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) ) )
80 79 imp 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( ( F |` C ) : C -1-1-> B /\ ( F ` X ) e/ ( F " C ) ) ) -> ( ( y e. { X } /\ z e. C ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) )
81 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
82 81 neeq1d 
 |-  ( x = y -> ( ( F ` x ) =/= ( F ` X ) <-> ( F ` y ) =/= ( F ` X ) ) )
83 52 82 bitr3id 
 |-  ( x = y -> ( -. ( F ` x ) = ( F ` X ) <-> ( F ` y ) =/= ( F ` X ) ) )
84 83 rspcv 
 |-  ( y e. C -> ( A. x e. C -. ( F ` x ) = ( F ` X ) -> ( F ` y ) =/= ( F ` X ) ) )
85 84 ad2antrl 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. C /\ z e. { X } ) ) -> ( A. x e. C -. ( F ` x ) = ( F ` X ) -> ( F ` y ) =/= ( F ` X ) ) )
86 29 ad2antrl 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. C /\ z e. { X } ) ) -> y e. ( C u. { X } ) )
87 86 fvresd 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. C /\ z e. { X } ) ) -> ( ( F |` ( C u. { X } ) ) ` y ) = ( F ` y ) )
88 87 eqcomd 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. C /\ z e. { X } ) ) -> ( F ` y ) = ( ( F |` ( C u. { X } ) ) ` y ) )
89 elsni 
 |-  ( z e. { X } -> z = X )
90 89 eqcomd 
 |-  ( z e. { X } -> X = z )
91 90 ad2antll 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. C /\ z e. { X } ) ) -> X = z )
92 91 fveq2d 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. C /\ z e. { X } ) ) -> ( F ` X ) = ( F ` z ) )
93 elun2 
 |-  ( z e. { X } -> z e. ( C u. { X } ) )
94 93 ad2antll 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. C /\ z e. { X } ) ) -> z e. ( C u. { X } ) )
95 94 fvresd 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. C /\ z e. { X } ) ) -> ( ( F |` ( C u. { X } ) ) ` z ) = ( F ` z ) )
96 92 95 eqtr4d 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. C /\ z e. { X } ) ) -> ( F ` X ) = ( ( F |` ( C u. { X } ) ) ` z ) )
97 88 96 neeq12d 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. C /\ z e. { X } ) ) -> ( ( F ` y ) =/= ( F ` X ) <-> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) )
98 97 biimpd 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. C /\ z e. { X } ) ) -> ( ( F ` y ) =/= ( F ` X ) -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) )
99 98 a1dd 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. C /\ z e. { X } ) ) -> ( ( F ` y ) =/= ( F ` X ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) )
100 85 99 syld 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. C /\ z e. { X } ) ) -> ( A. x e. C -. ( F ` x ) = ( F ` X ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) )
101 100 a1d 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( y e. C /\ z e. { X } ) ) -> ( ( F |` C ) : C -1-1-> B -> ( A. x e. C -. ( F ` x ) = ( F ` X ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) ) )
102 101 ex 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> ( ( y e. C /\ z e. { X } ) -> ( ( F |` C ) : C -1-1-> B -> ( A. x e. C -. ( F ` x ) = ( F ` X ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) ) ) )
103 102 com24 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> ( A. x e. C -. ( F ` x ) = ( F ` X ) -> ( ( F |` C ) : C -1-1-> B -> ( ( y e. C /\ z e. { X } ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) ) ) )
104 51 103 sylbid 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> ( ( F ` X ) e/ ( F " C ) -> ( ( F |` C ) : C -1-1-> B -> ( ( y e. C /\ z e. { X } ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) ) ) )
105 104 impcomd 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> ( ( ( F |` C ) : C -1-1-> B /\ ( F ` X ) e/ ( F " C ) ) -> ( ( y e. C /\ z e. { X } ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) ) )
106 105 imp 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( ( F |` C ) : C -1-1-> B /\ ( F ` X ) e/ ( F " C ) ) ) -> ( ( y e. C /\ z e. { X } ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) )
107 velsn 
 |-  ( y e. { X } <-> y = X )
108 velsn 
 |-  ( z e. { X } <-> z = X )
109 eqtr3 
 |-  ( ( y = X /\ z = X ) -> y = z )
110 eqneqall 
 |-  ( y = z -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) )
111 109 110 syl 
 |-  ( ( y = X /\ z = X ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) )
112 107 108 111 syl2anb 
 |-  ( ( y e. { X } /\ z e. { X } ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) )
113 112 a1i 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( ( F |` C ) : C -1-1-> B /\ ( F ` X ) e/ ( F " C ) ) ) -> ( ( y e. { X } /\ z e. { X } ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) )
114 44 80 106 113 ccased 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( ( F |` C ) : C -1-1-> B /\ ( F ` X ) e/ ( F " C ) ) ) -> ( ( ( y e. C \/ y e. { X } ) /\ ( z e. C \/ z e. { X } ) ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) )
115 11 114 biimtrid 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( ( F |` C ) : C -1-1-> B /\ ( F ` X ) e/ ( F " C ) ) ) -> ( ( y e. ( C u. { X } ) /\ z e. ( C u. { X } ) ) -> ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) )
116 115 ralrimivv 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( ( F |` C ) : C -1-1-> B /\ ( F ` X ) e/ ( F " C ) ) ) -> A. y e. ( C u. { X } ) A. z e. ( C u. { X } ) ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) )
117 dff14a 
 |-  ( ( F |` ( C u. { X } ) ) : ( C u. { X } ) -1-1-> B <-> ( ( F |` ( C u. { X } ) ) : ( C u. { X } ) --> B /\ A. y e. ( C u. { X } ) A. z e. ( C u. { X } ) ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) )
118 8 116 117 sylanbrc 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( ( F |` C ) : C -1-1-> B /\ ( F ` X ) e/ ( F " C ) ) ) -> ( F |` ( C u. { X } ) ) : ( C u. { X } ) -1-1-> B )
119 fssres 
 |-  ( ( F : A --> B /\ C C_ A ) -> ( F |` C ) : C --> B )
120 119 3adant2 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> ( F |` C ) : C --> B )
121 120 adantr 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( F |` ( C u. { X } ) ) : ( C u. { X } ) -1-1-> B ) -> ( F |` C ) : C --> B )
122 df-f1 
 |-  ( ( F |` ( C u. { X } ) ) : ( C u. { X } ) -1-1-> B <-> ( ( F |` ( C u. { X } ) ) : ( C u. { X } ) --> B /\ Fun `' ( F |` ( C u. { X } ) ) ) )
123 funres11 
 |-  ( Fun `' ( F |` ( C u. { X } ) ) -> Fun `' ( ( F |` ( C u. { X } ) ) |` C ) )
124 122 123 simplbiim 
 |-  ( ( F |` ( C u. { X } ) ) : ( C u. { X } ) -1-1-> B -> Fun `' ( ( F |` ( C u. { X } ) ) |` C ) )
125 124 adantl 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( F |` ( C u. { X } ) ) : ( C u. { X } ) -1-1-> B ) -> Fun `' ( ( F |` ( C u. { X } ) ) |` C ) )
126 ssun1 
 |-  C C_ ( C u. { X } )
127 126 resabs1i 
 |-  ( ( F |` ( C u. { X } ) ) |` C ) = ( F |` C )
128 127 eqcomi 
 |-  ( F |` C ) = ( ( F |` ( C u. { X } ) ) |` C )
129 128 cnveqi 
 |-  `' ( F |` C ) = `' ( ( F |` ( C u. { X } ) ) |` C )
130 129 funeqi 
 |-  ( Fun `' ( F |` C ) <-> Fun `' ( ( F |` ( C u. { X } ) ) |` C ) )
131 125 130 sylibr 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( F |` ( C u. { X } ) ) : ( C u. { X } ) -1-1-> B ) -> Fun `' ( F |` C ) )
132 df-f1 
 |-  ( ( F |` C ) : C -1-1-> B <-> ( ( F |` C ) : C --> B /\ Fun `' ( F |` C ) ) )
133 121 131 132 sylanbrc 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( F |` ( C u. { X } ) ) : ( C u. { X } ) -1-1-> B ) -> ( F |` C ) : C -1-1-> B )
134 elun1 
 |-  ( x e. C -> x e. ( C u. { X } ) )
135 snidg 
 |-  ( X e. ( A \ C ) -> X e. { X } )
136 135 3ad2ant2 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> X e. { X } )
137 elun2 
 |-  ( X e. { X } -> X e. ( C u. { X } ) )
138 136 137 syl 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> X e. ( C u. { X } ) )
139 neeq1 
 |-  ( y = x -> ( y =/= z <-> x =/= z ) )
140 fveq2 
 |-  ( y = x -> ( ( F |` ( C u. { X } ) ) ` y ) = ( ( F |` ( C u. { X } ) ) ` x ) )
141 140 neeq1d 
 |-  ( y = x -> ( ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) <-> ( ( F |` ( C u. { X } ) ) ` x ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) )
142 139 141 imbi12d 
 |-  ( y = x -> ( ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) <-> ( x =/= z -> ( ( F |` ( C u. { X } ) ) ` x ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) )
143 neeq2 
 |-  ( z = X -> ( x =/= z <-> x =/= X ) )
144 fveq2 
 |-  ( z = X -> ( ( F |` ( C u. { X } ) ) ` z ) = ( ( F |` ( C u. { X } ) ) ` X ) )
145 144 neeq2d 
 |-  ( z = X -> ( ( ( F |` ( C u. { X } ) ) ` x ) =/= ( ( F |` ( C u. { X } ) ) ` z ) <-> ( ( F |` ( C u. { X } ) ) ` x ) =/= ( ( F |` ( C u. { X } ) ) ` X ) ) )
146 143 145 imbi12d 
 |-  ( z = X -> ( ( x =/= z -> ( ( F |` ( C u. { X } ) ) ` x ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) <-> ( x =/= X -> ( ( F |` ( C u. { X } ) ) ` x ) =/= ( ( F |` ( C u. { X } ) ) ` X ) ) ) )
147 142 146 rspc2v 
 |-  ( ( x e. ( C u. { X } ) /\ X e. ( C u. { X } ) ) -> ( A. y e. ( C u. { X } ) A. z e. ( C u. { X } ) ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) -> ( x =/= X -> ( ( F |` ( C u. { X } ) ) ` x ) =/= ( ( F |` ( C u. { X } ) ) ` X ) ) ) )
148 134 138 147 syl2anr 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ x e. C ) -> ( A. y e. ( C u. { X } ) A. z e. ( C u. { X } ) ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) -> ( x =/= X -> ( ( F |` ( C u. { X } ) ) ` x ) =/= ( ( F |` ( C u. { X } ) ) ` X ) ) ) )
149 148 adantr 
 |-  ( ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ x e. C ) /\ ( F |` ( C u. { X } ) ) : ( C u. { X } ) --> B ) -> ( A. y e. ( C u. { X } ) A. z e. ( C u. { X } ) ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) -> ( x =/= X -> ( ( F |` ( C u. { X } ) ) ` x ) =/= ( ( F |` ( C u. { X } ) ) ` X ) ) ) )
150 eldifn 
 |-  ( X e. ( A \ C ) -> -. X e. C )
151 nelelne 
 |-  ( -. X e. C -> ( x e. C -> x =/= X ) )
152 150 151 syl 
 |-  ( X e. ( A \ C ) -> ( x e. C -> x =/= X ) )
153 152 3ad2ant2 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> ( x e. C -> x =/= X ) )
154 153 imp 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ x e. C ) -> x =/= X )
155 154 adantr 
 |-  ( ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ x e. C ) /\ ( F |` ( C u. { X } ) ) : ( C u. { X } ) --> B ) -> x =/= X )
156 pm2.27 
 |-  ( x =/= X -> ( ( x =/= X -> ( ( F |` ( C u. { X } ) ) ` x ) =/= ( ( F |` ( C u. { X } ) ) ` X ) ) -> ( ( F |` ( C u. { X } ) ) ` x ) =/= ( ( F |` ( C u. { X } ) ) ` X ) ) )
157 155 156 syl 
 |-  ( ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ x e. C ) /\ ( F |` ( C u. { X } ) ) : ( C u. { X } ) --> B ) -> ( ( x =/= X -> ( ( F |` ( C u. { X } ) ) ` x ) =/= ( ( F |` ( C u. { X } ) ) ` X ) ) -> ( ( F |` ( C u. { X } ) ) ` x ) =/= ( ( F |` ( C u. { X } ) ) ` X ) ) )
158 134 adantl 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ x e. C ) -> x e. ( C u. { X } ) )
159 158 adantr 
 |-  ( ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ x e. C ) /\ ( F |` ( C u. { X } ) ) : ( C u. { X } ) --> B ) -> x e. ( C u. { X } ) )
160 159 fvresd 
 |-  ( ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ x e. C ) /\ ( F |` ( C u. { X } ) ) : ( C u. { X } ) --> B ) -> ( ( F |` ( C u. { X } ) ) ` x ) = ( F ` x ) )
161 135 137 syl 
 |-  ( X e. ( A \ C ) -> X e. ( C u. { X } ) )
162 161 3ad2ant2 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> X e. ( C u. { X } ) )
163 162 adantr 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ x e. C ) -> X e. ( C u. { X } ) )
164 163 fvresd 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ x e. C ) -> ( ( F |` ( C u. { X } ) ) ` X ) = ( F ` X ) )
165 164 adantr 
 |-  ( ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ x e. C ) /\ ( F |` ( C u. { X } ) ) : ( C u. { X } ) --> B ) -> ( ( F |` ( C u. { X } ) ) ` X ) = ( F ` X ) )
166 160 165 neeq12d 
 |-  ( ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ x e. C ) /\ ( F |` ( C u. { X } ) ) : ( C u. { X } ) --> B ) -> ( ( ( F |` ( C u. { X } ) ) ` x ) =/= ( ( F |` ( C u. { X } ) ) ` X ) <-> ( F ` x ) =/= ( F ` X ) ) )
167 157 166 sylibd 
 |-  ( ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ x e. C ) /\ ( F |` ( C u. { X } ) ) : ( C u. { X } ) --> B ) -> ( ( x =/= X -> ( ( F |` ( C u. { X } ) ) ` x ) =/= ( ( F |` ( C u. { X } ) ) ` X ) ) -> ( F ` x ) =/= ( F ` X ) ) )
168 149 167 syld 
 |-  ( ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ x e. C ) /\ ( F |` ( C u. { X } ) ) : ( C u. { X } ) --> B ) -> ( A. y e. ( C u. { X } ) A. z e. ( C u. { X } ) ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) -> ( F ` x ) =/= ( F ` X ) ) )
169 168 expimpd 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ x e. C ) -> ( ( ( F |` ( C u. { X } ) ) : ( C u. { X } ) --> B /\ A. y e. ( C u. { X } ) A. z e. ( C u. { X } ) ( y =/= z -> ( ( F |` ( C u. { X } ) ) ` y ) =/= ( ( F |` ( C u. { X } ) ) ` z ) ) ) -> ( F ` x ) =/= ( F ` X ) ) )
170 117 169 biimtrid 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ x e. C ) -> ( ( F |` ( C u. { X } ) ) : ( C u. { X } ) -1-1-> B -> ( F ` x ) =/= ( F ` X ) ) )
171 170 impancom 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( F |` ( C u. { X } ) ) : ( C u. { X } ) -1-1-> B ) -> ( x e. C -> ( F ` x ) =/= ( F ` X ) ) )
172 171 imp 
 |-  ( ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( F |` ( C u. { X } ) ) : ( C u. { X } ) -1-1-> B ) /\ x e. C ) -> ( F ` x ) =/= ( F ` X ) )
173 172 neneqd 
 |-  ( ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( F |` ( C u. { X } ) ) : ( C u. { X } ) -1-1-> B ) /\ x e. C ) -> -. ( F ` x ) = ( F ` X ) )
174 173 ralrimiva 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( F |` ( C u. { X } ) ) : ( C u. { X } ) -1-1-> B ) -> A. x e. C -. ( F ` x ) = ( F ` X ) )
175 51 adantr 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( F |` ( C u. { X } ) ) : ( C u. { X } ) -1-1-> B ) -> ( ( F ` X ) e/ ( F " C ) <-> A. x e. C -. ( F ` x ) = ( F ` X ) ) )
176 174 175 mpbird 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( F |` ( C u. { X } ) ) : ( C u. { X } ) -1-1-> B ) -> ( F ` X ) e/ ( F " C ) )
177 133 176 jca 
 |-  ( ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) /\ ( F |` ( C u. { X } ) ) : ( C u. { X } ) -1-1-> B ) -> ( ( F |` C ) : C -1-1-> B /\ ( F ` X ) e/ ( F " C ) ) )
178 118 177 impbida 
 |-  ( ( F : A --> B /\ X e. ( A \ C ) /\ C C_ A ) -> ( ( ( F |` C ) : C -1-1-> B /\ ( F ` X ) e/ ( F " C ) ) <-> ( F |` ( C u. { X } ) ) : ( C u. { X } ) -1-1-> B ) )