tposf2

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

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

Step	Hyp	Ref	Expression
1		tposfo2	$⊢ Rel A \to (F : A \underset{onto}{⟶} ran F \to tpos F : A^{-1} \underset{onto}{⟶} ran F)$
2		ffn	$⊢ F : A ⟶ B \to F Fn A$
3		dffn4	$⊢ F Fn A \leftrightarrow F : A \underset{onto}{⟶} ran F$
4	2 3	sylib	$⊢ F : A ⟶ B \to F : A \underset{onto}{⟶} ran F$
5	1 4	impel	$⊢ (Rel A \land F : A ⟶ B) \to tpos F : A^{-1} \underset{onto}{⟶} ran F$
6		fof	$⊢ tpos F : A^{-1} \underset{onto}{⟶} ran F \to tpos F : A^{-1} ⟶ ran F$
7	5 6	syl	$⊢ (Rel A \land F : A ⟶ B) \to tpos F : A^{-1} ⟶ ran F$
8		frn	$⊢ F : A ⟶ B \to ran F \subseteq B$
9	8	adantl	$⊢ (Rel A \land F : A ⟶ B) \to ran F \subseteq B$
10	7 9	fssd	$⊢ (Rel A \land F : A ⟶ B) \to tpos F : A^{-1} ⟶ B$
11	10	ex	$⊢ Rel A \to (F : A ⟶ B \to tpos F : A^{-1} ⟶ B)$

Metamath Proof Explorer