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 ) ) } ⊆ ( 𝐼 ‘ ( 𝑓𝑘 ) ) ) ) } )