Step |
Hyp |
Ref |
Expression |
1 |
|
upwlksfval.v |
|- V = ( Vtx ` G ) |
2 |
|
upwlksfval.i |
|- I = ( iEdg ` G ) |
3 |
1 2
|
upwlksfval |
|- ( G e. _V -> ( UPWalks ` G ) = { <. f , p >. | ( f e. Word dom I /\ p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0 ..^ ( # ` f ) ) ( I ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) } ) |
4 |
3
|
breqd |
|- ( G e. _V -> ( F ( UPWalks ` G ) P <-> F { <. f , p >. | ( f e. Word dom I /\ p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0 ..^ ( # ` f ) ) ( I ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) } P ) ) |
5 |
|
brabv |
|- ( F { <. f , p >. | ( f e. Word dom I /\ p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0 ..^ ( # ` f ) ) ( I ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) } P -> ( F e. _V /\ P e. _V ) ) |
6 |
4 5
|
syl6bi |
|- ( G e. _V -> ( F ( UPWalks ` G ) P -> ( F e. _V /\ P e. _V ) ) ) |
7 |
6
|
imdistani |
|- ( ( G e. _V /\ F ( UPWalks ` G ) P ) -> ( G e. _V /\ ( F e. _V /\ P e. _V ) ) ) |
8 |
|
3anass |
|- ( ( G e. _V /\ F e. _V /\ P e. _V ) <-> ( G e. _V /\ ( F e. _V /\ P e. _V ) ) ) |
9 |
7 8
|
sylibr |
|- ( ( G e. _V /\ F ( UPWalks ` G ) P ) -> ( G e. _V /\ F e. _V /\ P e. _V ) ) |
10 |
9
|
ex |
|- ( G e. _V -> ( F ( UPWalks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) ) ) |
11 |
|
fvprc |
|- ( -. G e. _V -> ( UPWalks ` G ) = (/) ) |
12 |
|
breq |
|- ( ( UPWalks ` G ) = (/) -> ( F ( UPWalks ` G ) P <-> F (/) P ) ) |
13 |
|
br0 |
|- -. F (/) P |
14 |
13
|
pm2.21i |
|- ( F (/) P -> ( G e. _V /\ F e. _V /\ P e. _V ) ) |
15 |
12 14
|
syl6bi |
|- ( ( UPWalks ` G ) = (/) -> ( F ( UPWalks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) ) ) |
16 |
11 15
|
syl |
|- ( -. G e. _V -> ( F ( UPWalks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) ) ) |
17 |
10 16
|
pm2.61i |
|- ( F ( UPWalks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) ) |