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