Step |
Hyp |
Ref |
Expression |
1 |
|
tposfo2 |
|- ( Rel A -> ( F : A -onto-> ran F -> tpos F : `' A -onto-> ran F ) ) |
2 |
|
ffn |
|- ( F : A --> B -> F Fn A ) |
3 |
|
dffn4 |
|- ( F Fn A <-> F : A -onto-> ran F ) |
4 |
2 3
|
sylib |
|- ( F : A --> B -> F : A -onto-> ran F ) |
5 |
1 4
|
impel |
|- ( ( Rel A /\ F : A --> B ) -> tpos F : `' A -onto-> ran F ) |
6 |
|
fof |
|- ( tpos F : `' A -onto-> ran F -> tpos F : `' A --> ran F ) |
7 |
5 6
|
syl |
|- ( ( Rel A /\ F : A --> B ) -> tpos F : `' A --> ran F ) |
8 |
|
frn |
|- ( F : A --> B -> ran F C_ B ) |
9 |
8
|
adantl |
|- ( ( Rel A /\ F : A --> B ) -> ran F C_ B ) |
10 |
7 9
|
fssd |
|- ( ( Rel A /\ F : A --> B ) -> tpos F : `' A --> B ) |
11 |
10
|
ex |
|- ( Rel A -> ( F : A --> B -> tpos F : `' A --> B ) ) |