Metamath Proof Explorer

Theorem isconngr

Description: The property of being a connected graph. (Contributed by Alexander van der Vekens, 2-Dec-2017) (Revised by AV, 15-Feb-2021)

Ref Expression
Hypothesis isconngr.v 
|- V = ( Vtx ` G )
Assertion isconngr 
|- ( G e. W -> ( G e. ConnGraph <-> A. k e. V A. n e. V E. f E. p f ( k ( PathsOn ` G ) n ) p ) )

Proof

Step Hyp Ref Expression
1 isconngr.v 
 |-  V = ( Vtx ` G )
2 df-conngr 
 |-  ConnGraph = { g | [. ( Vtx ` g ) / v ]. A. k e. v A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p }
3 2 eleq2i 
 |-  ( G e. ConnGraph <-> G e. { g | [. ( Vtx ` g ) / v ]. A. k e. v A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p } )
4 fvex 
 |-  ( Vtx ` g ) e. _V
5 raleq 
 |-  ( v = ( Vtx ` g ) -> ( A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p <-> A. n e. ( Vtx ` g ) E. f E. p f ( k ( PathsOn ` g ) n ) p ) )
6 5 raleqbi1dv 
 |-  ( v = ( Vtx ` g ) -> ( A. k e. v A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p <-> A. k e. ( Vtx ` g ) A. n e. ( Vtx ` g ) E. f E. p f ( k ( PathsOn ` g ) n ) p ) )
7 4 6 sbcie 
 |-  ( [. ( Vtx ` g ) / v ]. A. k e. v A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p <-> A. k e. ( Vtx ` g ) A. n e. ( Vtx ` g ) E. f E. p f ( k ( PathsOn ` g ) n ) p )
8 7 abbii 
 |-  { g | [. ( Vtx ` g ) / v ]. A. k e. v A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p } = { g | A. k e. ( Vtx ` g ) A. n e. ( Vtx ` g ) E. f E. p f ( k ( PathsOn ` g ) n ) p }
9 8 eleq2i 
 |-  ( G e. { g | [. ( Vtx ` g ) / v ]. A. k e. v A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p } <-> G e. { g | A. k e. ( Vtx ` g ) A. n e. ( Vtx ` g ) E. f E. p f ( k ( PathsOn ` g ) n ) p } )
10 fveq2 
 |-  ( h = G -> ( Vtx ` h ) = ( Vtx ` G ) )
11 10 1 eqtr4di 
 |-  ( h = G -> ( Vtx ` h ) = V )
12 fveq2 
 |-  ( h = G -> ( PathsOn ` h ) = ( PathsOn ` G ) )
13 12 oveqd 
 |-  ( h = G -> ( k ( PathsOn ` h ) n ) = ( k ( PathsOn ` G ) n ) )
14 13 breqd 
 |-  ( h = G -> ( f ( k ( PathsOn ` h ) n ) p <-> f ( k ( PathsOn ` G ) n ) p ) )
15 14 2exbidv 
 |-  ( h = G -> ( E. f E. p f ( k ( PathsOn ` h ) n ) p <-> E. f E. p f ( k ( PathsOn ` G ) n ) p ) )
16 11 15 raleqbidv 
 |-  ( h = G -> ( A. n e. ( Vtx ` h ) E. f E. p f ( k ( PathsOn ` h ) n ) p <-> A. n e. V E. f E. p f ( k ( PathsOn ` G ) n ) p ) )
17 11 16 raleqbidv 
 |-  ( h = G -> ( A. k e. ( Vtx ` h ) A. n e. ( Vtx ` h ) E. f E. p f ( k ( PathsOn ` h ) n ) p <-> A. k e. V A. n e. V E. f E. p f ( k ( PathsOn ` G ) n ) p ) )
18 fveq2 
 |-  ( g = h -> ( Vtx ` g ) = ( Vtx ` h ) )
19 fveq2 
 |-  ( g = h -> ( PathsOn ` g ) = ( PathsOn ` h ) )
20 19 oveqd 
 |-  ( g = h -> ( k ( PathsOn ` g ) n ) = ( k ( PathsOn ` h ) n ) )
21 20 breqd 
 |-  ( g = h -> ( f ( k ( PathsOn ` g ) n ) p <-> f ( k ( PathsOn ` h ) n ) p ) )
22 21 2exbidv 
 |-  ( g = h -> ( E. f E. p f ( k ( PathsOn ` g ) n ) p <-> E. f E. p f ( k ( PathsOn ` h ) n ) p ) )
23 18 22 raleqbidv 
 |-  ( g = h -> ( A. n e. ( Vtx ` g ) E. f E. p f ( k ( PathsOn ` g ) n ) p <-> A. n e. ( Vtx ` h ) E. f E. p f ( k ( PathsOn ` h ) n ) p ) )
24 18 23 raleqbidv 
 |-  ( g = h -> ( A. k e. ( Vtx ` g ) A. n e. ( Vtx ` g ) E. f E. p f ( k ( PathsOn ` g ) n ) p <-> A. k e. ( Vtx ` h ) A. n e. ( Vtx ` h ) E. f E. p f ( k ( PathsOn ` h ) n ) p ) )
25 24 cbvabv 
 |-  { g | A. k e. ( Vtx ` g ) A. n e. ( Vtx ` g ) E. f E. p f ( k ( PathsOn ` g ) n ) p } = { h | A. k e. ( Vtx ` h ) A. n e. ( Vtx ` h ) E. f E. p f ( k ( PathsOn ` h ) n ) p }
26 17 25 elab2g 
 |-  ( G e. W -> ( G e. { g | A. k e. ( Vtx ` g ) A. n e. ( Vtx ` g ) E. f E. p f ( k ( PathsOn ` g ) n ) p } <-> A. k e. V A. n e. V E. f E. p f ( k ( PathsOn ` G ) n ) p ) )
27 9 26 syl5bb 
 |-  ( G e. W -> ( G e. { g | [. ( Vtx ` g ) / v ]. A. k e. v A. n e. v E. f E. p f ( k ( PathsOn ` g ) n ) p } <-> A. k e. V A. n e. V E. f E. p f ( k ( PathsOn ` G ) n ) p ) )
28 3 27 syl5bb 
 |-  ( G e. W -> ( G e. ConnGraph <-> A. k e. V A. n e. V E. f E. p f ( k ( PathsOn ` G ) n ) p ) )