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

Metamath Proof Explorer

Theorem structn0fun

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

		Ref	Expression
	Assertion	structn0fun	$⊢ F Struct X \to Fun (F ∖ \{\emptyset\})$

Step	Hyp	Ref	Expression
1		isstruct2	$⊢ F Struct X \leftrightarrow (X \in (\leq \cap (ℕ \times ℕ)) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq \dots (X))$
2	1	simp2bi	$⊢ F Struct X \to Fun (F ∖ \{\emptyset\})$