Metamath Proof Explorer

Theorem tposf2

Description: The domain and codomain 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 ) )