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

Metamath Proof Explorer

Theorem structfun

Description: Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015) (Proof shortened by AV, 12-Nov-2021)

		Ref	Expression
	Hypothesis	structfun.1	$⊢ F Struct X$
	Assertion	structfun	$⊢ Fun {F^{-1}}^{-1}$

Step	Hyp	Ref	Expression
1		structfun.1	$⊢ F Struct X$
2		structfung	$⊢ F Struct X \to Fun {F^{-1}}^{-1}$
3	1 2	ax-mp	$⊢ Fun {F^{-1}}^{-1}$