Metamath Proof Explorer


Theorem tposfn2

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

Ref Expression
Assertion tposfn2
|- ( Rel A -> ( F Fn A -> tpos F Fn `' A ) )

Proof

Step Hyp Ref Expression
1 tposfun
 |-  ( Fun F -> Fun tpos F )
2 1 a1i
 |-  ( Rel A -> ( Fun F -> Fun tpos F ) )
3 dmtpos
 |-  ( Rel dom F -> dom tpos F = `' dom F )
4 3 a1i
 |-  ( dom F = A -> ( Rel dom F -> dom tpos F = `' dom F ) )
5 releq
 |-  ( dom F = A -> ( Rel dom F <-> Rel A ) )
6 cnveq
 |-  ( dom F = A -> `' dom F = `' A )
7 6 eqeq2d
 |-  ( dom F = A -> ( dom tpos F = `' dom F <-> dom tpos F = `' A ) )
8 4 5 7 3imtr3d
 |-  ( dom F = A -> ( Rel A -> dom tpos F = `' A ) )
9 8 com12
 |-  ( Rel A -> ( dom F = A -> dom tpos F = `' A ) )
10 2 9 anim12d
 |-  ( Rel A -> ( ( Fun F /\ dom F = A ) -> ( Fun tpos F /\ dom tpos F = `' A ) ) )
11 df-fn
 |-  ( F Fn A <-> ( Fun F /\ dom F = A ) )
12 df-fn
 |-  ( tpos F Fn `' A <-> ( Fun tpos F /\ dom tpos F = `' A ) )
13 10 11 12 3imtr4g
 |-  ( Rel A -> ( F Fn A -> tpos F Fn `' A ) )