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