Metamath Proof Explorer

Theorem hashf1lem1

Description: Lemma for hashf1 . (Contributed by Mario Carneiro, 17-Apr-2015) (Proof shortened by AV, 14-Aug-2024)

Ref Expression
Hypotheses hashf1lem2.1 
|- ( ph -> A e. Fin )
hashf1lem2.2 
|- ( ph -> B e. Fin )
hashf1lem2.3 
|- ( ph -> -. z e. A )
hashf1lem2.4 
|- ( ph -> ( ( # ` A ) + 1 ) <_ ( # ` B ) )
hashf1lem1.5 
|- ( ph -> F : A -1-1-> B )
Assertion hashf1lem1 
|- ( ph -> { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } ~~ ( B \ ran F ) )

Proof

Step Hyp Ref Expression
1 hashf1lem2.1 
 |-  ( ph -> A e. Fin )
2 hashf1lem2.2 
 |-  ( ph -> B e. Fin )
3 hashf1lem2.3 
 |-  ( ph -> -. z e. A )
4 hashf1lem2.4 
 |-  ( ph -> ( ( # ` A ) + 1 ) <_ ( # ` B ) )
5 hashf1lem1.5 
 |-  ( ph -> F : A -1-1-> B )
6 f1setex 
 |-  ( B e. Fin -> { f | f : ( A u. { z } ) -1-1-> B } e. _V )
7 2 6 syl 
 |-  ( ph -> { f | f : ( A u. { z } ) -1-1-> B } e. _V )
8 abanssr 
 |-  { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } C_ { f | f : ( A u. { z } ) -1-1-> B }
9 8 a1i 
 |-  ( ph -> { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } C_ { f | f : ( A u. { z } ) -1-1-> B } )
10 7 9 ssexd 
 |-  ( ph -> { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } e. _V )
11 2 difexd 
 |-  ( ph -> ( B \ ran F ) e. _V )
12 vex 
 |-  g e. _V
13 reseq1 
 |-  ( f = g -> ( f |` A ) = ( g |` A ) )
14 13 eqeq1d 
 |-  ( f = g -> ( ( f |` A ) = F <-> ( g |` A ) = F ) )
15 f1eq1 
 |-  ( f = g -> ( f : ( A u. { z } ) -1-1-> B <-> g : ( A u. { z } ) -1-1-> B ) )
16 14 15 anbi12d 
 |-  ( f = g -> ( ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) <-> ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) )
17 12 16 elab 
 |-  ( g e. { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } <-> ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) )
18 f1f 
 |-  ( g : ( A u. { z } ) -1-1-> B -> g : ( A u. { z } ) --> B )
19 18 ad2antll 
 |-  ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> g : ( A u. { z } ) --> B )
20 ssun2 
 |-  { z } C_ ( A u. { z } )
21 vex 
 |-  z e. _V
22 21 snss 
 |-  ( z e. ( A u. { z } ) <-> { z } C_ ( A u. { z } ) )
23 20 22 mpbir 
 |-  z e. ( A u. { z } )
24 ffvelcdm 
 |-  ( ( g : ( A u. { z } ) --> B /\ z e. ( A u. { z } ) ) -> ( g ` z ) e. B )
25 19 23 24 sylancl 
 |-  ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> ( g ` z ) e. B )
26 3 adantr 
 |-  ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> -. z e. A )
27 df-ima 
 |-  ( g " A ) = ran ( g |` A )
28 simprl 
 |-  ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> ( g |` A ) = F )
29 28 rneqd 
 |-  ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> ran ( g |` A ) = ran F )
30 27 29 eqtrid 
 |-  ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> ( g " A ) = ran F )
31 30 eleq2d 
 |-  ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> ( ( g ` z ) e. ( g " A ) <-> ( g ` z ) e. ran F ) )
32 simprr 
 |-  ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> g : ( A u. { z } ) -1-1-> B )
33 23 a1i 
 |-  ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> z e. ( A u. { z } ) )
34 ssun1 
 |-  A C_ ( A u. { z } )
35 34 a1i 
 |-  ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> A C_ ( A u. { z } ) )
36 f1elima 
 |-  ( ( g : ( A u. { z } ) -1-1-> B /\ z e. ( A u. { z } ) /\ A C_ ( A u. { z } ) ) -> ( ( g ` z ) e. ( g " A ) <-> z e. A ) )
37 32 33 35 36 syl3anc 
 |-  ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> ( ( g ` z ) e. ( g " A ) <-> z e. A ) )
38 31 37 bitr3d 
 |-  ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> ( ( g ` z ) e. ran F <-> z e. A ) )
39 26 38 mtbird 
 |-  ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> -. ( g ` z ) e. ran F )
40 25 39 eldifd 
 |-  ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> ( g ` z ) e. ( B \ ran F ) )
41 40 ex 
 |-  ( ph -> ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) -> ( g ` z ) e. ( B \ ran F ) ) )
42 17 41 biimtrid 
 |-  ( ph -> ( g e. { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } -> ( g ` z ) e. ( B \ ran F ) ) )
43 f1f 
 |-  ( F : A -1-1-> B -> F : A --> B )
44 5 43 syl 
 |-  ( ph -> F : A --> B )
45 44 adantr 
 |-  ( ( ph /\ x e. ( B \ ran F ) ) -> F : A --> B )
46 vex 
 |-  x e. _V
47 21 46 f1osn 
 |-  { <. z , x >. } : { z } -1-1-onto-> { x }
48 f1of 
 |-  ( { <. z , x >. } : { z } -1-1-onto-> { x } -> { <. z , x >. } : { z } --> { x } )
49 47 48 ax-mp 
 |-  { <. z , x >. } : { z } --> { x }
50 eldifi 
 |-  ( x e. ( B \ ran F ) -> x e. B )
51 50 adantl 
 |-  ( ( ph /\ x e. ( B \ ran F ) ) -> x e. B )
52 51 snssd 
 |-  ( ( ph /\ x e. ( B \ ran F ) ) -> { x } C_ B )
53 fss 
 |-  ( ( { <. z , x >. } : { z } --> { x } /\ { x } C_ B ) -> { <. z , x >. } : { z } --> B )
54 49 52 53 sylancr 
 |-  ( ( ph /\ x e. ( B \ ran F ) ) -> { <. z , x >. } : { z } --> B )
55 res0 
 |-  ( F |` (/) ) = (/)
56 res0 
 |-  ( { <. z , x >. } |` (/) ) = (/)
57 55 56 eqtr4i 
 |-  ( F |` (/) ) = ( { <. z , x >. } |` (/) )
58 disjsn 
 |-  ( ( A i^i { z } ) = (/) <-> -. z e. A )
59 3 58 sylibr 
 |-  ( ph -> ( A i^i { z } ) = (/) )
60 59 adantr 
 |-  ( ( ph /\ x e. ( B \ ran F ) ) -> ( A i^i { z } ) = (/) )
61 60 reseq2d 
 |-  ( ( ph /\ x e. ( B \ ran F ) ) -> ( F |` ( A i^i { z } ) ) = ( F |` (/) ) )
62 60 reseq2d 
 |-  ( ( ph /\ x e. ( B \ ran F ) ) -> ( { <. z , x >. } |` ( A i^i { z } ) ) = ( { <. z , x >. } |` (/) ) )
63 57 61 62 3eqtr4a 
 |-  ( ( ph /\ x e. ( B \ ran F ) ) -> ( F |` ( A i^i { z } ) ) = ( { <. z , x >. } |` ( A i^i { z } ) ) )
64 fresaunres1 
 |-  ( ( F : A --> B /\ { <. z , x >. } : { z } --> B /\ ( F |` ( A i^i { z } ) ) = ( { <. z , x >. } |` ( A i^i { z } ) ) ) -> ( ( F u. { <. z , x >. } ) |` A ) = F )
65 45 54 63 64 syl3anc 
 |-  ( ( ph /\ x e. ( B \ ran F ) ) -> ( ( F u. { <. z , x >. } ) |` A ) = F )
66 f1f1orn 
 |-  ( F : A -1-1-> B -> F : A -1-1-onto-> ran F )
67 5 66 syl 
 |-  ( ph -> F : A -1-1-onto-> ran F )
68 67 adantr 
 |-  ( ( ph /\ x e. ( B \ ran F ) ) -> F : A -1-1-onto-> ran F )
69 47 a1i 
 |-  ( ( ph /\ x e. ( B \ ran F ) ) -> { <. z , x >. } : { z } -1-1-onto-> { x } )
70 eldifn 
 |-  ( x e. ( B \ ran F ) -> -. x e. ran F )
71 70 adantl 
 |-  ( ( ph /\ x e. ( B \ ran F ) ) -> -. x e. ran F )
72 disjsn 
 |-  ( ( ran F i^i { x } ) = (/) <-> -. x e. ran F )
73 71 72 sylibr 
 |-  ( ( ph /\ x e. ( B \ ran F ) ) -> ( ran F i^i { x } ) = (/) )
74 f1oun 
 |-  ( ( ( F : A -1-1-onto-> ran F /\ { <. z , x >. } : { z } -1-1-onto-> { x } ) /\ ( ( A i^i { z } ) = (/) /\ ( ran F i^i { x } ) = (/) ) ) -> ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-onto-> ( ran F u. { x } ) )
75 68 69 60 73 74 syl22anc 
 |-  ( ( ph /\ x e. ( B \ ran F ) ) -> ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-onto-> ( ran F u. { x } ) )
76 f1of1 
 |-  ( ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-onto-> ( ran F u. { x } ) -> ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-> ( ran F u. { x } ) )
77 75 76 syl 
 |-  ( ( ph /\ x e. ( B \ ran F ) ) -> ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-> ( ran F u. { x } ) )
78 45 frnd 
 |-  ( ( ph /\ x e. ( B \ ran F ) ) -> ran F C_ B )
79 78 52 unssd 
 |-  ( ( ph /\ x e. ( B \ ran F ) ) -> ( ran F u. { x } ) C_ B )
80 f1ss 
 |-  ( ( ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-> ( ran F u. { x } ) /\ ( ran F u. { x } ) C_ B ) -> ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-> B )
81 77 79 80 syl2anc 
 |-  ( ( ph /\ x e. ( B \ ran F ) ) -> ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-> B )
82 44 1 fexd 
 |-  ( ph -> F e. _V )
83 82 adantr 
 |-  ( ( ph /\ x e. ( B \ ran F ) ) -> F e. _V )
84 snex 
 |-  { <. z , x >. } e. _V
85 unexg 
 |-  ( ( F e. _V /\ { <. z , x >. } e. _V ) -> ( F u. { <. z , x >. } ) e. _V )
86 83 84 85 sylancl 
 |-  ( ( ph /\ x e. ( B \ ran F ) ) -> ( F u. { <. z , x >. } ) e. _V )
87 reseq1 
 |-  ( f = ( F u. { <. z , x >. } ) -> ( f |` A ) = ( ( F u. { <. z , x >. } ) |` A ) )
88 87 eqeq1d 
 |-  ( f = ( F u. { <. z , x >. } ) -> ( ( f |` A ) = F <-> ( ( F u. { <. z , x >. } ) |` A ) = F ) )
89 f1eq1 
 |-  ( f = ( F u. { <. z , x >. } ) -> ( f : ( A u. { z } ) -1-1-> B <-> ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-> B ) )
90 88 89 anbi12d 
 |-  ( f = ( F u. { <. z , x >. } ) -> ( ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) <-> ( ( ( F u. { <. z , x >. } ) |` A ) = F /\ ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-> B ) ) )
91 90 elabg 
 |-  ( ( F u. { <. z , x >. } ) e. _V -> ( ( F u. { <. z , x >. } ) e. { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } <-> ( ( ( F u. { <. z , x >. } ) |` A ) = F /\ ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-> B ) ) )
92 86 91 syl 
 |-  ( ( ph /\ x e. ( B \ ran F ) ) -> ( ( F u. { <. z , x >. } ) e. { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } <-> ( ( ( F u. { <. z , x >. } ) |` A ) = F /\ ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-> B ) ) )
93 65 81 92 mpbir2and 
 |-  ( ( ph /\ x e. ( B \ ran F ) ) -> ( F u. { <. z , x >. } ) e. { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } )
94 93 ex 
 |-  ( ph -> ( x e. ( B \ ran F ) -> ( F u. { <. z , x >. } ) e. { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } ) )
95 17 anbi1i 
 |-  ( ( g e. { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } /\ x e. ( B \ ran F ) ) <-> ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) )
96 simprlr 
 |-  ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> g : ( A u. { z } ) -1-1-> B )
97 f1fn 
 |-  ( g : ( A u. { z } ) -1-1-> B -> g Fn ( A u. { z } ) )
98 96 97 syl 
 |-  ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> g Fn ( A u. { z } ) )
99 75 adantrl 
 |-  ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-onto-> ( ran F u. { x } ) )
100 f1ofn 
 |-  ( ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-onto-> ( ran F u. { x } ) -> ( F u. { <. z , x >. } ) Fn ( A u. { z } ) )
101 99 100 syl 
 |-  ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> ( F u. { <. z , x >. } ) Fn ( A u. { z } ) )
102 eqfnfv 
 |-  ( ( g Fn ( A u. { z } ) /\ ( F u. { <. z , x >. } ) Fn ( A u. { z } ) ) -> ( g = ( F u. { <. z , x >. } ) <-> A. y e. ( A u. { z } ) ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) ) )
