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

Proof

Step	Hyp	Ref	Expression
1		usgr0v	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ USGraph )
2	1	adantr	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ∧ ( iEdg ‘ 𝐺 ) = ∅ ) ∧ 𝑘 ∈ ℕ0* ) → 𝐺 ∈ USGraph )
3		0vtxrgr	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ∀ 𝑣 ∈ ℕ0* 𝐺 RegGraph 𝑣 )
4		breq2	⊢ ( 𝑣 = 𝑘 → ( 𝐺 RegGraph 𝑣 ↔ 𝐺 RegGraph 𝑘 ) )
5	4	rspccv	⊢ ( ∀ 𝑣 ∈ ℕ0* 𝐺 RegGraph 𝑣 → ( 𝑘 ∈ ℕ0* → 𝐺 RegGraph 𝑘 ) )
6	3 5	syl	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( 𝑘 ∈ ℕ0* → 𝐺 RegGraph 𝑘 ) )
7	6	3adant3	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → ( 𝑘 ∈ ℕ0* → 𝐺 RegGraph 𝑘 ) )
8	7	imp	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ∧ ( iEdg ‘ 𝐺 ) = ∅ ) ∧ 𝑘 ∈ ℕ0* ) → 𝐺 RegGraph 𝑘 )
9		isrusgr	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑘 ∈ ℕ0* ) → ( 𝐺 RegUSGraph 𝑘 ↔ ( 𝐺 ∈ USGraph ∧ 𝐺 RegGraph 𝑘 ) ) )
10	9	3ad2antl1	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ∧ ( iEdg ‘ 𝐺 ) = ∅ ) ∧ 𝑘 ∈ ℕ0* ) → ( 𝐺 RegUSGraph 𝑘 ↔ ( 𝐺 ∈ USGraph ∧ 𝐺 RegGraph 𝑘 ) ) )
11	2 8 10	mpbir2and	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ∧ ( iEdg ‘ 𝐺 ) = ∅ ) ∧ 𝑘 ∈ ℕ0* ) → 𝐺 RegUSGraph 𝑘 )
12	11	ralrimiva	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → ∀ 𝑘 ∈ ℕ0* 𝐺 RegUSGraph 𝑘 )