Metamath Proof Explorer

Theorem tposfo2

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

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

Proof

Step Hyp Ref Expression
1 tposfn2 
 |-  ( Rel A -> ( F Fn A -> tpos F Fn `' A ) )
2 1 adantrd 
 |-  ( Rel A -> ( ( F Fn A /\ ran F = B ) -> tpos F Fn `' A ) )
3 fndm 
 |-  ( F Fn A -> dom F = A )
4 3 releqd 
 |-  ( F Fn A -> ( Rel dom F <-> Rel A ) )
5 4 biimparc 
 |-  ( ( Rel A /\ F Fn A ) -> Rel dom F )
6 rntpos 
 |-  ( Rel dom F -> ran tpos F = ran F )
7 5 6 syl 
 |-  ( ( Rel A /\ F Fn A ) -> ran tpos F = ran F )
8 7 eqeq1d 
 |-  ( ( Rel A /\ F Fn A ) -> ( ran tpos F = B <-> ran F = B ) )
9 8 biimprd 
 |-  ( ( Rel A /\ F Fn A ) -> ( ran F = B -> ran tpos F = B ) )
10 9 expimpd 
 |-  ( Rel A -> ( ( F Fn A /\ ran F = B ) -> ran tpos F = B ) )
11 2 10 jcad 
 |-  ( Rel A -> ( ( F Fn A /\ ran F = B ) -> ( tpos F Fn `' A /\ ran tpos F = B ) ) )
12 df-fo 
 |-  ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
13 df-fo 
 |-  ( tpos F : `' A -onto-> B <-> ( tpos F Fn `' A /\ ran tpos F = B ) )
14 11 12 13 3imtr4g 
 |-  ( Rel A -> ( F : A -onto-> B -> tpos F : `' A -onto-> B ) )