Metamath Proof Explorer

Theorem isupwlkg

Description: Generalization of isupwlk : Conditions for two classes to represent a simple walk. (Contributed by AV, 5-Nov-2021)

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

Proof

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 brfvopab 
 |-  ( F ( UPWalks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
5 4 a1i 
 |-  ( G e. W -> ( F ( UPWalks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) ) )
6 elex 
 |-  ( G e. W -> G 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 ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) -> ( F e. _V /\ P e. _V ) )
14 6 13 anim12i 
 |-  ( ( G e. W /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) -> ( G e. _V /\ ( F e. _V /\ P e. _V ) ) )
15 14 ex 
 |-  ( G e. W -> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) -> ( G e. _V /\ ( F e. _V /\ P e. _V ) ) ) )
16 3anass 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) <-> ( G e. _V /\ ( F e. _V /\ P e. _V ) ) )
17 15 16 syl6ibr 
 |-  ( G e. W -> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) -> ( G e. _V /\ F e. _V /\ P e. _V ) ) )
18 1 2 isupwlk 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( F ( UPWalks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
19 18 a1i 
 |-  ( G e. W -> ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( F ( UPWalks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) ) )
20 5 17 19 pm5.21ndd 
 |-  ( G e. W -> ( F ( UPWalks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )