Metamath Proof Explorer


Theorem clwlkcompim

Description: Implications for the properties of the components of a closed walk. (Contributed by Alexander van der Vekens, 24-Jun-2018) (Revised by AV, 17-Feb-2021)

Ref Expression
Hypotheses isclwlke.v
|- V = ( Vtx ` G )
isclwlke.i
|- I = ( iEdg ` G )
clwlkcomp.1
|- F = ( 1st ` W )
clwlkcomp.2
|- P = ( 2nd ` W )
Assertion clwlkcompim
|- ( W e. ( ClWalks ` G ) -> ( ( 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 ) ) ) /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isclwlke.v
 |-  V = ( Vtx ` G )
2 isclwlke.i
 |-  I = ( iEdg ` G )
3 clwlkcomp.1
 |-  F = ( 1st ` W )
4 clwlkcomp.2
 |-  P = ( 2nd ` W )
5 elfvex
 |-  ( W e. ( ClWalks ` G ) -> G e. _V )
6 clwlks
 |-  ( ClWalks ` G ) = { <. f , g >. | ( f ( Walks ` G ) g /\ ( g ` 0 ) = ( g ` ( # ` f ) ) ) }
7 6 a1i
 |-  ( G e. _V -> ( ClWalks ` G ) = { <. f , g >. | ( f ( Walks ` G ) g /\ ( g ` 0 ) = ( g ` ( # ` f ) ) ) } )
8 7 eleq2d
 |-  ( G e. _V -> ( W e. ( ClWalks ` G ) <-> W e. { <. f , g >. | ( f ( Walks ` G ) g /\ ( g ` 0 ) = ( g ` ( # ` f ) ) ) } ) )
9 elopaelxp
 |-  ( W e. { <. f , g >. | ( f ( Walks ` G ) g /\ ( g ` 0 ) = ( g ` ( # ` f ) ) ) } -> W e. ( _V X. _V ) )
10 9 anim2i
 |-  ( ( G e. _V /\ W e. { <. f , g >. | ( f ( Walks ` G ) g /\ ( g ` 0 ) = ( g ` ( # ` f ) ) ) } ) -> ( G e. _V /\ W e. ( _V X. _V ) ) )
11 10 ex
 |-  ( G e. _V -> ( W e. { <. f , g >. | ( f ( Walks ` G ) g /\ ( g ` 0 ) = ( g ` ( # ` f ) ) ) } -> ( G e. _V /\ W e. ( _V X. _V ) ) ) )
12 8 11 sylbid
 |-  ( G e. _V -> ( W e. ( ClWalks ` G ) -> ( G e. _V /\ W e. ( _V X. _V ) ) ) )
13 5 12 mpcom
 |-  ( W e. ( ClWalks ` G ) -> ( G e. _V /\ W e. ( _V X. _V ) ) )
14 1 2 3 4 clwlkcomp
 |-  ( ( G e. _V /\ W e. ( _V X. _V ) ) -> ( W e. ( ClWalks ` G ) <-> ( ( 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 ) ) ) /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) ) )
15 13 14 syl
 |-  ( W e. ( ClWalks ` G ) -> ( W e. ( ClWalks ` G ) <-> ( ( 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 ) ) ) /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) ) )
16 15 ibi
 |-  ( W e. ( ClWalks ` G ) -> ( ( 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 ) ) ) /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) )