tposfun

Description: The transposition of a function is a function. (Contributed by Mario Carneiro, 10-Sep-2015)

		Ref	Expression
	Assertion	tposfun	$⊢ Fun F \to Fun tpos F$

Step	Hyp	Ref	Expression
1		funmpt	$⊢ Fun (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
2		funco	$⊢ (Fun F \land Fun (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})) \to Fun (F \circ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}))$
3	1 2	mpan2	$⊢ Fun F \to Fun (F \circ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}))$
4		df-tpos	$⊢ tpos F = F \circ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1})$
5	4	funeqi	$⊢ Fun tpos F \leftrightarrow Fun (F \circ (x \in ({dom F}^{-1} \cup \{\emptyset\}) ⟼ ⋃ {\{x\}}^{-1}))$
6	3 5	sylibr	$⊢ Fun F \to Fun tpos F$

Metamath Proof Explorer