Metamath Proof Explorer

Theorem upgriswlk

Description: Properties of a pair of functions to be a walk in a pseudograph. (Contributed by AV, 2-Jan-2021) (Revised by AV, 28-Oct-2021)

Ref Expression
Hypotheses upgriswlk.v 
|- V = ( Vtx ` G )
upgriswlk.i 
|- I = ( iEdg ` G )
Assertion upgriswlk 
|- ( G e. UPGraph -> ( F ( Walks ` 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 upgriswlk.v 
 |-  V = ( Vtx ` G )
2 upgriswlk.i 
 |-  I = ( iEdg ` G )
3 1 2 iswlkg 
 |-  ( G e. UPGraph -> ( 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 ) ) ) ) ) )
4 df-ifp 
 |-  ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) <-> ( ( ( P ` k ) = ( P ` ( k + 1 ) ) /\ ( I ` ( F ` k ) ) = { ( P ` k ) } ) \/ ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) )
5 dfsn2 
 |-  { ( P ` k ) } = { ( P ` k ) , ( P ` k ) }
6 preq2 
 |-  ( ( P ` k ) = ( P ` ( k + 1 ) ) -> { ( P ` k ) , ( P ` k ) } = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
7 5 6 eqtrid 
 |-  ( ( P ` k ) = ( P ` ( k + 1 ) ) -> { ( P ` k ) } = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
8 7 eqeq2d 
 |-  ( ( P ` k ) = ( P ` ( k + 1 ) ) -> ( ( I ` ( F ` k ) ) = { ( P ` k ) } <-> ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
9 8 biimpa 
 |-  ( ( ( P ` k ) = ( P ` ( k + 1 ) ) /\ ( I ` ( F ` k ) ) = { ( P ` k ) } ) -> ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
10 9 a1d 
 |-  ( ( ( P ` k ) = ( P ` ( k + 1 ) ) /\ ( I ` ( F ` k ) ) = { ( P ` k ) } ) -> ( ( ( G e. UPGraph /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
11 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
12 2 11 upgredginwlk 
 |-  ( ( G e. UPGraph /\ F e. Word dom I ) -> ( k e. ( 0 ..^ ( # ` F ) ) -> ( I ` ( F ` k ) ) e. ( Edg ` G ) ) )
13 12 adantrr 
 |-  ( ( G e. UPGraph /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) ) -> ( k e. ( 0 ..^ ( # ` F ) ) -> ( I ` ( F ` k ) ) e. ( Edg ` G ) ) )
14 13 imp 
 |-  ( ( ( G e. UPGraph /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( I ` ( F ` k ) ) e. ( Edg ` G ) )
15 simp-4l 
 |-  ( ( ( ( ( G e. UPGraph /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ ( I ` ( F ` k ) ) e. ( Edg ` G ) ) /\ ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) -> G e. UPGraph )
16 simpr 
 |-  ( ( ( ( G e. UPGraph /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ ( I ` ( F ` k ) ) e. ( Edg ` G ) ) -> ( I ` ( F ` k ) ) e. ( Edg ` G ) )
17 16 adantr 
 |-  ( ( ( ( ( G e. UPGraph /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ ( I ` ( F ` k ) ) e. ( Edg ` G ) ) /\ ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) -> ( I ` ( F ` k ) ) e. ( Edg ` G ) )
18 simpr 
 |-  ( ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )
19 18 adantl 
 |-  ( ( ( ( ( G e. UPGraph /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ ( I ` ( F ` k ) ) e. ( Edg ` G ) ) /\ ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) -> { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )
20 fvexd 
 |-  ( -. ( P ` k ) = ( P ` ( k + 1 ) ) -> ( P ` k ) e. _V )
21 fvexd 
 |-  ( -. ( P ` k ) = ( P ` ( k + 1 ) ) -> ( P ` ( k + 1 ) ) e. _V )
22 neqne 
 |-  ( -. ( P ` k ) = ( P ` ( k + 1 ) ) -> ( P ` k ) =/= ( P ` ( k + 1 ) ) )
23 20 21 22 3jca 
 |-  ( -. ( P ` k ) = ( P ` ( k + 1 ) ) -> ( ( P ` k ) e. _V /\ ( P ` ( k + 1 ) ) e. _V /\ ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
24 23 adantr 
 |-  ( ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> ( ( P ` k ) e. _V /\ ( P ` ( k + 1 ) ) e. _V /\ ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
25 24 adantl 
 |-  ( ( ( ( ( G e. UPGraph /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ ( I ` ( F ` k ) ) e. ( Edg ` G ) ) /\ ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) -> ( ( P ` k ) e. _V /\ ( P ` ( k + 1 ) ) e. _V /\ ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
26 1 11 upgredgpr 
 |-  ( ( ( G e. UPGraph /\ ( I ` ( F ` k ) ) e. ( Edg ` G ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) /\ ( ( P ` k ) e. _V /\ ( P ` ( k + 1 ) ) e. _V /\ ( P ` k ) =/= ( P ` ( k + 1 ) ) ) ) -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = ( I ` ( F ` k ) ) )
27 15 17 19 25 26 syl31anc 
 |-  ( ( ( ( ( G e. UPGraph /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ ( I ` ( F ` k ) ) e. ( Edg ` G ) ) /\ ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = ( I ` ( F ` k ) ) )
28 27 eqcomd 
 |-  ( ( ( ( ( G e. UPGraph /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) /\ ( I ` ( F ` k ) ) e. ( Edg ` G ) ) /\ ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) -> ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
29 28 exp31 
 |-  ( ( ( G e. UPGraph /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( I ` ( F ` k ) ) e. ( Edg ` G ) -> ( ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
30 14 29 mpd 
 |-  ( ( ( G e. UPGraph /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
31 30 com12 
 |-  ( ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> ( ( ( G e. UPGraph /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
32 10 31 jaoi 
 |-  ( ( ( ( P ` k ) = ( P ` ( k + 1 ) ) /\ ( I ` ( F ` k ) ) = { ( P ` k ) } ) \/ ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) -> ( ( ( G e. UPGraph /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
33 32 com12 
 |-  ( ( ( G e. UPGraph /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( ( P ` k ) = ( P ` ( k + 1 ) ) /\ ( I ` ( F ` k ) ) = { ( P ` k ) } ) \/ ( -. ( P ` k ) = ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) -> ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
34 4 33 biimtrid 
 |-  ( ( ( G e. UPGraph /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
35 ifpprsnss 
 |-  ( ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
36 34 35 impbid1 
 |-  ( ( ( G e. UPGraph /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) <-> ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
37 36 ralbidva 
 |-  ( ( G e. UPGraph /\ ( 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 ) ) ) <-> A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
38 37 pm5.32da 
 |-  ( G e. UPGraph -> ( ( ( 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. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
39 df-3an 
 |-  ( ( 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. 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 ) ) ) ) )
40 df-3an 
 |-  ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) <-> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
41 38 39 40 3bitr4g 
 |-  ( G e. UPGraph -> ( ( 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. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
42 3 41 bitrd 
 |-  ( G e. UPGraph -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )