Theorem wlkp1lem2

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|$$
	wlkp1.e	$$⊢\phi \to E\in \mathrm{Edg}\left(G\right)$$
	wlkp1.x	$$⊢\phi \to \left\{P\left(N\right),C\right\}\subseteq E$$
	wlkp1.u	$$⊢\phi \to \mathrm{iEdg}\left(S\right)=I\cup \left\{⟨B,E⟩\right\}$$
	wlkp1.h	$$⊢H=F\cup \left\{⟨N,B⟩\right\}$$
Assertion	wlkp1lem2	$$⊢\phi \to \left|H\right|=N+1$$

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		wlkp1.e	$$⊢\phi \to E\in \mathrm{Edg}\left(G\right)$$
11		wlkp1.x	$$⊢\phi \to \left\{P\left(N\right),C\right\}\subseteq E$$
12		wlkp1.u	$$⊢\phi \to \mathrm{iEdg}\left(S\right)=I\cup \left\{⟨B,E⟩\right\}$$
13		wlkp1.h	$$⊢H=F\cup \left\{⟨N,B⟩\right\}$$
14	13	fveq2i	$$⊢\left|H\right|=\left|F\cup \left\{⟨N,B⟩\right\}\right|$$
15	14	a1i	$$⊢\phi \to \left|H\right|=\left|F\cup \left\{⟨N,B⟩\right\}\right|$$
16		opex	$$⊢⟨N,B⟩\in \mathrm{V}$$
17	2	wlkf	$$⊢F\mathrm{Walks}\left(G\right)P\to F\in \mathrm{Word}\mathrm{dom}I$$
18		wrdfin	$$⊢F\in \mathrm{Word}\mathrm{dom}I\to F\in \mathrm{Fin}$$
19	8 17 18	3syl	$$⊢\phi \to F\in \mathrm{Fin}$$
20		fzonel	$$⊢\neg \left|F\right|\in \left(0..^\left|F\right|\right)$$
21	20	a1i	$$⊢\phi \to \neg \left|F\right|\in \left(0..^\left|F\right|\right)$$
22		eleq1	$$⊢N=\left|F\right|\to \left(N\in \left(0..^\left|F\right|\right)\leftrightarrow \left|F\right|\in \left(0..^\left|F\right|\right)\right)$$
23	22	notbid	$$⊢N=\left|F\right|\to \left(\neg N\in \left(0..^\left|F\right|\right)\leftrightarrow \neg \left|F\right|\in \left(0..^\left|F\right|\right)\right)$$
24	21 23	syl5ibr	$$⊢N=\left|F\right|\to \left(\phi \to \neg N\in \left(0..^\left|F\right|\right)\right)$$
25	9 24	ax-mp	$$⊢\phi \to \neg N\in \left(0..^\left|F\right|\right)$$
26		wrdfn	$$⊢F\in \mathrm{Word}\mathrm{dom}I\to FFn\left(0..^\left|F\right|\right)$$
27	8 17 26	3syl	$$⊢\phi \to FFn\left(0..^\left|F\right|\right)$$
28		fnop	$$⊢\left(FFn\left(0..^\left|F\right|\right)\wedge ⟨N,B⟩\in F\right)\to N\in \left(0..^\left|F\right|\right)$$
29	28	ex	$$⊢FFn\left(0..^\left|F\right|\right)\to \left(⟨N,B⟩\in F\to N\in \left(0..^\left|F\right|\right)\right)$$
30	27 29	syl	$$⊢\phi \to \left(⟨N,B⟩\in F\to N\in \left(0..^\left|F\right|\right)\right)$$
31	25 30	mtod	$$⊢\phi \to \neg ⟨N,B⟩\in F$$
32	19 31	jca	$$⊢\phi \to \left(F\in \mathrm{Fin}\wedge \neg ⟨N,B⟩\in F\right)$$
33		hashunsng	$$⊢⟨N,B⟩\in \mathrm{V}\to \left(\left(F\in \mathrm{Fin}\wedge \neg ⟨N,B⟩\in F\right)\to \left|F\cup \left\{⟨N,B⟩\right\}\right|=\left|F\right|+1\right)$$
34	16 32 33	mpsyl	$$⊢\phi \to \left|F\cup \left\{⟨N,B⟩\right\}\right|=\left|F\right|+1$$
35	9	eqcomi	$$⊢\left|F\right|=N$$
36	35	a1i	$$⊢\phi \to \left|F\right|=N$$
37	36	oveq1d	$$⊢\phi \to \left|F\right|+1=N+1$$
38	15 34 37	3eqtrd	$$⊢\phi \to \left|H\right|=N+1$$