Metamath Proof Explorer

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 ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → G ∈ ConnGraph

Proof

Step Hyp Ref Expression
1 rzal ⊢ Vtx ⁡ G = ∅ → ∀ k ∈ Vtx ⁡ G ∀ n ∈ Vtx ⁡ G ∃ f ∃ p f k PathsOn ⁡ G n p
2 1 adantl ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → ∀ k ∈ Vtx ⁡ G ∀ n ∈ Vtx ⁡ G ∃ f ∃ p f k PathsOn ⁡ G n p
3 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
4 3 isconngr ⊢ G ∈ W → G ∈ ConnGraph ↔ ∀ k ∈ Vtx ⁡ G ∀ n ∈ Vtx ⁡ G ∃ f ∃ p f k PathsOn ⁡ G n p
5 4 adantr ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → G ∈ ConnGraph ↔ ∀ k ∈ Vtx ⁡ G ∀ n ∈ Vtx ⁡ G ∃ f ∃ p f k PathsOn ⁡ G n p
6 2 5 mpbird ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → G ∈ ConnGraph