Metamath Proof Explorer

Theorem resf1o

Description: Restriction of functions to a superset of their support creates a bijection. (Contributed by Thierry Arnoux, 12-Sep-2017)

Ref Expression
Hypotheses resf1o.1 
|- X = { f e. ( B ^m A ) | ( `' f " ( B \ { Z } ) ) C_ C }
resf1o.2 
|- F = ( f e. X |-> ( f |` C ) )
Assertion resf1o 
|- ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) -> F : X -1-1-onto-> ( B ^m C ) )

Proof

Step Hyp Ref Expression
1 resf1o.1 
 |-  X = { f e. ( B ^m A ) | ( `' f " ( B \ { Z } ) ) C_ C }
2 resf1o.2 
 |-  F = ( f e. X |-> ( f |` C ) )
3 resexg 
 |-  ( f e. X -> ( f |` C ) e. _V )
4 3 adantl 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ f e. X ) -> ( f |` C ) e. _V )
5 simpr 
 |-  ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ g e. ( B ^m C ) ) -> g e. ( B ^m C ) )
6 difexg 
 |-  ( A e. V -> ( A \ C ) e. _V )
7 6 3ad2ant1 
 |-  ( ( A e. V /\ B e. W /\ C C_ A ) -> ( A \ C ) e. _V )
8 snex 
 |-  { Z } e. _V
9 xpexg 
 |-  ( ( ( A \ C ) e. _V /\ { Z } e. _V ) -> ( ( A \ C ) X. { Z } ) e. _V )
10 7 8 9 sylancl 
 |-  ( ( A e. V /\ B e. W /\ C C_ A ) -> ( ( A \ C ) X. { Z } ) e. _V )
11 10 adantr 
 |-  ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ g e. ( B ^m C ) ) -> ( ( A \ C ) X. { Z } ) e. _V )
12 unexg 
 |-  ( ( g e. ( B ^m C ) /\ ( ( A \ C ) X. { Z } ) e. _V ) -> ( g u. ( ( A \ C ) X. { Z } ) ) e. _V )
13 5 11 12 syl2anc 
 |-  ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ g e. ( B ^m C ) ) -> ( g u. ( ( A \ C ) X. { Z } ) ) e. _V )
14 13 adantlr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ g e. ( B ^m C ) ) -> ( g u. ( ( A \ C ) X. { Z } ) ) e. _V )
15 1 rabeq2i 
 |-  ( f e. X <-> ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) )
16 15 anbi1i 
 |-  ( ( f e. X /\ g = ( f |` C ) ) <-> ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) )
17 simprr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> g = ( f |` C ) )
18 simprll 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> f e. ( B ^m A ) )
19 elmapi 
 |-  ( f e. ( B ^m A ) -> f : A --> B )
20 18 19 syl 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> f : A --> B )
21 simp3 
 |-  ( ( A e. V /\ B e. W /\ C C_ A ) -> C C_ A )
22 21 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> C C_ A )
23 20 22 fssresd 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> ( f |` C ) : C --> B )
24 simp2 
 |-  ( ( A e. V /\ B e. W /\ C C_ A ) -> B e. W )
25 simp1 
 |-  ( ( A e. V /\ B e. W /\ C C_ A ) -> A e. V )
26 25 21 ssexd 
 |-  ( ( A e. V /\ B e. W /\ C C_ A ) -> C e. _V )
27 elmapg 
 |-  ( ( B e. W /\ C e. _V ) -> ( ( f |` C ) e. ( B ^m C ) <-> ( f |` C ) : C --> B ) )
28 24 26 27 syl2anc 
 |-  ( ( A e. V /\ B e. W /\ C C_ A ) -> ( ( f |` C ) e. ( B ^m C ) <-> ( f |` C ) : C --> B ) )
29 28 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> ( ( f |` C ) e. ( B ^m C ) <-> ( f |` C ) : C --> B ) )
30 23 29 mpbird 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> ( f |` C ) e. ( B ^m C ) )
31 17 30 eqeltrd 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> g e. ( B ^m C ) )
32 undif 
 |-  ( C C_ A <-> ( C u. ( A \ C ) ) = A )
