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

Metamath Proof Explorer

Theorem wlkvtxiedg

Description: The vertices of a walk are connected by indexed edges. (Contributed by Alexander van der Vekens, 22-Jul-2018) (Revised by AV, 2-Jan-2021) (Proof shortened by AV, 4-Apr-2021)

Ref Expression
Hypothesis wlkvtxeledg.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion wlkvtxiedg ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∃ 𝑒 ∈ ran 𝐼 { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ 𝑒 )

Proof

Step Hyp Ref Expression
1 wlkvtxeledg.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2 1 wlkvtxeledg ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
3 fvex ⊢ ( 𝑃 ‘ 𝑘 ) ∈ V
4 3 prnz ⊢ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ≠ ∅
5 ssn0 ⊢ ( ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ∧ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ≠ ∅ ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ≠ ∅ )
6 4 5 mpan2 ⊢ ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ≠ ∅ )
7 6 adantl ⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ≠ ∅ )
8 fvn0fvelrn ⊢ ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ≠ ∅ → ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ran 𝐼 )
9 7 8 syl ⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ran 𝐼 )
10 sseq2 ⊢ ( 𝑒 = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ 𝑒 ↔ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
11 10 adantl ⊢ ( ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ∧ 𝑒 = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ 𝑒 ↔ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
12 simpr ⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
13 9 11 12 rspcedvd ⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ∃ 𝑒 ∈ ran 𝐼 { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ 𝑒 )
14 13 ex ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) → ∃ 𝑒 ∈ ran 𝐼 { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ 𝑒 ) )
15 14 ralimdva ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∃ 𝑒 ∈ ran 𝐼 { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ 𝑒 ) )
16 2 15 mpd ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∃ 𝑒 ∈ ran 𝐼 { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ 𝑒 )