Theorem 0conngr

Description: A graph without vertices is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017) (Revised by AV, 15-Feb-2021)

	Ref	Expression
Assertion	0conngr	⊢ ∅ ∈ ConnGraph

Proof

Step	Hyp	Ref	Expression
1		ral0	⊢ ∀ 𝑘 ∈ ∅ ∀ 𝑛 ∈ ∅ ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ ∅ ) 𝑛 ) 𝑝
2		0ex	⊢ ∅ ∈ V
3		vtxval0	⊢ ( Vtx ‘ ∅ ) = ∅
4	3	eqcomi	⊢ ∅ = ( Vtx ‘ ∅ )
5	4	isconngr	⊢ ( ∅ ∈ V → ( ∅ ∈ ConnGraph ↔ ∀ 𝑘 ∈ ∅ ∀ 𝑛 ∈ ∅ ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ ∅ ) 𝑛 ) 𝑝 ) )
6	2 5	ax-mp	⊢ ( ∅ ∈ ConnGraph ↔ ∀ 𝑘 ∈ ∅ ∀ 𝑛 ∈ ∅ ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ ∅ ) 𝑛 ) 𝑝 )
7	1 6	mpbir	⊢ ∅ ∈ ConnGraph