Theorem tposco

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

	Ref	Expression
Assertion	tposco	|- tpos ( F o. G ) = ( F o. tpos G )

Proof

Step	Hyp	Ref	Expression
1		coass	|- ( ( F o. G ) o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) = ( F o. ( G o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) )
2		dftpos4	|- tpos ( F o. G ) = ( ( F o. G ) o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) )
3		dftpos4	|- tpos G = ( G o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) )
4	3	coeq2i	|- ( F o. tpos G ) = ( F o. ( G o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) )
5	1 2 4	3eqtr4i	|- tpos ( F o. G ) = ( F o. tpos G )