Theorem wlkp1lem1

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

	Ref	Expression
Hypotheses	wlkp1.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	wlkp1.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
	wlkp1.f	$$⊢\phi \to \mathrm{Fun}I$$
	wlkp1.a	$$⊢\phi \to I\in \mathrm{Fin}$$
	wlkp1.b	$$⊢\phi \to B\in W$$
	wlkp1.c	$$⊢\phi \to C\in V$$
	wlkp1.d	$$⊢\phi \to \neg B\in \mathrm{dom}I$$
	wlkp1.w	$$⊢\phi \to F\mathrm{Walks}\left(G\right)P$$
	wlkp1.n	$$⊢N=\left|F\right|$$
Assertion	wlkp1lem1	$$⊢\phi \to \neg N+1\in \mathrm{dom}P$$

Proof

Step	Hyp	Ref	Expression
1		wlkp1.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		wlkp1.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
3		wlkp1.f	$$⊢\phi \to \mathrm{Fun}I$$
4		wlkp1.a	$$⊢\phi \to I\in \mathrm{Fin}$$
5		wlkp1.b	$$⊢\phi \to B\in W$$
6		wlkp1.c	$$⊢\phi \to C\in V$$
7		wlkp1.d	$$⊢\phi \to \neg B\in \mathrm{dom}I$$
8		wlkp1.w	$$⊢\phi \to F\mathrm{Walks}\left(G\right)P$$
9		wlkp1.n	$$⊢N=\left|F\right|$$
10		wlkcl	$$⊢F\mathrm{Walks}\left(G\right)P\to \left|F\right|\in {\mathbb{N}}_0$$
11	1	wlkp	$$⊢F\mathrm{Walks}\left(G\right)P\to P:\left(0\dots \left|F\right|\right)⟶V$$
12	10 11	jca	$$⊢F\mathrm{Walks}\left(G\right)P\to \left(\left|F\right|\in {\mathbb{N}}_0\wedge P:\left(0\dots \left|F\right|\right)⟶V\right)$$
13		fzp1nel	$$⊢\neg \left|F\right|+1\in \left(0\dots \left|F\right|\right)$$
14	13	a1i	$$⊢\left|F\right|\in {\mathbb{N}}_0\to \neg \left|F\right|+1\in \left(0\dots \left|F\right|\right)$$
15	9	oveq1i	$$⊢N+1=\left|F\right|+1$$
16	15	eleq1i	$$⊢N+1\in \left(0\dots \left|F\right|\right)\leftrightarrow \left|F\right|+1\in \left(0\dots \left|F\right|\right)$$
17	14 16	sylnibr	$$⊢\left|F\right|\in {\mathbb{N}}_0\to \neg N+1\in \left(0\dots \left|F\right|\right)$$
18		eleq2	$$⊢\mathrm{dom}P=\left(0\dots \left|F\right|\right)\to \left(N+1\in \mathrm{dom}P\leftrightarrow N+1\in \left(0\dots \left|F\right|\right)\right)$$
19	18	notbid	$$⊢\mathrm{dom}P=\left(0\dots \left|F\right|\right)\to \left(\neg N+1\in \mathrm{dom}P\leftrightarrow \neg N+1\in \left(0\dots \left|F\right|\right)\right)$$
20	17 19	syl5ibrcom	$$⊢\left|F\right|\in {\mathbb{N}}_0\to \left(\mathrm{dom}P=\left(0\dots \left|F\right|\right)\to \neg N+1\in \mathrm{dom}P\right)$$
21		fdm	$$⊢P:\left(0\dots \left|F\right|\right)⟶V\to \mathrm{dom}P=\left(0\dots \left|F\right|\right)$$
22	20 21	impel	$$⊢\left(\left|F\right|\in {\mathbb{N}}_0\wedge P:\left(0\dots \left|F\right|\right)⟶V\right)\to \neg N+1\in \mathrm{dom}P$$
23	8 12 22	3syl	$$⊢\phi \to \neg N+1\in \mathrm{dom}P$$