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