Theorem trlsegvdeglem1

Description: Lemma for trlsegvdeg . (Contributed by AV, 20-Feb-2021)

	Ref	Expression
Hypotheses	trlsegvdeg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	trlsegvdeg.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	trlsegvdeg.f	⊢ ( 𝜑 → Fun 𝐼 )
	trlsegvdeg.n	⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
	trlsegvdeg.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	trlsegvdeg.w	⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
Assertion	trlsegvdeglem1	⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝑁 ) ∈ 𝑉 ∧ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∈ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		trlsegvdeg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		trlsegvdeg.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3		trlsegvdeg.f	⊢ ( 𝜑 → Fun 𝐼 )
4		trlsegvdeg.n	⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
5		trlsegvdeg.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
6		trlsegvdeg.w	⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
7		trliswlk	⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
8	1	wlkpvtx	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) → ( 𝑃 ‘ 𝑁 ) ∈ 𝑉 ) )
9		elfzofz	⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
10	8 9	impel	⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 𝑁 ) ∈ 𝑉 )
11	1	wlkpvtx	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) → ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∈ 𝑉 ) )
12		fzofzp1	⊢ ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝑁 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
13	11 12	impel	⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∈ 𝑉 )
14	10 13	jca	⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑃 ‘ 𝑁 ) ∈ 𝑉 ∧ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∈ 𝑉 ) )
15	14	ex	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( 𝑃 ‘ 𝑁 ) ∈ 𝑉 ∧ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∈ 𝑉 ) ) )
16	6 7 15	3syl	⊢ ( 𝜑 → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( 𝑃 ‘ 𝑁 ) ∈ 𝑉 ∧ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∈ 𝑉 ) ) )
17	4 16	mpd	⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝑁 ) ∈ 𝑉 ∧ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ∈ 𝑉 ) )