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

Proof

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