This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem structfung

Description: The converse of the converse of a structure is a function. Closed form of structfun . (Contributed by AV, 12-Nov-2021)

		Ref	Expression
	Assertion	structfung	$⊢ F Struct X \to Fun {F^{-1}}^{-1}$

Step	Hyp	Ref	Expression
1		structn0fun	$⊢ F Struct X \to Fun (F ∖ \{\emptyset\})$
2		structcnvcnv	$⊢ F Struct X \to {F^{-1}}^{-1} = F ∖ \{\emptyset\}$
3	2	funeqd	$⊢ F Struct X \to (Fun {F^{-1}}^{-1} \leftrightarrow Fun (F ∖ \{\emptyset\}))$
4	1 3	mpbird	$⊢ F Struct X \to Fun {F^{-1}}^{-1}$