Metamath Proof Explorer

Theorem isconngr1

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 isconngr1 
|- ( G e. W -> ( G e. ConnGraph <-> A. k e. V A. n e. ( V \ { k } ) E. f E. p f ( k ( PathsOn ` G ) n ) p ) )

Proof

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