Metamath Proof Explorer


Theorem iswlkg

Description: Generalization of iswlk : Conditions for two classes to represent a walk. (Contributed by Alexander van der Vekens, 23-Jun-2018) (Revised by AV, 1-Jan-2021)

Ref Expression
Hypotheses iswlkg.v
|- V = ( Vtx ` G )
iswlkg.i
|- I = ( iEdg ` G )
Assertion iswlkg
|- ( G e. W -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 iswlkg.v
 |-  V = ( Vtx ` G )
2 iswlkg.i
 |-  I = ( iEdg ` G )
3 wlkv
 |-  ( F ( Walks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
4 3simpc
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( F e. _V /\ P e. _V ) )
5 3 4 syl
 |-  ( F ( Walks ` G ) P -> ( F e. _V /\ P e. _V ) )
6 5 a1i
 |-  ( G e. W -> ( F ( Walks ` G ) P -> ( F e. _V /\ P e. _V ) ) )
7 elex
 |-  ( F e. Word dom I -> F e. _V )
8 ovex
 |-  ( 0 ... ( # ` F ) ) e. _V
9 1 fvexi
 |-  V e. _V
10 8 9 fpm
 |-  ( P : ( 0 ... ( # ` F ) ) --> V -> P e. ( V ^pm ( 0 ... ( # ` F ) ) ) )
11 10 elexd
 |-  ( P : ( 0 ... ( # ` F ) ) --> V -> P e. _V )
12 7 11 anim12i
 |-  ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) -> ( F e. _V /\ P e. _V ) )
13 12 3adant3
 |-  ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) -> ( F e. _V /\ P e. _V ) )
14 13 a1i
 |-  ( G e. W -> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) -> ( F e. _V /\ P e. _V ) ) )
15 1 2 iswlk
 |-  ( ( G e. W /\ F e. _V /\ P e. _V ) -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )
16 15 3expib
 |-  ( G e. W -> ( ( F e. _V /\ P e. _V ) -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) ) )
17 6 14 16 pm5.21ndd
 |-  ( G e. W -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )