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

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 -1
4 3 a1i dom F = A Rel dom F dom tpos F = dom F -1
5 releq dom F = A Rel dom F Rel A
6 cnveq dom F = A dom F -1 = A -1
7 6 eqeq2d dom F = A dom tpos F = dom F -1 dom tpos F = A -1
8 4 5 7 3imtr3d dom F = A Rel A dom tpos F = A -1
9 8 com12 Rel A dom F = A dom tpos F = A -1
10 2 9 anim12d Rel A Fun F dom F = A Fun tpos F dom tpos F = A -1
11 df-fn F Fn A Fun F dom F = A
12 df-fn tpos F Fn A -1 Fun tpos F dom tpos F = A -1
13 10 11 12 3imtr4g Rel A F Fn A tpos F Fn A -1