This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 dfss2 ⊢ ( 𝐹 ⊆ ( ( ( 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 𝐹 = 𝐹 )