Metamath Proof Explorer

Theorem 0vtxrgr

Description: A null graph (with no vertices) is k-regular for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018) (Revised by AV, 26-Dec-2020)

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

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ ((G \in W \land Vtx (G) = \emptyset) \land k \in ℕ_{0}^{}) \to k \in ℕ_{0}^{}$
2		rzal	$⊢ Vtx (G) = \emptyset \to \forall v \in Vtx (G) VtxDeg (G) (v) = k$
3	2	ad2antlr	$⊢ ((G \in W \land Vtx (G) = \emptyset) \land k \in ℕ_{0}^{*}) \to \forall v \in Vtx (G) VtxDeg (G) (v) = k$
4		eqid	$⊢ Vtx (G) = Vtx (G)$
5		eqid	$⊢ VtxDeg (G) = VtxDeg (G)$
6	4 5	isrgr	$⊢ (G \in W \land k \in ℕ_{0}^{}) \to (G RegGraph k \leftrightarrow (k \in ℕ_{0}^{} \land \forall v \in Vtx (G) VtxDeg (G) (v) = k))$
7	6	adantlr	$⊢ ((G \in W \land Vtx (G) = \emptyset) \land k \in ℕ_{0}^{}) \to (G RegGraph k \leftrightarrow (k \in ℕ_{0}^{} \land \forall v \in Vtx (G) VtxDeg (G) (v) = k))$
8	1 3 7	mpbir2and	$⊢ ((G \in W \land Vtx (G) = \emptyset) \land k \in ℕ_{0}^{*}) \to G RegGraph k$
9	8	ralrimiva	$⊢ (G \in W \land Vtx (G) = \emptyset) \to \forall k \in ℕ_{0}^{*} G RegGraph k$