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 \land Rel dom F) \to tpos tpos F = F$

Step	Hyp	Ref	Expression
1		tpostpos	$⊢ tpos tpos F = F \cap (((V \times V) \cup \{\emptyset\}) \times V)$
2		relrelss	$⊢ (Rel F \land Rel dom F) \leftrightarrow F \subseteq (V \times V) \times V$
3		ssun1	$⊢ V \times V \subseteq (V \times V) \cup \{\emptyset\}$
4		xpss1	$⊢ V \times V \subseteq (V \times V) \cup \{\emptyset\} \to (V \times V) \times V \subseteq ((V \times V) \cup \{\emptyset\}) \times V$
5	3 4	ax-mp	$⊢ (V \times V) \times V \subseteq ((V \times V) \cup \{\emptyset\}) \times V$
6		sstr	$⊢ (F \subseteq (V \times V) \times V \land (V \times V) \times V \subseteq ((V \times V) \cup \{\emptyset\}) \times V) \to F \subseteq ((V \times V) \cup \{\emptyset\}) \times V$
7	5 6	mpan2	$⊢ F \subseteq (V \times V) \times V \to F \subseteq ((V \times V) \cup \{\emptyset\}) \times V$
8	2 7	sylbi	$⊢ (Rel F \land Rel dom F) \to F \subseteq ((V \times V) \cup \{\emptyset\}) \times V$
9		df-ss	$⊢ F \subseteq ((V \times V) \cup \{\emptyset\}) \times V \leftrightarrow F \cap (((V \times V) \cup \{\emptyset\}) \times V) = F$
10	8 9	sylib	$⊢ (Rel F \land Rel dom F) \to F \cap (((V \times V) \cup \{\emptyset\}) \times V) = F$
11	1 10	syl5eq	$⊢ (Rel F \land Rel dom F) \to tpos tpos F = F$

Metamath Proof Explorer