Theorem tposconst

Description: The transposition of a constant operation using the relation representation. (Contributed by SO, 11-Jul-2018)

	Ref	Expression
Assertion	tposconst	⊢ tpos ( ( 𝐴 × 𝐵 ) × { 𝐶 } ) = ( ( 𝐵 × 𝐴 ) × { 𝐶 } )

Proof

Step	Hyp	Ref	Expression
1		fconstmpo	⊢ ( ( 𝐴 × 𝐵 ) × { 𝐶 } ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2	1	tposmpo	⊢ tpos ( ( 𝐴 × 𝐵 ) × { 𝐶 } ) = ( 𝑦 ∈ 𝐵 , 𝑥 ∈ 𝐴 ↦ 𝐶 )
3		fconstmpo	⊢ ( ( 𝐵 × 𝐴 ) × { 𝐶 } ) = ( 𝑦 ∈ 𝐵 , 𝑥 ∈ 𝐴 ↦ 𝐶 )
4	2 3	eqtr4i	⊢ tpos ( ( 𝐴 × 𝐵 ) × { 𝐶 } ) = ( ( 𝐵 × 𝐴 ) × { 𝐶 } )