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 ) ) |