Theorem tposconst

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

	Ref	Expression
Assertion	tposconst	$$⊢tpos\left(\left(A\times B\right)\times \left\{C\right\}\right)=\left(B\times A\right)\times \left\{C\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fconstmpo	$$⊢\left(A\times B\right)\times \left\{C\right\}=\left(x\in A,y\in B⟼C\right)$$
2	1	tposmpo	$$⊢tpos\left(\left(A\times B\right)\times \left\{C\right\}\right)=\left(y\in B,x\in A⟼C\right)$$
3		fconstmpo	$$⊢\left(B\times A\right)\times \left\{C\right\}=\left(y\in B,x\in A⟼C\right)$$
4	2 3	eqtr4i	$$⊢tpos\left(\left(A\times B\right)\times \left\{C\right\}\right)=\left(B\times A\right)\times \left\{C\right\}$$