Metamath Proof Explorer

Theorem hashf1lem1OLD

Description: Obsolete version of hashf1lem1 as of 7-Aug-2024. (Contributed by Mario Carneiro, 17-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

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