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

Metamath Proof Explorer

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 )