Metamath Proof Explorer

Theorem tposf1o2

Description: Condition of a bijective transposition. (Contributed by NM, 10-Sep-2015)

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

Proof

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