Metamath Proof Explorer


Theorem dftpos4

Description: Alternate definition of tpos . (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Assertion dftpos4 tpos F = F x V × V x -1

Proof

Step Hyp Ref Expression
1 df-tpos tpos F = F x dom F -1 x -1
2 relcnv Rel dom F -1
3 df-rel Rel dom F -1 dom F -1 V × V
4 2 3 mpbi dom F -1 V × V
5 unss1 dom F -1 V × V dom F -1 V × V
6 resmpt dom F -1 V × V x V × V x -1 dom F -1 = x dom F -1 x -1
7 4 5 6 mp2b x V × V x -1 dom F -1 = x dom F -1 x -1
8 resss x V × V x -1 dom F -1 x V × V x -1
9 7 8 eqsstrri x dom F -1 x -1 x V × V x -1
10 coss2 x dom F -1 x -1 x V × V x -1 F x dom F -1 x -1 F x V × V x -1
11 9 10 ax-mp F x dom F -1 x -1 F x V × V x -1
12 1 11 eqsstri tpos F F x V × V x -1
13 relco Rel F x V × V x -1
14 vex y V
15 vex z V
16 14 15 opelco y z F x V × V x -1 w y x V × V x -1 w w F z
17 vex w V
18 eleq1 x = y x V × V y V × V
19 sneq x = y x = y
20 19 cnveqd x = y x -1 = y -1
21 20 unieqd x = y x -1 = y -1
22 21 eqeq2d x = y z = x -1 z = y -1
23 18 22 anbi12d x = y x V × V z = x -1 y V × V z = y -1
24 eqeq1 z = w z = y -1 w = y -1
25 24 anbi2d z = w y V × V z = y -1 y V × V w = y -1
26 df-mpt x V × V x -1 = x z | x V × V z = x -1
27 14 17 23 25 26 brab y x V × V x -1 w y V × V w = y -1
28 simplr y V × V w = y -1 w F z w = y -1
29 17 15 breldm w F z w dom F
30 29 adantl y V × V w = y -1 w F z w dom F
31 28 30 eqeltrrd y V × V w = y -1 w F z y -1 dom F
32 elvv y V × V z w y = z w
33 opswap z w -1 = w z
34 33 eleq1i z w -1 dom F w z dom F
35 15 17 opelcnv z w dom F -1 w z dom F
36 34 35 bitr4i z w -1 dom F z w dom F -1
37 sneq y = z w y = z w
38 37 cnveqd y = z w y -1 = z w -1
39 38 unieqd y = z w y -1 = z w -1
40 39 eleq1d y = z w y -1 dom F z w -1 dom F
41 eleq1 y = z w y dom F -1 z w dom F -1
42 40 41 bibi12d y = z w y -1 dom F y dom F -1 z w -1 dom F z w dom F -1
43 36 42 mpbiri y = z w y -1 dom F y dom F -1
44 43 exlimivv z w y = z w y -1 dom F y dom F -1
45 32 44 sylbi y V × V y -1 dom F y dom F -1
46 45 biimpcd y -1 dom F y V × V y dom F -1
47 elun1 y dom F -1 y dom F -1
48 46 47 syl6 y -1 dom F y V × V y dom F -1
49 31 48 syl y V × V w = y -1 w F z y V × V y dom F -1
50 elun2 y y dom F -1
51 50 a1i y V × V w = y -1 w F z y y dom F -1
52 simpll y V × V w = y -1 w F z y V × V
53 elun y V × V y V × V y
54 52 53 sylib y V × V w = y -1 w F z y V × V y
55 49 51 54 mpjaod y V × V w = y -1 w F z y dom F -1
56 simpr y V × V w = y -1 w F z w F z
57 28 56 eqbrtrrd y V × V w = y -1 w F z y -1 F z
58 55 57 jca y V × V w = y -1 w F z y dom F -1 y -1 F z
59 27 58 sylanb y x V × V x -1 w w F z y dom F -1 y -1 F z
60 brtpos2 z V y tpos F z y dom F -1 y -1 F z
61 15 60 ax-mp y tpos F z y dom F -1 y -1 F z
62 59 61 sylibr y x V × V x -1 w w F z y tpos F z
63 df-br y tpos F z y z tpos F
64 62 63 sylib y x V × V x -1 w w F z y z tpos F
65 64 exlimiv w y x V × V x -1 w w F z y z tpos F
66 16 65 sylbi y z F x V × V x -1 y z tpos F
67 13 66 relssi F x V × V x -1 tpos F
68 12 67 eqssi tpos F = F x V × V x -1