Metamath Proof Explorer


Theorem upwlksfval

Description: The set of simple walks (in an undirected graph). (Contributed by Alexander van der Vekens, 19-Oct-2017) (Revised by AV, 28-Dec-2020)

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

Proof

Step Hyp Ref Expression
1 upwlksfval.v 𝑉 = ( Vtx ‘ 𝐺 )
2 upwlksfval.i 𝐼 = ( iEdg ‘ 𝐺 )
3 df-upwlks UPWalks = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝑔 ) ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝑔 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } )
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 ‘ 𝑔 ) ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ↔ ( 𝐼 ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) )
15 14 ralbidv ( 𝑔 = 𝐺 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ↔ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) )
16 9 12 15 3anbi123d ( 𝑔 = 𝐺 → ( ( 𝑓 ∈ Word dom ( iEdg ‘ 𝑔 ) ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝑔 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) ↔ ( 𝑓 ∈ Word dom 𝐼𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) ) )
17 16 opabbidv ( 𝑔 = 𝐺 → { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom ( iEdg ‘ 𝑔 ) ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝑔 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( ( iEdg ‘ 𝑔 ) ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } )
18 elex ( 𝐺𝑊𝐺 ∈ V )
19 3anass ( ( 𝑓 ∈ Word dom 𝐼𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) ↔ ( 𝑓 ∈ Word dom 𝐼 ∧ ( 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) ) )
20 19 opabbii { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ ( 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) ) }
21 2 fvexi 𝐼 ∈ V
22 21 dmex dom 𝐼 ∈ V
23 wrdexg ( dom 𝐼 ∈ V → Word dom 𝐼 ∈ V )
24 22 23 mp1i ( 𝐺𝑊 → Word dom 𝐼 ∈ V )
25 ovex ( 0 ... ( ♯ ‘ 𝑓 ) ) ∈ V
26 1 fvexi 𝑉 ∈ V
27 26 a1i ( ( 𝐺𝑊𝑓 ∈ Word dom 𝐼 ) → 𝑉 ∈ V )
28 mapex ( ( ( 0 ... ( ♯ ‘ 𝑓 ) ) ∈ V ∧ 𝑉 ∈ V ) → { 𝑝𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 } ∈ V )
29 25 27 28 sylancr ( ( 𝐺𝑊𝑓 ∈ Word dom 𝐼 ) → { 𝑝𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 } ∈ V )
30 simpl ( ( 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) → 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 )
31 30 ss2abi { 𝑝 ∣ ( 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } ⊆ { 𝑝𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 }
32 31 a1i ( ( 𝐺𝑊𝑓 ∈ Word dom 𝐼 ) → { 𝑝 ∣ ( 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } ⊆ { 𝑝𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 } )
33 29 32 ssexd ( ( 𝐺𝑊𝑓 ∈ Word dom 𝐼 ) → { 𝑝 ∣ ( 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } ∈ V )
34 24 33 opabex3d ( 𝐺𝑊 → { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ ( 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) ) } ∈ V )
35 20 34 eqeltrid ( 𝐺𝑊 → { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } ∈ V )
36 3 17 18 35 fvmptd3 ( 𝐺𝑊 → ( UPWalks ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ∈ Word dom 𝐼𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓𝑘 ) ) = { ( 𝑝𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } )