Metamath Proof Explorer


Theorem dftpos3

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

Ref Expression
Assertion dftpos3 Rel dom F tpos F = x y z | y x F z

Proof

Step Hyp Ref Expression
1 relcnv Rel dom F -1
2 dmtpos Rel dom F dom tpos F = dom F -1
3 2 releqd Rel dom F Rel dom tpos F Rel dom F -1
4 1 3 mpbiri Rel dom F Rel dom tpos F
5 reltpos Rel tpos F
6 4 5 jctil Rel dom F Rel tpos F Rel dom tpos F
7 relrelss Rel tpos F Rel dom tpos F tpos F V × V × V
8 6 7 sylib Rel dom F tpos F V × V × V
9 8 sseld Rel dom F w tpos F w V × V × V
10 elvvv w V × V × V x y z w = x y z
11 9 10 syl6ib Rel dom F w tpos F x y z w = x y z
12 11 pm4.71rd Rel dom F w tpos F x y z w = x y z w tpos F
13 19.41vvv x y z w = x y z w tpos F x y z w = x y z w tpos F
14 eleq1 w = x y z w tpos F x y z tpos F
15 df-br x y tpos F z x y z tpos F
16 brtpos z V x y tpos F z y x F z
17 16 elv x y tpos F z y x F z
18 15 17 bitr3i x y z tpos F y x F z
19 14 18 bitrdi w = x y z w tpos F y x F z
20 19 pm5.32i w = x y z w tpos F w = x y z y x F z
21 20 3exbii x y z w = x y z w tpos F x y z w = x y z y x F z
22 13 21 bitr3i x y z w = x y z w tpos F x y z w = x y z y x F z
23 12 22 bitrdi Rel dom F w tpos F x y z w = x y z y x F z
24 23 abbi2dv Rel dom F tpos F = w | x y z w = x y z y x F z
25 df-oprab x y z | y x F z = w | x y z w = x y z y x F z
26 24 25 eqtr4di Rel dom F tpos F = x y z | y x F z