33 32 biimpi 
 |-  ( C C_ A -> ( C u. ( A \ C ) ) = A )
34 33 reseq2d 
 |-  ( C C_ A -> ( f |` ( C u. ( A \ C ) ) ) = ( f |` A ) )
35 22 34 syl 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> ( f |` ( C u. ( A \ C ) ) ) = ( f |` A ) )
36 ffn 
 |-  ( f : A --> B -> f Fn A )
37 fnresdm 
 |-  ( f Fn A -> ( f |` A ) = f )
38 20 36 37 3syl 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> ( f |` A ) = f )
39 35 38 eqtr2d 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> f = ( f |` ( C u. ( A \ C ) ) ) )
40 resundi 
 |-  ( f |` ( C u. ( A \ C ) ) ) = ( ( f |` C ) u. ( f |` ( A \ C ) ) )
41 39 40 eqtrdi 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> f = ( ( f |` C ) u. ( f |` ( A \ C ) ) ) )
42 17 eqcomd 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> ( f |` C ) = g )
43 simprlr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> ( `' f " ( B \ { Z } ) ) C_ C )
44 25 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> A e. V )
45 simplr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> Z e. B )
46 eqid 
 |-  ( B \ { Z } ) = ( B \ { Z } )
47 46 ffs2 
 |-  ( ( A e. V /\ Z e. B /\ f : A --> B ) -> ( f supp Z ) = ( `' f " ( B \ { Z } ) ) )
48 44 45 20 47 syl3anc 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> ( f supp Z ) = ( `' f " ( B \ { Z } ) ) )
49 sseqin2 
 |-  ( C C_ A <-> ( A i^i C ) = C )
50 49 biimpi 
 |-  ( C C_ A -> ( A i^i C ) = C )
51 22 50 syl 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> ( A i^i C ) = C )
52 43 48 51 3sstr4d 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> ( f supp Z ) C_ ( A i^i C ) )
53 simpl 
 |-  ( ( f e. ( B ^m A ) /\ Z e. B ) -> f e. ( B ^m A ) )
54 53 19 36 3syl 
 |-  ( ( f e. ( B ^m A ) /\ Z e. B ) -> f Fn A )
55 inundif 
 |-  ( ( A i^i C ) u. ( A \ C ) ) = A
56 55 fneq2i 
 |-  ( f Fn ( ( A i^i C ) u. ( A \ C ) ) <-> f Fn A )
57 54 56 sylibr 
 |-  ( ( f e. ( B ^m A ) /\ Z e. B ) -> f Fn ( ( A i^i C ) u. ( A \ C ) ) )
58 vex 
 |-  f e. _V
59 58 a1i 
 |-  ( ( f e. ( B ^m A ) /\ Z e. B ) -> f e. _V )
60 simpr 
 |-  ( ( f e. ( B ^m A ) /\ Z e. B ) -> Z e. B )
61 inindif 
 |-  ( ( A i^i C ) i^i ( A \ C ) ) = (/)
62 61 a1i 
 |-  ( ( f e. ( B ^m A ) /\ Z e. B ) -> ( ( A i^i C ) i^i ( A \ C ) ) = (/) )
63 fnsuppres 
 |-  ( ( f Fn ( ( A i^i C ) u. ( A \ C ) ) /\ ( f e. _V /\ Z e. B ) /\ ( ( A i^i C ) i^i ( A \ C ) ) = (/) ) -> ( ( f supp Z ) C_ ( A i^i C ) <-> ( f |` ( A \ C ) ) = ( ( A \ C ) X. { Z } ) ) )
64 57 59 60 62 63 syl121anc 
 |-  ( ( f e. ( B ^m A ) /\ Z e. B ) -> ( ( f supp Z ) C_ ( A i^i C ) <-> ( f |` ( A \ C ) ) = ( ( A \ C ) X. { Z } ) ) )
