Metamath Proof Explorer

Theorem upgr2wlk

Description: Properties of a pair of functions to be a walk of length 2 in a pseudograph. Note that the vertices need not to be distinct and the edges can be loops or multiedges. (Contributed by Alexander van der Vekens, 16-Feb-2018) (Revised by AV, 3-Jan-2021) (Revised by AV, 28-Oct-2021)

Ref Expression
Hypotheses upgr2wlk.v 
|- V = ( Vtx ` G )
upgr2wlk.i 
|- I = ( iEdg ` G )
Assertion upgr2wlk 
|- ( G e. UPGraph -> ( ( F ( Walks ` G ) P /\ ( # ` F ) = 2 ) <-> ( F : ( 0 ..^ 2 ) --> dom I /\ P : ( 0 ... 2 ) --> V /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) ) )

Proof

Step Hyp Ref Expression
1 upgr2wlk.v 
 |-  V = ( Vtx ` G )
2 upgr2wlk.i 
 |-  I = ( iEdg ` G )
3 1 2 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 ) ) } ) ) )
4 3 anbi1d 
 |-  ( G e. UPGraph -> ( ( F ( Walks ` G ) P /\ ( # ` F ) = 2 ) <-> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) /\ ( # ` F ) = 2 ) ) )
5 iswrdb 
 |-  ( F e. Word dom I <-> F : ( 0 ..^ ( # ` F ) ) --> dom I )
6 oveq2 
 |-  ( ( # ` F ) = 2 -> ( 0 ..^ ( # ` F ) ) = ( 0 ..^ 2 ) )
7 6 feq2d 
 |-  ( ( # ` F ) = 2 -> ( F : ( 0 ..^ ( # ` F ) ) --> dom I <-> F : ( 0 ..^ 2 ) --> dom I ) )
8 5 7 bitrid 
 |-  ( ( # ` F ) = 2 -> ( F e. Word dom I <-> F : ( 0 ..^ 2 ) --> dom I ) )
9 oveq2 
 |-  ( ( # ` F ) = 2 -> ( 0 ... ( # ` F ) ) = ( 0 ... 2 ) )
10 9 feq2d 
 |-  ( ( # ` F ) = 2 -> ( P : ( 0 ... ( # ` F ) ) --> V <-> P : ( 0 ... 2 ) --> V ) )
11 fzo0to2pr 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
12 6 11 eqtrdi 
 |-  ( ( # ` F ) = 2 -> ( 0 ..^ ( # ` F ) ) = { 0 , 1 } )
13 12 raleqdv 
 |-  ( ( # ` F ) = 2 -> ( A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } <-> A. k e. { 0 , 1 } ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
14 2wlklem 
 |-  ( A. k e. { 0 , 1 } ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } <-> ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) )
15 13 14 bitrdi 
 |-  ( ( # ` F ) = 2 -> ( A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } <-> ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) )
16 8 10 15 3anbi123d 
 |-  ( ( # ` F ) = 2 -> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) <-> ( F : ( 0 ..^ 2 ) --> dom I /\ P : ( 0 ... 2 ) --> V /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) ) )
17 16 adantl 
 |-  ( ( G e. UPGraph /\ ( # ` F ) = 2 ) -> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) <-> ( F : ( 0 ..^ 2 ) --> dom I /\ P : ( 0 ... 2 ) --> V /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) ) )
18 3anass 
 |-  ( ( F : ( 0 ..^ 2 ) --> dom I /\ P : ( 0 ... 2 ) --> V /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) <-> ( F : ( 0 ..^ 2 ) --> dom I /\ ( P : ( 0 ... 2 ) --> V /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) ) )
19 17 18 bitrdi 
 |-  ( ( G e. UPGraph /\ ( # ` F ) = 2 ) -> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) <-> ( F : ( 0 ..^ 2 ) --> dom I /\ ( P : ( 0 ... 2 ) --> V /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) ) ) )
20 19 ex 
 |-  ( G e. UPGraph -> ( ( # ` F ) = 2 -> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) <-> ( F : ( 0 ..^ 2 ) --> dom I /\ ( P : ( 0 ... 2 ) --> V /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) ) ) ) )
21 20 pm5.32rd 
 |-  ( G e. UPGraph -> ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) /\ ( # ` F ) = 2 ) <-> ( ( F : ( 0 ..^ 2 ) --> dom I /\ ( P : ( 0 ... 2 ) --> V /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) ) /\ ( # ` F ) = 2 ) ) )
22 3anass 
 |-  ( ( ( F : ( 0 ..^ 2 ) --> dom I /\ ( # ` F ) = 2 ) /\ P : ( 0 ... 2 ) --> V /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) <-> ( ( F : ( 0 ..^ 2 ) --> dom I /\ ( # ` F ) = 2 ) /\ ( P : ( 0 ... 2 ) --> V /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) ) )
23 an32 
 |-  ( ( ( F : ( 0 ..^ 2 ) --> dom I /\ ( # ` F ) = 2 ) /\ ( P : ( 0 ... 2 ) --> V /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) ) <-> ( ( F : ( 0 ..^ 2 ) --> dom I /\ ( P : ( 0 ... 2 ) --> V /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) ) /\ ( # ` F ) = 2 ) )
24 22 23 bitri 
 |-  ( ( ( F : ( 0 ..^ 2 ) --> dom I /\ ( # ` F ) = 2 ) /\ P : ( 0 ... 2 ) --> V /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) <-> ( ( F : ( 0 ..^ 2 ) --> dom I /\ ( P : ( 0 ... 2 ) --> V /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) ) /\ ( # ` F ) = 2 ) )
25 21 24 bitr4di 
 |-  ( G e. UPGraph -> ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) /\ ( # ` F ) = 2 ) <-> ( ( F : ( 0 ..^ 2 ) --> dom I /\ ( # ` F ) = 2 ) /\ P : ( 0 ... 2 ) --> V /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) ) )
26 2nn0 
 |-  2 e. NN0
27 fnfzo0hash 
 |-  ( ( 2 e. NN0 /\ F : ( 0 ..^ 2 ) --> dom I ) -> ( # ` F ) = 2 )
28 26 27 mpan 
 |-  ( F : ( 0 ..^ 2 ) --> dom I -> ( # ` F ) = 2 )
29 28 pm4.71i 
 |-  ( F : ( 0 ..^ 2 ) --> dom I <-> ( F : ( 0 ..^ 2 ) --> dom I /\ ( # ` F ) = 2 ) )
30 29 bicomi 
 |-  ( ( F : ( 0 ..^ 2 ) --> dom I /\ ( # ` F ) = 2 ) <-> F : ( 0 ..^ 2 ) --> dom I )
31 30 a1i 
 |-  ( G e. UPGraph -> ( ( F : ( 0 ..^ 2 ) --> dom I /\ ( # ` F ) = 2 ) <-> F : ( 0 ..^ 2 ) --> dom I ) )
32 31 3anbi1d 
 |-  ( G e. UPGraph -> ( ( ( F : ( 0 ..^ 2 ) --> dom I /\ ( # ` F ) = 2 ) /\ P : ( 0 ... 2 ) --> V /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) <-> ( F : ( 0 ..^ 2 ) --> dom I /\ P : ( 0 ... 2 ) --> V /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) ) )
33 4 25 32 3bitrd 
 |-  ( G e. UPGraph -> ( ( F ( Walks ` G ) P /\ ( # ` F ) = 2 ) <-> ( F : ( 0 ..^ 2 ) --> dom I /\ P : ( 0 ... 2 ) --> V /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) ) )