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 ffvelrn
 |-  ( ( 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 syl5bi
 |-  ( 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 syl5bi
 |-  ( 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 ) )