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 𝐹 ∧ Rel dom 𝐹 ) → tpos tpos 𝐹 = 𝐹 )

Proof

Step Hyp Ref Expression
1 tpostpos tpos tpos 𝐹 = ( 𝐹 ∩ ( ( ( V × V ) ∪ { ∅ } ) × V ) )
2 relrelss ( ( Rel 𝐹 ∧ Rel dom 𝐹 ) ↔ 𝐹 ⊆ ( ( 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 ( ( 𝐹 ⊆ ( ( V × V ) × V ) ∧ ( ( V × V ) × V ) ⊆ ( ( ( V × V ) ∪ { ∅ } ) × V ) ) → 𝐹 ⊆ ( ( ( V × V ) ∪ { ∅ } ) × V ) )
7 5 6 mpan2 ( 𝐹 ⊆ ( ( V × V ) × V ) → 𝐹 ⊆ ( ( ( V × V ) ∪ { ∅ } ) × V ) )
8 2 7 sylbi ( ( Rel 𝐹 ∧ Rel dom 𝐹 ) → 𝐹 ⊆ ( ( ( V × V ) ∪ { ∅ } ) × V ) )
9 df-ss ( 𝐹 ⊆ ( ( ( V × V ) ∪ { ∅ } ) × V ) ↔ ( 𝐹 ∩ ( ( ( V × V ) ∪ { ∅ } ) × V ) ) = 𝐹 )
10 8 9 sylib ( ( Rel 𝐹 ∧ Rel dom 𝐹 ) → ( 𝐹 ∩ ( ( ( V × V ) ∪ { ∅ } ) × V ) ) = 𝐹 )
11 1 10 eqtrid ( ( Rel 𝐹 ∧ Rel dom 𝐹 ) → tpos tpos 𝐹 = 𝐹 )