Theorem wlkp1lem1

Description: Lemma for wlkp1 . (Contributed by AV, 6-Mar-2021)

	Ref	Expression
Hypotheses	wlkp1.v	|- V = ( Vtx ` G )
	wlkp1.i	|- I = ( iEdg ` G )
	wlkp1.f	|- ( ph -> Fun I )
	wlkp1.a	|- ( ph -> I e. Fin )
	wlkp1.b	|- ( ph -> B e. W )
	wlkp1.c	|- ( ph -> C e. V )
	wlkp1.d	|- ( ph -> -. B e. dom I )
	wlkp1.w	|- ( ph -> F ( Walks ` G ) P )
	wlkp1.n	|- N = ( # ` F )
Assertion	wlkp1lem1	|- ( ph -> -. ( N + 1 ) e. dom P )

Proof

Step	Hyp	Ref	Expression
1		wlkp1.v	|- V = ( Vtx ` G )
2		wlkp1.i	|- I = ( iEdg ` G )
3		wlkp1.f	|- ( ph -> Fun I )
4		wlkp1.a	|- ( ph -> I e. Fin )
5		wlkp1.b	|- ( ph -> B e. W )
6		wlkp1.c	|- ( ph -> C e. V )
7		wlkp1.d	|- ( ph -> -. B e. dom I )
8		wlkp1.w	|- ( ph -> F ( Walks ` G ) P )
9		wlkp1.n	|- N = ( # ` F )
10		wlkcl	|- ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
11	1	wlkp	|- ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> V )
12	10 11	jca	|- ( F ( Walks ` G ) P -> ( ( # ` F ) e. NN0 /\ P : ( 0 ... ( # ` F ) ) --> V ) )
13		fzp1nel	|- -. ( ( # ` F ) + 1 ) e. ( 0 ... ( # ` F ) )
14	13	a1i	|- ( ( # ` F ) e. NN0 -> -. ( ( # ` F ) + 1 ) e. ( 0 ... ( # ` F ) ) )
15	9	oveq1i	|- ( N + 1 ) = ( ( # ` F ) + 1 )
16	15	eleq1i	|- ( ( N + 1 ) e. ( 0 ... ( # ` F ) ) <-> ( ( # ` F ) + 1 ) e. ( 0 ... ( # ` F ) ) )
17	14 16	sylnibr	|- ( ( # ` F ) e. NN0 -> -. ( N + 1 ) e. ( 0 ... ( # ` F ) ) )
18		eleq2	|- ( dom P = ( 0 ... ( # ` F ) ) -> ( ( N + 1 ) e. dom P <-> ( N + 1 ) e. ( 0 ... ( # ` F ) ) ) )
19	18	notbid	|- ( dom P = ( 0 ... ( # ` F ) ) -> ( -. ( N + 1 ) e. dom P <-> -. ( N + 1 ) e. ( 0 ... ( # ` F ) ) ) )
20	17 19	syl5ibrcom	|- ( ( # ` F ) e. NN0 -> ( dom P = ( 0 ... ( # ` F ) ) -> -. ( N + 1 ) e. dom P ) )
21		fdm	|- ( P : ( 0 ... ( # ` F ) ) --> V -> dom P = ( 0 ... ( # ` F ) ) )
22	20 21	impel	|- ( ( ( # ` F ) e. NN0 /\ P : ( 0 ... ( # ` F ) ) --> V ) -> -. ( N + 1 ) e. dom P )
23	8 12 22	3syl	|- ( ph -> -. ( N + 1 ) e. dom P )