tposfo

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

		Ref	Expression
	Assertion	tposfo	$⊢ F : A \times B \underset{onto}{⟶} C \to tpos F : B \times A \underset{onto}{⟶} C$

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

Metamath Proof Explorer