tposfo2

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

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

Step	Hyp	Ref	Expression
1		tposfn2	$⊢ Rel A \to (F Fn A \to tpos F Fn A^{-1})$
2	1	adantrd	$⊢ Rel A \to ((F Fn A \land ran F = B) \to tpos F Fn A^{-1})$
3		fndm	$⊢ F Fn A \to dom F = A$
4	3	releqd	$⊢ F Fn A \to (Rel dom F \leftrightarrow Rel A)$
5	4	biimparc	$⊢ (Rel A \land F Fn A) \to Rel dom F$
6		rntpos	$⊢ Rel dom F \to ran tpos F = ran F$
7	5 6	syl	$⊢ (Rel A \land F Fn A) \to ran tpos F = ran F$
8	7	eqeq1d	$⊢ (Rel A \land F Fn A) \to (ran tpos F = B \leftrightarrow ran F = B)$
9	8	biimprd	$⊢ (Rel A \land F Fn A) \to (ran F = B \to ran tpos F = B)$
10	9	expimpd	$⊢ Rel A \to ((F Fn A \land ran F = B) \to ran tpos F = B)$
11	2 10	jcad	$⊢ Rel A \to ((F Fn A \land ran F = B) \to (tpos F Fn A^{-1} \land ran tpos F = B))$
12		df-fo	$⊢ F : A \underset{onto}{⟶} B \leftrightarrow (F Fn A \land ran F = B)$
13		df-fo	$⊢ tpos F : A^{-1} \underset{onto}{⟶} B \leftrightarrow (tpos F Fn A^{-1} \land ran tpos F = B)$
14	11 12 13	3imtr4g	$⊢ Rel A \to (F : A \underset{onto}{⟶} B \to tpos F : A^{-1} \underset{onto}{⟶} B)$

Metamath Proof Explorer