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 ) ) } ) } )