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 
|- (/) e. ConnGraph

Proof

Step Hyp Ref Expression
1 ral0 
 |-  A. k e. (/) A. n e. (/) E. f E. p f ( k ( PathsOn ` (/) ) n ) p
2 0ex 
 |-  (/) e. _V
3 vtxval0 
 |-  ( Vtx ` (/) ) = (/)
4 3 eqcomi 
 |-  (/) = ( Vtx ` (/) )
5 4 isconngr 
 |-  ( (/) e. _V -> ( (/) e. ConnGraph <-> A. k e. (/) A. n e. (/) E. f E. p f ( k ( PathsOn ` (/) ) n ) p ) )
6 2 5 ax-mp 
 |-  ( (/) e. ConnGraph <-> A. k e. (/) A. n e. (/) E. f E. p f ( k ( PathsOn ` (/) ) n ) p )
7 1 6 mpbir 
 |-  (/) e. ConnGraph