Step |
Hyp |
Ref |
Expression |
1 |
|
ffrn |
|- ( F : A --> B -> F : A --> ran F ) |
2 |
|
f2ndf |
|- ( F : A --> ran F -> ( 2nd |` F ) : F --> ran F ) |
3 |
1 2
|
syl |
|- ( F : A --> B -> ( 2nd |` F ) : F --> ran F ) |
4 |
|
ffn |
|- ( F : A --> B -> F Fn A ) |
5 |
|
dffn3 |
|- ( F Fn A <-> F : A --> ran F ) |
6 |
5 2
|
sylbi |
|- ( F Fn A -> ( 2nd |` F ) : F --> ran F ) |
7 |
4 6
|
syl |
|- ( F : A --> B -> ( 2nd |` F ) : F --> ran F ) |
8 |
7
|
frnd |
|- ( F : A --> B -> ran ( 2nd |` F ) C_ ran F ) |
9 |
|
elrn2g |
|- ( y e. ran F -> ( y e. ran F <-> E. x <. x , y >. e. F ) ) |
10 |
9
|
ibi |
|- ( y e. ran F -> E. x <. x , y >. e. F ) |
11 |
|
fvres |
|- ( <. x , y >. e. F -> ( ( 2nd |` F ) ` <. x , y >. ) = ( 2nd ` <. x , y >. ) ) |
12 |
11
|
adantl |
|- ( ( F : A --> B /\ <. x , y >. e. F ) -> ( ( 2nd |` F ) ` <. x , y >. ) = ( 2nd ` <. x , y >. ) ) |
13 |
|
vex |
|- x e. _V |
14 |
|
vex |
|- y e. _V |
15 |
13 14
|
op2nd |
|- ( 2nd ` <. x , y >. ) = y |
16 |
12 15
|
eqtr2di |
|- ( ( F : A --> B /\ <. x , y >. e. F ) -> y = ( ( 2nd |` F ) ` <. x , y >. ) ) |
17 |
|
f2ndf |
|- ( F : A --> B -> ( 2nd |` F ) : F --> B ) |
18 |
17
|
ffnd |
|- ( F : A --> B -> ( 2nd |` F ) Fn F ) |
19 |
|
fnfvelrn |
|- ( ( ( 2nd |` F ) Fn F /\ <. x , y >. e. F ) -> ( ( 2nd |` F ) ` <. x , y >. ) e. ran ( 2nd |` F ) ) |
20 |
18 19
|
sylan |
|- ( ( F : A --> B /\ <. x , y >. e. F ) -> ( ( 2nd |` F ) ` <. x , y >. ) e. ran ( 2nd |` F ) ) |
21 |
16 20
|
eqeltrd |
|- ( ( F : A --> B /\ <. x , y >. e. F ) -> y e. ran ( 2nd |` F ) ) |
22 |
21
|
ex |
|- ( F : A --> B -> ( <. x , y >. e. F -> y e. ran ( 2nd |` F ) ) ) |
23 |
22
|
exlimdv |
|- ( F : A --> B -> ( E. x <. x , y >. e. F -> y e. ran ( 2nd |` F ) ) ) |
24 |
10 23
|
syl5 |
|- ( F : A --> B -> ( y e. ran F -> y e. ran ( 2nd |` F ) ) ) |
25 |
24
|
ssrdv |
|- ( F : A --> B -> ran F C_ ran ( 2nd |` F ) ) |
26 |
8 25
|
eqssd |
|- ( F : A --> B -> ran ( 2nd |` F ) = ran F ) |
27 |
|
dffo2 |
|- ( ( 2nd |` F ) : F -onto-> ran F <-> ( ( 2nd |` F ) : F --> ran F /\ ran ( 2nd |` F ) = ran F ) ) |
28 |
3 26 27
|
sylanbrc |
|- ( F : A --> B -> ( 2nd |` F ) : F -onto-> ran F ) |