tposf1o2

Description: Condition of a bijective transposition. (Contributed by NM, 10-Sep-2015)

		Ref	Expression
	Assertion	tposf1o2	$⊢ Rel A \to (F : A \underset{1-1 onto}{⟶} B \to tpos F : A^{-1} \underset{1-1 onto}{⟶} B)$

Step	Hyp	Ref	Expression
1		tposf12	$⊢ Rel A \to (F : A \underset{1-1}{⟶} B \to tpos F : A^{-1} \underset{1-1}{⟶} B)$
2		tposfo2	$⊢ Rel A \to (F : A \underset{onto}{⟶} B \to tpos F : A^{-1} \underset{onto}{⟶} B)$
3	1 2	anim12d	$⊢ Rel A \to ((F : A \underset{1-1}{⟶} B \land F : A \underset{onto}{⟶} B) \to (tpos F : A^{-1} \underset{1-1}{⟶} B \land tpos F : A^{-1} \underset{onto}{⟶} B))$
4		df-f1o	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (F : A \underset{1-1}{⟶} B \land F : A \underset{onto}{⟶} B)$
5		df-f1o	$⊢ tpos F : A^{-1} \underset{1-1 onto}{⟶} B \leftrightarrow (tpos F : A^{-1} \underset{1-1}{⟶} B \land tpos F : A^{-1} \underset{onto}{⟶} B)$
6	3 4 5	3imtr4g	$⊢ Rel A \to (F : A \underset{1-1 onto}{⟶} B \to tpos F : A^{-1} \underset{1-1 onto}{⟶} B)$

Metamath Proof Explorer