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

Metamath Proof Explorer

Theorem tposf

Description: The domain and codomain of a transposition. (Contributed by NM, 10-Sep-2015)

		Ref	Expression
	Assertion	tposf	$⊢ F : A \times B ⟶ C \to tpos F : B \times A ⟶ C$

Step	Hyp	Ref	Expression
1		relxp	$⊢ Rel (A \times B)$
2		tposf2	$⊢ Rel (A \times B) \to (F : A \times B ⟶ C \to tpos F : {(A \times B)}^{-1} ⟶ C)$
3	1 2	ax-mp	$⊢ F : A \times B ⟶ C \to tpos F : {(A \times B)}^{-1} ⟶ C$
4		cnvxp	$⊢ {(A \times B)}^{-1} = B \times A$
5	4	feq2i	$⊢ tpos F : {(A \times B)}^{-1} ⟶ C \leftrightarrow tpos F : B \times A ⟶ C$
6	3 5	sylib	$⊢ F : A \times B ⟶ C \to tpos F : B \times A ⟶ C$