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