65 18 45 64 syl2anc 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> ( ( f supp Z ) C_ ( A i^i C ) <-> ( f |` ( A \ C ) ) = ( ( A \ C ) X. { Z } ) ) )
66 52 65 mpbid 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> ( f |` ( A \ C ) ) = ( ( A \ C ) X. { Z } ) )
67 42 66 uneq12d 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> ( ( f |` C ) u. ( f |` ( A \ C ) ) ) = ( g u. ( ( A \ C ) X. { Z } ) ) )
68 41 67 eqtrd 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> f = ( g u. ( ( A \ C ) X. { Z } ) ) )
69 31 68 jca 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) ) -> ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) )
70 24 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) -> B e. W )
71 25 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) -> A e. V )
72 elmapi 
 |-  ( g e. ( B ^m C ) -> g : C --> B )
73 72 ad2antrl 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) -> g : C --> B )
74 simplr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) -> Z e. B )
75 fconst6g 
 |-  ( Z e. B -> ( ( A \ C ) X. { Z } ) : ( A \ C ) --> B )
76 74 75 syl 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) -> ( ( A \ C ) X. { Z } ) : ( A \ C ) --> B )
77 disjdif 
 |-  ( C i^i ( A \ C ) ) = (/)
78 77 a1i 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) -> ( C i^i ( A \ C ) ) = (/) )
79 fun2 
 |-  ( ( ( g : C --> B /\ ( ( A \ C ) X. { Z } ) : ( A \ C ) --> B ) /\ ( C i^i ( A \ C ) ) = (/) ) -> ( g u. ( ( A \ C ) X. { Z } ) ) : ( C u. ( A \ C ) ) --> B )
80 73 76 78 79 syl21anc 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) -> ( g u. ( ( A \ C ) X. { Z } ) ) : ( C u. ( A \ C ) ) --> B )
81 simprr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) -> f = ( g u. ( ( A \ C ) X. { Z } ) ) )
82 81 eqcomd 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) -> ( g u. ( ( A \ C ) X. { Z } ) ) = f )
83 21 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) -> C C_ A )
84 83 33 syl 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) -> ( C u. ( A \ C ) ) = A )
85 82 84 feq12d 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) -> ( ( g u. ( ( A \ C ) X. { Z } ) ) : ( C u. ( A \ C ) ) --> B <-> f : A --> B ) )
86 80 85 mpbid 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) -> f : A --> B )
87 elmapg 
 |-  ( ( B e. W /\ A e. V ) -> ( f e. ( B ^m A ) <-> f : A --> B ) )
88 87 biimpar 
 |-  ( ( ( B e. W /\ A e. V ) /\ f : A --> B ) -> f e. ( B ^m A ) )
89 70 71 86 88 syl21anc 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) -> f e. ( B ^m A ) )
90 71 74 86 47 syl3anc 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) -> ( f supp Z ) = ( `' f " ( B \ { Z } ) ) )
91 81 adantr 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) /\ x e. ( A \ C ) ) -> f = ( g u. ( ( A \ C ) X. { Z } ) ) )
92 91 fveq1d 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) /\ x e. ( A \ C ) ) -> ( f ` x ) = ( ( g u. ( ( A \ C ) X. { Z } ) ) ` x ) )
93 73 adantr 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) /\ x e. ( A \ C ) ) -> g : C --> B )
94 93 ffnd 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) /\ x e. ( A \ C ) ) -> g Fn C )
95 fconstg 
 |-  ( Z e. B -> ( ( A \ C ) X. { Z } ) : ( A \ C ) --> { Z } )
96 95 ad3antlr 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) /\ x e. ( A \ C ) ) -> ( ( A \ C ) X. { Z } ) : ( A \ C ) --> { Z } )
97 96 ffnd 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) /\ x e. ( A \ C ) ) -> ( ( A \ C ) X. { Z } ) Fn ( A \ C ) )
98 77 a1i 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) /\ x e. ( A \ C ) ) -> ( C i^i ( A \ C ) ) = (/) )
99 simpr 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) /\ x e. ( A \ C ) ) -> x e. ( A \ C ) )
100 fvun2 
 |-  ( ( g Fn C /\ ( ( A \ C ) X. { Z } ) Fn ( A \ C ) /\ ( ( C i^i ( A \ C ) ) = (/) /\ x e. ( A \ C ) ) ) -> ( ( g u. ( ( A \ C ) X. { Z } ) ) ` x ) = ( ( ( A \ C ) X. { Z } ) ` x ) )
101 94 97 98 99 100 syl112anc 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) /\ x e. ( A \ C ) ) -> ( ( g u. ( ( A \ C ) X. { Z } ) ) ` x ) = ( ( ( A \ C ) X. { Z } ) ` x ) )
102 fvconst 
 |-  ( ( ( ( A \ C ) X. { Z } ) : ( A \ C ) --> { Z } /\ x e. ( A \ C ) ) -> ( ( ( A \ C ) X. { Z } ) ` x ) = Z )
