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
|
syl5bb |
|- ( 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
|
syl5bb |
|- ( 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 ) ) |