Theorem tposco

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

	Ref	Expression
Assertion	tposco	⊢ tpos ( 𝐹 ∘ 𝐺 ) = ( 𝐹 ∘ tpos 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		coass	⊢ ( ( 𝐹 ∘ 𝐺 ) ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) = ( 𝐹 ∘ ( 𝐺 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) )
2		dftpos4	⊢ tpos ( 𝐹 ∘ 𝐺 ) = ( ( 𝐹 ∘ 𝐺 ) ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )
3		dftpos4	⊢ tpos 𝐺 = ( 𝐺 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )
4	3	coeq2i	⊢ ( 𝐹 ∘ tpos 𝐺 ) = ( 𝐹 ∘ ( 𝐺 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) )
5	1 2 4	3eqtr4i	⊢ tpos ( 𝐹 ∘ 𝐺 ) = ( 𝐹 ∘ tpos 𝐺 )