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	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ∀ 𝑘 ∈ ℕ0* 𝐺 RegGraph 𝑘 )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) ∧ 𝑘 ∈ ℕ0* ) → 𝑘 ∈ ℕ0* )
2		rzal	⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝑘 )
3	2	ad2antlr	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) ∧ 𝑘 ∈ ℕ0* ) → ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝑘 )
4		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
5		eqid	⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
6	4 5	isrgr	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑘 ∈ ℕ0* ) → ( 𝐺 RegGraph 𝑘 ↔ ( 𝑘 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝑘 ) ) )
7	6	adantlr	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) ∧ 𝑘 ∈ ℕ0* ) → ( 𝐺 RegGraph 𝑘 ↔ ( 𝑘 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝑘 ) ) )
8	1 3 7	mpbir2and	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) ∧ 𝑘 ∈ ℕ0* ) → 𝐺 RegGraph 𝑘 )
9	8	ralrimiva	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ∀ 𝑘 ∈ ℕ0* 𝐺 RegGraph 𝑘 )