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 i^i ( ( ( _V X. _V ) u. { (/) } ) X. _V ) )
2 relrelss 
 |-  ( ( Rel F /\ Rel dom F ) <-> F C_ ( ( _V X. _V ) X. _V ) )
3 ssun1 
 |-  ( _V X. _V ) C_ ( ( _V X. _V ) u. { (/) } )
4 xpss1 
 |-  ( ( _V X. _V ) C_ ( ( _V X. _V ) u. { (/) } ) -> ( ( _V X. _V ) X. _V ) C_ ( ( ( _V X. _V ) u. { (/) } ) X. _V ) )
5 3 4 ax-mp 
 |-  ( ( _V X. _V ) X. _V ) C_ ( ( ( _V X. _V ) u. { (/) } ) X. _V )
6 sstr 
 |-  ( ( F C_ ( ( _V X. _V ) X. _V ) /\ ( ( _V X. _V ) X. _V ) C_ ( ( ( _V X. _V ) u. { (/) } ) X. _V ) ) -> F C_ ( ( ( _V X. _V ) u. { (/) } ) X. _V ) )
7 5 6 mpan2 
 |-  ( F C_ ( ( _V X. _V ) X. _V ) -> F C_ ( ( ( _V X. _V ) u. { (/) } ) X. _V ) )
8 2 7 sylbi 
 |-  ( ( Rel F /\ Rel dom F ) -> F C_ ( ( ( _V X. _V ) u. { (/) } ) X. _V ) )
9 dfss2 
 |-  ( F C_ ( ( ( _V X. _V ) u. { (/) } ) X. _V ) <-> ( F i^i ( ( ( _V X. _V ) u. { (/) } ) X. _V ) ) = F )
10 8 9 sylib 
 |-  ( ( Rel F /\ Rel dom F ) -> ( F i^i ( ( ( _V X. _V ) u. { (/) } ) X. _V ) ) = F )
11 1 10 eqtrid 
 |-  ( ( Rel F /\ Rel dom F ) -> tpos tpos F = F )