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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
upgr2wlk.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion upgr2wlk ( 𝐺 ∈ UPGraph → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ) ↔ ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) )

Proof

Step Hyp Ref Expression
1 upgr2wlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 upgr2wlk.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 1 2 upgriswlk ⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )
4 3 anbi1d ⊢ ( 𝐺 ∈ UPGraph → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ) ↔ ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ∧ ( ♯ ‘ 𝐹 ) = 2 ) ) )
5 iswrdb ⊢ ( 𝐹 ∈ Word dom 𝐼 ↔ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 )
6 oveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 2 ) )
7 6 feq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 ↔ 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ) )
8 5 7 syl5bb ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝐹 ∈ Word dom 𝐼 ↔ 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ) )
9 oveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ... 2 ) )
10 9 feq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ↔ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) )
11 fzo0to2pr ⊢ ( 0 ..^ 2 ) = { 0 , 1 }
12 6 11 eqtrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = { 0 , 1 } )
13 12 raleqdv ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ∀ 𝑘 ∈ { 0 , 1 } ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
14 2wlklem ⊢ ( ∀ 𝑘 ∈ { 0 , 1 } ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
15 13 14 bitrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) )
16 8 10 15 3anbi123d ⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ↔ ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) )
17 16 adantl ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ↔ ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) )
18 3anass ⊢ ( ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ↔ ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ∧ ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) )
19 17 18 bitrdi ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ↔ ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ∧ ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) ) )
20 19 ex ⊢ ( 𝐺 ∈ UPGraph → ( ( ♯ ‘ 𝐹 ) = 2 → ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ↔ ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ∧ ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) ) ) )
21 20 pm5.32rd ⊢ ( 𝐺 ∈ UPGraph → ( ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ∧ ( ♯ ‘ 𝐹 ) = 2 ) ↔ ( ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ∧ ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) ∧ ( ♯ ‘ 𝐹 ) = 2 ) ) )
22 3anass ⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ∧ ( ♯ ‘ 𝐹 ) = 2 ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ↔ ( ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ∧ ( ♯ ‘ 𝐹 ) = 2 ) ∧ ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) )
23 an32 ⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ∧ ( ♯ ‘ 𝐹 ) = 2 ) ∧ ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) ↔ ( ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ∧ ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) ∧ ( ♯ ‘ 𝐹 ) = 2 ) )
24 22 23 bitri ⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ∧ ( ♯ ‘ 𝐹 ) = 2 ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ↔ ( ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ∧ ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) ∧ ( ♯ ‘ 𝐹 ) = 2 ) )
25 21 24 bitr4di ⊢ ( 𝐺 ∈ UPGraph → ( ( ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ∧ ( ♯ ‘ 𝐹 ) = 2 ) ↔ ( ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ∧ ( ♯ ‘ 𝐹 ) = 2 ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) )
26 2nn0 ⊢ 2 ∈ ℕ0
27 fnfzo0hash ⊢ ( ( 2 ∈ ℕ0 ∧ 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ) → ( ♯ ‘ 𝐹 ) = 2 )
28 26 27 mpan ⊢ ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 → ( ♯ ‘ 𝐹 ) = 2 )
29 28 pm4.71i ⊢ ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ↔ ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ∧ ( ♯ ‘ 𝐹 ) = 2 ) )
30 29 bicomi ⊢ ( ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ∧ ( ♯ ‘ 𝐹 ) = 2 ) ↔ 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 )
31 30 a1i ⊢ ( 𝐺 ∈ UPGraph → ( ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ∧ ( ♯ ‘ 𝐹 ) = 2 ) ↔ 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ) )
32 31 3anbi1d ⊢ ( 𝐺 ∈ UPGraph → ( ( ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ∧ ( ♯ ‘ 𝐹 ) = 2 ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ↔ ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) )
33 4 25 32 3bitrd ⊢ ( 𝐺 ∈ UPGraph → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ) ↔ ( 𝐹 : ( 0 ..^ 2 ) ⟶ dom 𝐼 ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) )