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 e. W /\ ( Vtx ` G ) = (/) ) -> G e. ConnGraph )

Proof

Step Hyp Ref Expression
1 rzal 
 |-  ( ( Vtx ` G ) = (/) -> A. k e. ( Vtx ` G ) A. n e. ( Vtx ` G ) E. f E. p f ( k ( PathsOn ` G ) n ) p )
2 1 adantl 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> A. k e. ( Vtx ` G ) A. n e. ( Vtx ` G ) E. f E. p f ( k ( PathsOn ` G ) n ) p )
3 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
4 3 isconngr 
 |-  ( G e. W -> ( G e. ConnGraph <-> A. k e. ( Vtx ` G ) A. n e. ( Vtx ` G ) E. f E. p f ( k ( PathsOn ` G ) n ) p ) )
5 4 adantr 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( G e. ConnGraph <-> A. k e. ( Vtx ` G ) A. n e. ( Vtx ` G ) E. f E. p f ( k ( PathsOn ` G ) n ) p ) )
6 2 5 mpbird 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> G e. ConnGraph )