Theorem trlsegvdeglem1

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

	Ref	Expression
Hypotheses	trlsegvdeg.v	|- V = ( Vtx ` G )
	trlsegvdeg.i	|- I = ( iEdg ` G )
	trlsegvdeg.f	|- ( ph -> Fun I )
	trlsegvdeg.n	|- ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
	trlsegvdeg.u	|- ( ph -> U e. V )
	trlsegvdeg.w	|- ( ph -> F ( Trails ` G ) P )
Assertion	trlsegvdeglem1	|- ( ph -> ( ( P ` N ) e. V /\ ( P ` ( N + 1 ) ) e. V ) )

Proof

Step	Hyp	Ref	Expression
1		trlsegvdeg.v	|- V = ( Vtx ` G )
2		trlsegvdeg.i	|- I = ( iEdg ` G )
3		trlsegvdeg.f	|- ( ph -> Fun I )
4		trlsegvdeg.n	|- ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
5		trlsegvdeg.u	|- ( ph -> U e. V )
6		trlsegvdeg.w	|- ( ph -> F ( Trails ` G ) P )
7		trliswlk	|- ( F ( Trails ` G ) P -> F ( Walks ` G ) P )
8	1	wlkpvtx	|- ( F ( Walks ` G ) P -> ( N e. ( 0 ... ( # ` F ) ) -> ( P ` N ) e. V ) )
9		elfzofz	|- ( N e. ( 0 ..^ ( # ` F ) ) -> N e. ( 0 ... ( # ` F ) ) )
10	8 9	impel	|- ( ( F ( Walks ` G ) P /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( P ` N ) e. V )
11	1	wlkpvtx	|- ( F ( Walks ` G ) P -> ( ( N + 1 ) e. ( 0 ... ( # ` F ) ) -> ( P ` ( N + 1 ) ) e. V ) )
12		fzofzp1	|- ( N e. ( 0 ..^ ( # ` F ) ) -> ( N + 1 ) e. ( 0 ... ( # ` F ) ) )
13	11 12	impel	|- ( ( F ( Walks ` G ) P /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( P ` ( N + 1 ) ) e. V )
14	10 13	jca	|- ( ( F ( Walks ` G ) P /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( P ` N ) e. V /\ ( P ` ( N + 1 ) ) e. V ) )
15	14	ex	|- ( F ( Walks ` G ) P -> ( N e. ( 0 ..^ ( # ` F ) ) -> ( ( P ` N ) e. V /\ ( P ` ( N + 1 ) ) e. V ) ) )
16	6 7 15	3syl	|- ( ph -> ( N e. ( 0 ..^ ( # ` F ) ) -> ( ( P ` N ) e. V /\ ( P ` ( N + 1 ) ) e. V ) ) )
17	4 16	mpd	|- ( ph -> ( ( P ` N ) e. V /\ ( P ` ( N + 1 ) ) e. V ) )