103 98 101 102 syl2anc 
 |-  ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> ( g = ( F u. { <. z , x >. } ) <-> A. y e. ( A u. { z } ) ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) ) )
104 fvres 
 |-  ( y e. A -> ( ( g |` A ) ` y ) = ( g ` y ) )
105 104 eqcomd 
 |-  ( y e. A -> ( g ` y ) = ( ( g |` A ) ` y ) )
106 simprll 
 |-  ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> ( g |` A ) = F )
107 106 fveq1d 
 |-  ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> ( ( g |` A ) ` y ) = ( F ` y ) )
108 105 107 sylan9eqr 
 |-  ( ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) /\ y e. A ) -> ( g ` y ) = ( F ` y ) )
109 5 ad2antrr 
 |-  ( ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) /\ y e. A ) -> F : A -1-1-> B )
110 f1fn 
 |-  ( F : A -1-1-> B -> F Fn A )
111 109 110 syl 
 |-  ( ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) /\ y e. A ) -> F Fn A )
112 21 46 fnsn 
 |-  { <. z , x >. } Fn { z }
113 112 a1i 
 |-  ( ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) /\ y e. A ) -> { <. z , x >. } Fn { z } )
114 59 ad2antrr 
 |-  ( ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) /\ y e. A ) -> ( A i^i { z } ) = (/) )
115 simpr 
 |-  ( ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) /\ y e. A ) -> y e. A )
116 111 113 114 115 fvun1d 
 |-  ( ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) /\ y e. A ) -> ( ( F u. { <. z , x >. } ) ` y ) = ( F ` y ) )
117 108 116 eqtr4d 
 |-  ( ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) /\ y e. A ) -> ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) )
118 117 ralrimiva 
 |-  ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> A. y e. A ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) )
119 118 biantrurd 
 |-  ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> ( A. y e. { z } ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) <-> ( A. y e. A ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) /\ A. y e. { z } ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) ) ) )
120 ralunb 
 |-  ( A. y e. ( A u. { z } ) ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) <-> ( A. y e. A ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) /\ A. y e. { z } ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) ) )
121 119 120 bitr4di 
 |-  ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> ( A. y e. { z } ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) <-> A. y e. ( A u. { z } ) ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) ) )
122 44 fdmd 
 |-  ( ph -> dom F = A )
123 122 eleq2d 
 |-  ( ph -> ( z e. dom F <-> z e. A ) )
124 3 123 mtbird 
 |-  ( ph -> -. z e. dom F )
125 124 adantr 
 |-  ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> -. z e. dom F )
126 fsnunfv 
 |-  ( ( z e. _V /\ x e. _V /\ -. z e. dom F ) -> ( ( F u. { <. z , x >. } ) ` z ) = x )
127 21 46 125 126 mp3an12i 
 |-  ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> ( ( F u. { <. z , x >. } ) ` z ) = x )
128 127 eqeq2d 
 |-  ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> ( ( g ` z ) = ( ( F u. { <. z , x >. } ) ` z ) <-> ( g ` z ) = x ) )
129 fveq2 
 |-  ( y = z -> ( g ` y ) = ( g ` z ) )
130 fveq2 
 |-  ( y = z -> ( ( F u. { <. z , x >. } ) ` y ) = ( ( F u. { <. z , x >. } ) ` z ) )
131 129 130 eqeq12d 
 |-  ( y = z -> ( ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) <-> ( g ` z ) = ( ( F u. { <. z , x >. } ) ` z ) ) )
132 21 131 ralsn 
 |-  ( A. y e. { z } ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) <-> ( g ` z ) = ( ( F u. { <. z , x >. } ) ` z ) )
133 eqcom 
 |-  ( x = ( g ` z ) <-> ( g ` z ) = x )
134 128 132 133 3bitr4g 
 |-  ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> ( A. y e. { z } ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) <-> x = ( g ` z ) ) )
135 103 121 134 3bitr2d 
 |-  ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> ( g = ( F u. { <. z , x >. } ) <-> x = ( g ` z ) ) )
136 135 ex 
 |-  ( ph -> ( ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) -> ( g = ( F u. { <. z , x >. } ) <-> x = ( g ` z ) ) ) )
137 95 136 biimtrid 
 |-  ( ph -> ( ( g e. { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } /\ x e. ( B \ ran F ) ) -> ( g = ( F u. { <. z , x >. } ) <-> x = ( g ` z ) ) ) )
138 10 11 42 94 137 en3d 
 |-  ( ph -> { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } ~~ ( B \ ran F ) )