Step |
Hyp |
Ref |
Expression |
1 |
|
tposf12 |
|- ( Rel A -> ( F : A -1-1-> B -> tpos F : `' A -1-1-> B ) ) |
2 |
|
tposfo2 |
|- ( Rel A -> ( F : A -onto-> B -> tpos F : `' A -onto-> B ) ) |
3 |
1 2
|
anim12d |
|- ( Rel A -> ( ( F : A -1-1-> B /\ F : A -onto-> B ) -> ( tpos F : `' A -1-1-> B /\ tpos F : `' A -onto-> B ) ) ) |
4 |
|
df-f1o |
|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) ) |
5 |
|
df-f1o |
|- ( tpos F : `' A -1-1-onto-> B <-> ( tpos F : `' A -1-1-> B /\ tpos F : `' A -onto-> B ) ) |
6 |
3 4 5
|
3imtr4g |
|- ( Rel A -> ( F : A -1-1-onto-> B -> tpos F : `' A -1-1-onto-> B ) ) |