Metamath Proof Explorer

Theorem wlkvtxiedg

Description: The vertices of a walk are connected by indexed edges. (Contributed by Alexander van der Vekens, 22-Jul-2018) (Revised by AV, 2-Jan-2021) (Proof shortened by AV, 4-Apr-2021)

Ref Expression
Hypothesis wlkvtxeledg.i 
|- I = ( iEdg ` G )
Assertion wlkvtxiedg 
|- ( F ( Walks ` G ) P -> A. k e. ( 0 ..^ ( # ` F ) ) E. e e. ran I { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e )

Proof

Step Hyp Ref Expression
1 wlkvtxeledg.i 
 |-  I = ( iEdg ` G )
2 1 wlkvtxeledg 
 |-  ( F ( Walks ` G ) P -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )
3 fvex 
 |-  ( P ` k ) e. _V
4 3 prnz 
 |-  { ( P ` k ) , ( P ` ( k + 1 ) ) } =/= (/)
5 ssn0 
 |-  ( ( { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } =/= (/) ) -> ( I ` ( F ` k ) ) =/= (/) )
6 4 5 mpan2 
 |-  ( { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) -> ( I ` ( F ` k ) ) =/= (/) )
7 6 adantl 
 |-  ( ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> ( I ` ( F ` k ) ) =/= (/) )
8 fvn0fvelrn 
 |-  ( ( I ` ( F ` k ) ) =/= (/) -> ( I ` ( F ` k ) ) e. ran I )
9 7 8 syl 
 |-  ( ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> ( I ` ( F ` k ) ) e. ran I )
10 sseq2 
 |-  ( e = ( I ` ( F ` k ) ) -> ( { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e <-> { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
11 10 adantl 
 |-  ( ( ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) /\ e = ( I ` ( F ` k ) ) ) -> ( { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e <-> { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
12 simpr 
 |-  ( ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )
13 9 11 12 rspcedvd 
 |-  ( ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> E. e e. ran I { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e )
14 13 ex 
 |-  ( ( F ( Walks ` G ) P /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) -> E. e e. ran I { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e ) )
15 14 ralimdva 
 |-  ( F ( Walks ` G ) P -> ( A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) E. e e. ran I { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e ) )
16 2 15 mpd 
 |-  ( F ( Walks ` G ) P -> A. k e. ( 0 ..^ ( # ` F ) ) E. e e. ran I { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e )