Metamath Proof Explorer


Theorem tpostpos2

Description: Value of the double transposition for a relation on triples. (Contributed by Mario Carneiro, 16-Sep-2015)

Ref Expression
Assertion tpostpos2 Rel F Rel dom F tpos tpos F = F

Proof

Step Hyp Ref Expression
1 tpostpos tpos tpos F = F V × V × V
2 relrelss Rel F Rel dom F F V × V × V
3 ssun1 V × V V × V
4 xpss1 V × V V × V V × V × V V × V × V
5 3 4 ax-mp V × V × V V × V × V
6 sstr F V × V × V V × V × V V × V × V F V × V × V
7 5 6 mpan2 F V × V × V F V × V × V
8 2 7 sylbi Rel F Rel dom F F V × V × V
9 df-ss F V × V × V F V × V × V = F
10 8 9 sylib Rel F Rel dom F F V × V × V = F
11 1 10 eqtrid Rel F Rel dom F tpos tpos F = F