Metamath Proof Explorer


Theorem upgriswlk

Description: Properties of a pair of functions to be a walk in a pseudograph. (Contributed by AV, 2-Jan-2021) (Revised by AV, 28-Oct-2021)

Ref Expression
Hypotheses upgriswlk.v 𝑉 = ( Vtx ‘ 𝐺 )
upgriswlk.i 𝐼 = ( iEdg ‘ 𝐺 )
Assertion upgriswlk ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )

Proof

Step Hyp Ref Expression
1 upgriswlk.v 𝑉 = ( Vtx ‘ 𝐺 )
2 upgriswlk.i 𝐼 = ( iEdg ‘ 𝐺 )
3 1 2 iswlkg ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) ) )
4 df-ifp ( if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ↔ ( ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } ) ∨ ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) )
5 dfsn2 { ( 𝑃𝑘 ) } = { ( 𝑃𝑘 ) , ( 𝑃𝑘 ) }
6 preq2 ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) → { ( 𝑃𝑘 ) , ( 𝑃𝑘 ) } = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
7 5 6 syl5eq ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) → { ( 𝑃𝑘 ) } = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
8 7 eqeq2d ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) → ( ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } ↔ ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
9 8 biimpa ( ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } ) → ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
10 9 a1d ( ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } ) → ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
11 eqid ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
12 2 11 upgredginwlk ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ∈ Word dom 𝐼 ) → ( 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼 ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) ) )
13 12 adantrr ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ) → ( 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼 ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) ) )
14 13 imp ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐼 ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) )
15 simp-4l ( ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) → 𝐺 ∈ UPGraph )
16 simpr ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) ) → ( 𝐼 ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) )
17 16 adantr ( ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) → ( 𝐼 ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) )
18 simpr ( ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) → { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) )
19 18 adantl ( ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) → { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) )
20 fvexd ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) → ( 𝑃𝑘 ) ∈ V )
21 fvexd ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ V )
22 neqne ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) → ( 𝑃𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
23 20 21 22 3jca ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) → ( ( 𝑃𝑘 ) ∈ V ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ V ∧ ( 𝑃𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
24 23 adantr ( ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) → ( ( 𝑃𝑘 ) ∈ V ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ V ∧ ( 𝑃𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
25 24 adantl ( ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) → ( ( 𝑃𝑘 ) ∈ V ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ V ∧ ( 𝑃𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
26 1 11 upgredgpr ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ∧ ( ( 𝑃𝑘 ) ∈ V ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ V ∧ ( 𝑃𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = ( 𝐼 ‘ ( 𝐹𝑘 ) ) )
27 15 17 19 25 26 syl31anc ( ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) → { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = ( 𝐼 ‘ ( 𝐹𝑘 ) ) )
28 27 eqcomd ( ( ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) → ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
29 28 exp31 ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐼 ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) → ( ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) → ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )
30 14 29 mpd ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) → ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
31 30 com12 ( ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) → ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
32 10 31 jaoi ( ( ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } ) ∨ ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) → ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
33 32 com12 ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } ) ∨ ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) → ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
34 4 33 syl5bi ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) → ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
35 ifpprsnss ( ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } → if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) )
36 34 35 impbid1 ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ↔ ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
37 36 ralbidva ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ↔ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
38 37 pm5.32da ( 𝐺 ∈ UPGraph → ( ( ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) ↔ ( ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )
39 df-3an ( ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) ↔ ( ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) )
40 df-3an ( ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ↔ ( ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
41 38 39 40 3bitr4g ( 𝐺 ∈ UPGraph → ( ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) ↔ ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )
42 3 41 bitrd ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )