Metamath Proof Explorer

Theorem iswlk

Description: Properties of a pair of functions to be a walk. (Contributed by AV, 30-Dec-2020)

Ref Expression
Hypotheses wksfval.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
wksfval.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion iswlk ( ( 𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 wksfval.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wksfval.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 df-br ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ⟨ 𝐹 , 𝑃 ⟩ ∈ ( Walks ‘ 𝐺 ) )
4 1 2 wksfval ⊢ ( 𝐺 ∈ 𝑊 → ( Walks ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } )
5 4 3ad2ant1 ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) → ( Walks ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } )
6 5 eleq2d ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) → ( ⟨ 𝐹 , 𝑃 ⟩ ∈ ( Walks ‘ 𝐺 ) ↔ ⟨ 𝐹 , 𝑃 ⟩ ∈ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } ) )
7 3 6 syl5bb ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ⟨ 𝐹 , 𝑃 ⟩ ∈ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } ) )
8 eleq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∈ Word dom 𝐼 ↔ 𝐹 ∈ Word dom 𝐼 ) )
9 8 adantr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝑓 ∈ Word dom 𝐼 ↔ 𝐹 ∈ Word dom 𝐼 ) )
10 simpr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → 𝑝 = 𝑃 )
11 fveq2 ⊢ ( 𝑓 = 𝐹 → ( ♯ ‘ 𝑓 ) = ( ♯ ‘ 𝐹 ) )
12 11 oveq2d ⊢ ( 𝑓 = 𝐹 → ( 0 ... ( ♯ ‘ 𝑓 ) ) = ( 0 ... ( ♯ ‘ 𝐹 ) ) )
13 12 adantr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 0 ... ( ♯ ‘ 𝑓 ) ) = ( 0 ... ( ♯ ‘ 𝐹 ) ) )
14 10 13 feq12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ↔ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) )
15 11 oveq2d ⊢ ( 𝑓 = 𝐹 → ( 0 ..^ ( ♯ ‘ 𝑓 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
16 15 adantr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 0 ..^ ( ♯ ‘ 𝑓 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
17 fveq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑘 ) )
18 fveq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
19 17 18 eqeq12d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) ↔ ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
20 19 adantl ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) ↔ ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
21 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
22 21 fveq2d ⊢ ( 𝑓 = 𝐹 → ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
23 17 sneqd ⊢ ( 𝑝 = 𝑃 → { ( 𝑝 ‘ 𝑘 ) } = { ( 𝑃 ‘ 𝑘 ) } )
24 22 23 eqeqan12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } ) )
25 17 18 preq12d ⊢ ( 𝑝 = 𝑃 → { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
26 25 adantl ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
27 22 adantr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
28 26 27 sseq12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ↔ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
29 20 24 28 ifpbi123d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ↔ if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
30 16 29 raleqbidv ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ↔ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
31 9 14 30 3anbi123d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
32 31 opelopabga ⊢ ( ( 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) → ( ⟨ 𝐹 , 𝑃 ⟩ ∈ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
33 32 3adant1 ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) → ( ⟨ 𝐹 , 𝑃 ⟩ ∈ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
34 7 33 bitrd ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )