Metamath Proof Explorer

Theorem 0uhgrrusgr

Description: The null graph as hypergraph is a k-regular simple graph for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018) (Revised by AV, 26-Dec-2020)

		Ref	Expression
	Assertion	0uhgrrusgr	$⊢ (G \in UHGraph \land Vtx (G) = \emptyset) \to \forall k \in ℕ_{0}^{*} G RegUSGraph k$

Proof

Step	Hyp	Ref	Expression
1		uhgr0vb	$⊢ (G \in UHGraph \land Vtx (G) = \emptyset) \to (G \in UHGraph \leftrightarrow iEdg (G) = \emptyset)$
2	1	biimpd	$⊢ (G \in UHGraph \land Vtx (G) = \emptyset) \to (G \in UHGraph \to iEdg (G) = \emptyset)$
3	2	ex	$⊢ G \in UHGraph \to (Vtx (G) = \emptyset \to (G \in UHGraph \to iEdg (G) = \emptyset))$
4	3	pm2.43a	$⊢ G \in UHGraph \to (Vtx (G) = \emptyset \to iEdg (G) = \emptyset)$
5	4	imp	$⊢ (G \in UHGraph \land Vtx (G) = \emptyset) \to iEdg (G) = \emptyset$
6		0vtxrusgr	$⊢ (G \in UHGraph \land Vtx (G) = \emptyset \land iEdg (G) = \emptyset) \to \forall k \in ℕ_{0}^{*} G RegUSGraph k$
7	5 6	mpd3an3	$⊢ (G \in UHGraph \land Vtx (G) = \emptyset) \to \forall k \in ℕ_{0}^{*} G RegUSGraph k$