This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem upgrwlkvtxedg

Description: The pairs of connected vertices of a walk are edges in a pseudograph. (Contributed by Alexander van der Vekens, 22-Jul-2018) (Revised by AV, 2-Jan-2021)

Ref Expression
Hypothesis wlkvtxedg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion upgrwlkvtxedg ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 )

Proof

Step Hyp Ref Expression
1 wlkvtxedg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
2 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
4 2 3 upgriswlk ⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )
5 3 1 upgredginwlk ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ 𝐸 ) )
6 5 ancoms ⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝐺 ∈ UPGraph ) → ( 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ 𝐸 ) )
7 6 imp ⊢ ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ 𝐸 )
8 eleq1 ⊢ ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ 𝐸 ) )
9 8 eqcoms ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ 𝐸 ) )
10 7 9 syl5ibrcom ⊢ ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ) )
11 10 ralimdva ⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝐺 ∈ UPGraph ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ) )
12 11 impancom ⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) → ( 𝐺 ∈ UPGraph → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ) )
13 12 3adant2 ⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) → ( 𝐺 ∈ UPGraph → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ) )
14 13 com12 ⊢ ( 𝐺 ∈ UPGraph → ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ) )
15 4 14 sylbid ⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 ) )
16 15 imp ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ∈ 𝐸 )