Metamath Proof Explorer

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 ⊢ ∀ k ∈ ∅ ∀ n ∈ ∅ ∃ f ∃ p f k PathsOn ⁡ ∅ n p
2 0ex ⊢ ∅ ∈ V
3 vtxval0 ⊢ Vtx ⁡ ∅ = ∅
4 3 eqcomi ⊢ ∅ = Vtx ⁡ ∅
5 4 isconngr ⊢ ∅ ∈ V → ∅ ∈ ConnGraph ↔ ∀ k ∈ ∅ ∀ n ∈ ∅ ∃ f ∃ p f k PathsOn ⁡ ∅ n p
6 2 5 ax-mp ⊢ ∅ ∈ ConnGraph ↔ ∀ k ∈ ∅ ∀ n ∈ ∅ ∃ f ∃ p f k PathsOn ⁡ ∅ n p
7 1 6 mpbir ⊢ ∅ ∈ ConnGraph