Theorem 0vconngr

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	0vconngr	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ ConnGraph )

Proof

Step	Hyp	Ref	Expression
1		rzal	⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 )
2	1	adantl	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 )
3		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
4	3	isconngr	⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ ConnGraph ↔ ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 ) )
5	4	adantr	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( 𝐺 ∈ ConnGraph ↔ ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑛 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑘 ( PathsOn ‘ 𝐺 ) 𝑛 ) 𝑝 ) )
6	2 5	mpbird	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ ConnGraph )