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\mathrm{Struct}X$$
Assertion	structfun	$$⊢\mathrm{Fun}{F^{-1}}^{-1}$$

Proof

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