Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
2 |
|
eqid |
|- ( iEdg ` G ) = ( iEdg ` G ) |
3 |
1 2
|
upgriswlk |
|- ( G e. UPGraph -> ( F ( Walks ` G ) P <-> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) ) |
4 |
|
df-f1 |
|- ( P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) <-> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' P ) ) |
5 |
4
|
simplbi2 |
|- ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( Fun `' P -> P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) ) ) |
6 |
5
|
3ad2ant2 |
|- ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) -> ( Fun `' P -> P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) ) ) |
7 |
6
|
impcom |
|- ( ( Fun `' P /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) -> P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) ) |
8 |
|
simpr1 |
|- ( ( Fun `' P /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) -> F e. Word dom ( iEdg ` G ) ) |
9 |
7 8
|
jca |
|- ( ( Fun `' P /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) -> ( P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) /\ F e. Word dom ( iEdg ` G ) ) ) |
10 |
|
simpr3 |
|- ( ( Fun `' P /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) |
11 |
|
upgrwlkdvdelem |
|- ( ( P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) /\ F e. Word dom ( iEdg ` G ) ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> Fun `' F ) ) |
12 |
9 10 11
|
sylc |
|- ( ( Fun `' P /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) -> Fun `' F ) |
13 |
12
|
expcom |
|- ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) -> ( Fun `' P -> Fun `' F ) ) |
14 |
3 13
|
syl6bi |
|- ( G e. UPGraph -> ( F ( Walks ` G ) P -> ( Fun `' P -> Fun `' F ) ) ) |
15 |
14
|
3imp |
|- ( ( G e. UPGraph /\ F ( Walks ` G ) P /\ Fun `' P ) -> Fun `' F ) |