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