uhgr0edg0rgr

Description: A hypergraph is 0-regular if it has no edges. (Contributed by AV, 19-Dec-2020)

		Ref	Expression
	Assertion	uhgr0edg0rgr	$⊢ (G \in UHGraph \land Edg (G) = \emptyset) \to G RegGraph 0$

Step	Hyp	Ref	Expression
1		uhgriedg0edg0	$⊢ G \in UHGraph \to (Edg (G) = \emptyset \leftrightarrow iEdg (G) = \emptyset)$
2	1	biimpa	$⊢ (G \in UHGraph \land Edg (G) = \emptyset) \to iEdg (G) = \emptyset$
3		0edg0rgr	$⊢ (G \in UHGraph \land iEdg (G) = \emptyset) \to G RegGraph 0$
4	2 3	syldan	$⊢ (G \in UHGraph \land Edg (G) = \emptyset) \to G RegGraph 0$

Metamath Proof Explorer