103 96 99 102 syl2anc 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) /\ x e. ( A \ C ) ) -> ( ( ( A \ C ) X. { Z } ) ` x ) = Z )
104 92 101 103 3eqtrd 
 |-  ( ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) /\ x e. ( A \ C ) ) -> ( f ` x ) = Z )
105 86 104 suppss 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) -> ( f supp Z ) C_ C )
106 90 105 eqsstrrd 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) -> ( `' f " ( B \ { Z } ) ) C_ C )
107 81 reseq1d 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) -> ( f |` C ) = ( ( g u. ( ( A \ C ) X. { Z } ) ) |` C ) )
108 res0 
 |-  ( ( ( A \ C ) X. { Z } ) |` (/) ) = (/)
109 res0 
 |-  ( g |` (/) ) = (/)
110 108 109 eqtr4i 
 |-  ( ( ( A \ C ) X. { Z } ) |` (/) ) = ( g |` (/) )
111 77 reseq2i 
 |-  ( ( ( A \ C ) X. { Z } ) |` ( C i^i ( A \ C ) ) ) = ( ( ( A \ C ) X. { Z } ) |` (/) )
112 77 reseq2i 
 |-  ( g |` ( C i^i ( A \ C ) ) ) = ( g |` (/) )
113 110 111 112 3eqtr4ri 
 |-  ( g |` ( C i^i ( A \ C ) ) ) = ( ( ( A \ C ) X. { Z } ) |` ( C i^i ( A \ C ) ) )
114 113 a1i 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) -> ( g |` ( C i^i ( A \ C ) ) ) = ( ( ( A \ C ) X. { Z } ) |` ( C i^i ( A \ C ) ) ) )
115 fresaunres1 
 |-  ( ( g : C --> B /\ ( ( A \ C ) X. { Z } ) : ( A \ C ) --> B /\ ( g |` ( C i^i ( A \ C ) ) ) = ( ( ( A \ C ) X. { Z } ) |` ( C i^i ( A \ C ) ) ) ) -> ( ( g u. ( ( A \ C ) X. { Z } ) ) |` C ) = g )
116 73 76 114 115 syl3anc 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) -> ( ( g u. ( ( A \ C ) X. { Z } ) ) |` C ) = g )
117 107 116 eqtr2d 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) -> g = ( f |` C ) )
118 89 106 117 jca31 
 |-  ( ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) /\ ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) -> ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) )
119 69 118 impbida 
 |-  ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) -> ( ( ( f e. ( B ^m A ) /\ ( `' f " ( B \ { Z } ) ) C_ C ) /\ g = ( f |` C ) ) <-> ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) )
120 16 119 syl5bb 
 |-  ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) -> ( ( f e. X /\ g = ( f |` C ) ) <-> ( g e. ( B ^m C ) /\ f = ( g u. ( ( A \ C ) X. { Z } ) ) ) ) )
121 2 4 14 120 f1od 
 |-  ( ( ( A e. V /\ B e. W /\ C C_ A ) /\ Z e. B ) -> F : X -1-1-onto-> ( B ^m C ) )