Metamath Proof Explorer

Theorem 0vtxrusgr

Description: A graph with no vertices and an empty edge function 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	0vtxrusgr	$⊢ (G \in W \land Vtx (G) = \emptyset \land iEdg (G) = \emptyset) \to \forall k \in ℕ_{0}^{*} G RegUSGraph k$

Proof

Step	Hyp	Ref	Expression
1		usgr0v	$⊢ (G \in W \land Vtx (G) = \emptyset \land iEdg (G) = \emptyset) \to G \in USGraph$
2	1	adantr	$⊢ ((G \in W \land Vtx (G) = \emptyset \land iEdg (G) = \emptyset) \land k \in ℕ_{0}^{*}) \to G \in USGraph$
3		0vtxrgr	$⊢ (G \in W \land Vtx (G) = \emptyset) \to \forall v \in ℕ_{0}^{*} G RegGraph v$
4		breq2	$⊢ v = k \to (G RegGraph v \leftrightarrow G RegGraph k)$
5	4	rspccv	$⊢ \forall v \in ℕ_{0}^{} G RegGraph v \to (k \in ℕ_{0}^{} \to G RegGraph k)$
6	3 5	syl	$⊢ (G \in W \land Vtx (G) = \emptyset) \to (k \in ℕ_{0}^{*} \to G RegGraph k)$
7	6	3adant3	$⊢ (G \in W \land Vtx (G) = \emptyset \land iEdg (G) = \emptyset) \to (k \in ℕ_{0}^{*} \to G RegGraph k)$
8	7	imp	$⊢ ((G \in W \land Vtx (G) = \emptyset \land iEdg (G) = \emptyset) \land k \in ℕ_{0}^{*}) \to G RegGraph k$
9		isrusgr	$⊢ (G \in W \land k \in ℕ_{0}^{*}) \to (G RegUSGraph k \leftrightarrow (G \in USGraph \land G RegGraph k))$
10	9	3ad2antl1	$⊢ ((G \in W \land Vtx (G) = \emptyset \land iEdg (G) = \emptyset) \land k \in ℕ_{0}^{*}) \to (G RegUSGraph k \leftrightarrow (G \in USGraph \land G RegGraph k))$
11	2 8 10	mpbir2and	$⊢ ((G \in W \land Vtx (G) = \emptyset \land iEdg (G) = \emptyset) \land k \in ℕ_{0}^{*}) \to G RegUSGraph k$
12	11	ralrimiva	$⊢ (G \in W \land Vtx (G) = \emptyset \land iEdg (G) = \emptyset) \to \forall k \in ℕ_{0}^{*} G RegUSGraph k$