Metamath Proof Explorer


Theorem upgrwlkupwlk

Description: In a pseudograph, a walk is a simple walk. (Contributed by AV, 30-Dec-2020) (Proof shortened by AV, 2-Jan-2021)

Ref Expression
Assertion upgrwlkupwlk ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 )

Proof

Step Hyp Ref Expression
1 wlkv ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
2 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3 eqid ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
4 2 3 iswlk ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ) ) )
5 simpr1 ( ( ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ) ) → 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) )
6 simpr2 ( ( ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ) ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
7 df-ifp ( if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ↔ ( ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } ) ∨ ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ) )
8 dfsn2 { ( 𝑃𝑘 ) } = { ( 𝑃𝑘 ) , ( 𝑃𝑘 ) }
9 preq2 ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) → { ( 𝑃𝑘 ) , ( 𝑃𝑘 ) } = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
10 8 9 syl5eq ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) → { ( 𝑃𝑘 ) } = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
11 10 eqeq2d ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
12 11 biimpa ( ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
13 12 a1d ( ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } ) → ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
14 simpr ( ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) → 𝐺 ∈ UPGraph )
15 simpl ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) )
16 eqid ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
17 3 16 upgredginwlk ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) ) )
18 14 15 17 syl2anr ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ) → ( 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) ) )
19 18 imp ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) )
20 simprr ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ) → 𝐺 ∈ UPGraph )
21 20 adantr ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝐺 ∈ UPGraph )
22 21 adantr ( ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) ) → 𝐺 ∈ UPGraph )
23 22 adantr ( ( ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ) → 𝐺 ∈ UPGraph )
24 simplr ( ( ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) )
25 simprr ( ( ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ) → { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) )
26 df-ne ( ( 𝑃𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ↔ ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
27 fvexd ( ( 𝑃𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) → ( 𝑃𝑘 ) ∈ V )
28 fvexd ( ( 𝑃𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ V )
29 id ( ( 𝑃𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) → ( 𝑃𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
30 27 28 29 3jca ( ( 𝑃𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) → ( ( 𝑃𝑘 ) ∈ V ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ V ∧ ( 𝑃𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
31 26 30 sylbir ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) → ( ( 𝑃𝑘 ) ∈ V ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ V ∧ ( 𝑃𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
32 31 adantr ( ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) → ( ( 𝑃𝑘 ) ∈ V ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ V ∧ ( 𝑃𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
33 32 adantl ( ( ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ) → ( ( 𝑃𝑘 ) ∈ V ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ V ∧ ( 𝑃𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
34 2 16 upgredgpr ( ( ( 𝐺 ∈ UPGraph ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ∧ ( ( 𝑃𝑘 ) ∈ V ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ V ∧ ( 𝑃𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) → { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) )
35 23 24 25 33 34 syl31anc ( ( ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ) → { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) )
36 35 eqcomd ( ( ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
37 36 exp31 ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) → ( ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )
38 19 37 mpd ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
39 38 com12 ( ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) → ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
40 13 39 jaoi ( ( ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } ) ∨ ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ) → ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
41 40 com12 ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } ) ∨ ( ¬ ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
42 7 41 syl5bi ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
43 42 ralimdva ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
44 43 ex ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )
45 44 com23 ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) → ( ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )
46 45 3impia ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ) → ( ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
47 46 impcom ( ( ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ) ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
48 5 6 47 3jca ( ( ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ∧ 𝐺 ∈ UPGraph ) ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ) ) → ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
49 48 exp31 ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝐺 ∈ UPGraph → ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ) → ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) ) )
50 49 com23 ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) ) ) → ( 𝐺 ∈ UPGraph → ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) ) )
51 4 50 sylbid ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ UPGraph → ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) ) )
52 51 impd ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃𝐺 ∈ UPGraph ) → ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )
53 52 impcom ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃𝐺 ∈ UPGraph ) ∧ ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) )
54 2 3 isupwlk ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )
55 54 adantl ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃𝐺 ∈ UPGraph ) ∧ ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )
56 53 55 mpbird ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃𝐺 ∈ UPGraph ) ∧ ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 )
57 56 exp31 ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ UPGraph → ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 ) ) )
58 1 57 mpid ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ UPGraph → 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 ) )
59 58 impcom ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 )