Theorem structn0fun

Description: A structure without the empty set is a function. (Contributed by AV, 13-Nov-2021)

	Ref	Expression
Assertion	structn0fun	$$⊢F\mathrm{Struct}X\to \mathrm{Fun}\left(F\setminus \left\{\varnothing \right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		isstruct2	$$⊢F\mathrm{Struct}X\leftrightarrow \left(X\in \left(\le \cap \left(\mathbb{N}\times \mathbb{N}\right)\right)\wedge \mathrm{Fun}\left(F\setminus \left\{\varnothing \right\}\right)\wedge \mathrm{dom}F\subseteq \dots \left(X\right)\right)$$
2	1	simp2bi	$$⊢F\mathrm{Struct}X\to \mathrm{Fun}\left(F\setminus \left\{\varnothing \right\}\right)$$