Metamath Proof Explorer


Theorem dftpos2

Description: Alternate definition of tpos when F has relational domain. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion dftpos2 Rel dom F tpos F = F x dom F -1 x -1

Proof

Step Hyp Ref Expression
1 dmtpos Rel dom F dom tpos F = dom F -1
2 1 reseq2d Rel dom F tpos F dom tpos F = tpos F dom F -1
3 reltpos Rel tpos F
4 resdm Rel tpos F tpos F dom tpos F = tpos F
5 3 4 ax-mp tpos F dom tpos F = tpos F
6 df-tpos tpos F = F x dom F -1 x -1
7 6 reseq1i tpos F dom F -1 = F x dom F -1 x -1 dom F -1
8 resco F x dom F -1 x -1 dom F -1 = F x dom F -1 x -1 dom F -1
9 ssun1 dom F -1 dom F -1
10 resmpt dom F -1 dom F -1 x dom F -1 x -1 dom F -1 = x dom F -1 x -1
11 9 10 ax-mp x dom F -1 x -1 dom F -1 = x dom F -1 x -1
12 11 coeq2i F x dom F -1 x -1 dom F -1 = F x dom F -1 x -1
13 7 8 12 3eqtri tpos F dom F -1 = F x dom F -1 x -1
14 2 5 13 3eqtr3g Rel dom F tpos F = F x dom F -1 x -1