tposco

Description: Transposition of a composition. (Contributed by Mario Carneiro, 4-Oct-2015)

		Ref	Expression
	Assertion	tposco	$⊢ tpos (F \circ G) = F \circ tpos G$

Step	Hyp	Ref	Expression
1		coass	$⊢ (F \circ G) \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}) = F \circ (G \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}))$
2		dftpos4	$⊢ tpos (F \circ G) = (F \circ G) \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
3		dftpos4	$⊢ tpos G = G \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
4	3	coeq2i	$⊢ F \circ tpos G = F \circ (G \circ (x \in ((V \times V) \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}))$
5	1 2 4	3eqtr4i	$⊢ tpos (F \circ G) = F \circ tpos G$

Metamath Proof Explorer