Metamath Proof Explorer


Theorem tposf2

Description: The domain and range of a transposition. (Contributed by NM, 10-Sep-2015)

Ref Expression
Assertion tposf2
|- ( Rel A -> ( F : A --> B -> tpos F : `' A --> B ) )

Proof

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