Metamath Proof Explorer

Theorem wksfval

Description: The set of walks (in an undirected graph). (Contributed by AV, 30-Dec-2020)

Ref Expression
Hypotheses wksfval.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
wksfval.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion wksfval ( 𝐺 ∈ 𝑊 → ( Walks ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } )

Proof

Step Hyp Ref Expression
1 wksfval.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 wksfval.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 df-wlks ⊢ Walks = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝑔 ) ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝑔 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } )
4 fveq2 ⊢ ( 𝑔 = 𝐺 → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) )
5 4 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( iEdg ‘ 𝑔 ) = 𝐼 )
6 5 dmeqd ⊢ ( 𝑔 = 𝐺 → dom ( iEdg ‘ 𝑔 ) = dom 𝐼 )
7 wrdeq ⊢ ( dom ( iEdg ‘ 𝑔 ) = dom 𝐼 → Word dom ( iEdg ‘ 𝑔 ) = Word dom 𝐼 )
8 6 7 syl ⊢ ( 𝑔 = 𝐺 → Word dom ( iEdg ‘ 𝑔 ) = Word dom 𝐼 )
9 8 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑓 ∈ Word dom ( iEdg ‘ 𝑔 ) ↔ 𝑓 ∈ Word dom 𝐼 ) )
10 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
11 10 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = 𝑉 )
12 11 feq3d ⊢ ( 𝑔 = 𝐺 → ( 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝑔 ) ↔ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ) )
13 5 fveq1d ⊢ ( 𝑔 = 𝐺 → ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) )
14 13 eqeq1d ⊢ ( 𝑔 = 𝐺 → ( ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } ↔ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } ) )
15 13 sseq2d ⊢ ( 𝑔 = 𝐺 → ( { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ↔ { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) )
16 14 15 ifpbi23d ⊢ ( 𝑔 = 𝐺 → ( if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ↔ if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) )
17 16 ralbidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ↔ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) )
18 9 12 17 3anbi123d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑓 ∈ Word dom ( iEdg ‘ 𝑔 ) ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝑔 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ↔ ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) )
19 18 opabbidv ⊢ ( 𝑔 = 𝐺 → { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝑔 ) ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝑔 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } )
20 elex ⊢ ( 𝐺 ∈ 𝑊 → 𝐺 ∈ V )
21 3anass ⊢ ( ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ↔ ( 𝑓 ∈ Word dom 𝐼 ∧ ( 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) )
22 21 opabbii ⊢ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ ( 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) }
23 2 fvexi ⊢ 𝐼 ∈ V
24 23 dmex ⊢ dom 𝐼 ∈ V
25 wrdexg ⊢ ( dom 𝐼 ∈ V → Word dom 𝐼 ∈ V )
26 24 25 mp1i ⊢ ( 𝐺 ∈ 𝑊 → Word dom 𝐼 ∈ V )
27 ovex ⊢ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∈ V
28 1 fvexi ⊢ 𝑉 ∈ V
29 28 a1i ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑓 ∈ Word dom 𝐼 ) → 𝑉 ∈ V )
30 mapex ⊢ ( ( ( 0 ... ( ♯ ‘ 𝑓 ) ) ∈ V ∧ 𝑉 ∈ V ) → { 𝑝 ∣ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 } ∈ V )
31 27 29 30 sylancr ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑓 ∈ Word dom 𝐼 ) → { 𝑝 ∣ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 } ∈ V )
32 simpl ⊢ ( ( 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) → 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 )
33 32 ss2abi ⊢ { 𝑝 ∣ ( 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } ⊆ { 𝑝 ∣ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 }
34 33 a1i ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑓 ∈ Word dom 𝐼 ) → { 𝑝 ∣ ( 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } ⊆ { 𝑝 ∣ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 } )
35 31 34 ssexd ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑓 ∈ Word dom 𝐼 ) → { 𝑝 ∣ ( 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } ∈ V )
36 26 35 opabex3d ⊢ ( 𝐺 ∈ 𝑊 → { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ ( 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } ∈ V )
37 22 36 eqeltrid ⊢ ( 𝐺 ∈ 𝑊 → { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } ∈ V )
38 3 19 20 37 fvmptd3 ⊢ ( 𝐺 ∈ 𝑊 → ( Walks ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) if- ( ( 𝑝 ‘ 𝑘 ) = ( 𝑝 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) } , { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) } )