Metamath Proof Explorer


Theorem tpostpos

Description: Value of the double transposition for a general class F . (Contributed by Mario Carneiro, 16-Sep-2015)

Ref Expression
Assertion tpostpos tpos tpos F = F V × V × V

Proof

Step Hyp Ref Expression
1 reltpos Rel tpos tpos F
2 relinxp Rel F V × V × V
3 relcnv Rel dom tpos F -1
4 df-rel Rel dom tpos F -1 dom tpos F -1 V × V
5 3 4 mpbi dom tpos F -1 V × V
6 simpl w dom tpos F -1 w -1 tpos F z w dom tpos F -1
7 5 6 sselid w dom tpos F -1 w -1 tpos F z w V × V
8 simpr w F z w V × V w V × V
9 elvv w V × V x y w = x y
10 eleq1 w = x y w dom tpos F -1 x y dom tpos F -1
11 vex x V
12 vex y V
13 11 12 opelcnv x y dom tpos F -1 y x dom tpos F
14 10 13 bitrdi w = x y w dom tpos F -1 y x dom tpos F
15 sneq w = x y w = x y
16 15 cnveqd w = x y w -1 = x y -1
17 16 unieqd w = x y w -1 = x y -1
18 opswap x y -1 = y x
19 17 18 eqtrdi w = x y w -1 = y x
20 19 breq1d w = x y w -1 tpos F z y x tpos F z
21 14 20 anbi12d w = x y w dom tpos F -1 w -1 tpos F z y x dom tpos F y x tpos F z
22 opex y x V
23 vex z V
24 22 23 breldm y x tpos F z y x dom tpos F
25 24 pm4.71ri y x tpos F z y x dom tpos F y x tpos F z
26 brtpos z V y x tpos F z x y F z
27 26 elv y x tpos F z x y F z
28 25 27 bitr3i y x dom tpos F y x tpos F z x y F z
29 21 28 bitrdi w = x y w dom tpos F -1 w -1 tpos F z x y F z
30 breq1 w = x y w F z x y F z
31 29 30 bitr4d w = x y w dom tpos F -1 w -1 tpos F z w F z
32 31 exlimivv x y w = x y w dom tpos F -1 w -1 tpos F z w F z
33 9 32 sylbi w V × V w dom tpos F -1 w -1 tpos F z w F z
34 iba w V × V w F z w F z w V × V
35 33 34 bitrd w V × V w dom tpos F -1 w -1 tpos F z w F z w V × V
36 7 8 35 pm5.21nii w dom tpos F -1 w -1 tpos F z w F z w V × V
37 elsni w w =
38 37 sneqd w w =
39 38 cnveqd w w -1 = -1
40 cnvsn0 -1 =
41 39 40 eqtrdi w w -1 =
42 41 unieqd w w -1 =
43 uni0 =
44 42 43 eqtrdi w w -1 =
45 44 breq1d w w -1 tpos F z tpos F z
46 brtpos0 z V tpos F z F z
47 46 elv tpos F z F z
48 45 47 bitrdi w w -1 tpos F z F z
49 37 breq1d w w F z F z
50 48 49 bitr4d w w -1 tpos F z w F z
51 50 pm5.32i w w -1 tpos F z w w F z
52 51 biancomi w w -1 tpos F z w F z w
53 36 52 orbi12i w dom tpos F -1 w -1 tpos F z w w -1 tpos F z w F z w V × V w F z w
54 andir w dom tpos F -1 w w -1 tpos F z w dom tpos F -1 w -1 tpos F z w w -1 tpos F z
55 andi w F z w V × V w w F z w V × V w F z w
56 53 54 55 3bitr4i w dom tpos F -1 w w -1 tpos F z w F z w V × V w
57 elun w dom tpos F -1 w dom tpos F -1 w
58 57 anbi1i w dom tpos F -1 w -1 tpos F z w dom tpos F -1 w w -1 tpos F z
59 brxp w V × V × V z w V × V z V
60 23 59 mpbiran2 w V × V × V z w V × V
61 elun w V × V w V × V w
62 60 61 bitri w V × V × V z w V × V w
63 62 anbi2i w F z w V × V × V z w F z w V × V w
64 56 58 63 3bitr4i w dom tpos F -1 w -1 tpos F z w F z w V × V × V z
65 brtpos2 z V w tpos tpos F z w dom tpos F -1 w -1 tpos F z
66 65 elv w tpos tpos F z w dom tpos F -1 w -1 tpos F z
67 brin w F V × V × V z w F z w V × V × V z
68 64 66 67 3bitr4i w tpos tpos F z w F V × V × V z
69 1 2 68 eqbrriv tpos tpos F = F V × V × V