Theorem wlkp1lem2

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

	Ref	Expression
Hypotheses	wlkp1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	wlkp1.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	wlkp1.f	⊢ ( 𝜑 → Fun 𝐼 )
	wlkp1.a	⊢ ( 𝜑 → 𝐼 ∈ Fin )
	wlkp1.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	wlkp1.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	wlkp1.d	⊢ ( 𝜑 → ¬ 𝐵 ∈ dom 𝐼 )
	wlkp1.w	⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
	wlkp1.n	⊢ 𝑁 = ( ♯ ‘ 𝐹 )
	wlkp1.e	⊢ ( 𝜑 → 𝐸 ∈ ( Edg ‘ 𝐺 ) )
	wlkp1.x	⊢ ( 𝜑 → { ( 𝑃 ‘ 𝑁 ) , 𝐶 } ⊆ 𝐸 )
	wlkp1.u	⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) )
	wlkp1.h	⊢ 𝐻 = ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } )
Assertion	wlkp1lem2	⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) = ( 𝑁 + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		wlkp1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		wlkp1.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3		wlkp1.f	⊢ ( 𝜑 → Fun 𝐼 )
4		wlkp1.a	⊢ ( 𝜑 → 𝐼 ∈ Fin )
5		wlkp1.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
6		wlkp1.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
7		wlkp1.d	⊢ ( 𝜑 → ¬ 𝐵 ∈ dom 𝐼 )
8		wlkp1.w	⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
9		wlkp1.n	⊢ 𝑁 = ( ♯ ‘ 𝐹 )
10		wlkp1.e	⊢ ( 𝜑 → 𝐸 ∈ ( Edg ‘ 𝐺 ) )
11		wlkp1.x	⊢ ( 𝜑 → { ( 𝑃 ‘ 𝑁 ) , 𝐶 } ⊆ 𝐸 )
12		wlkp1.u	⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) )
13		wlkp1.h	⊢ 𝐻 = ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } )
14	13	fveq2i	⊢ ( ♯ ‘ 𝐻 ) = ( ♯ ‘ ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) )
15	14	a1i	⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) = ( ♯ ‘ ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ) )
16		opex	⊢ ⟨ 𝑁 , 𝐵 ⟩ ∈ V
17	2	wlkf	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
18		wrdfin	⊢ ( 𝐹 ∈ Word dom 𝐼 → 𝐹 ∈ Fin )
19	8 17 18	3syl	⊢ ( 𝜑 → 𝐹 ∈ Fin )
20		fzonel	⊢ ¬ ( ♯ ‘ 𝐹 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) )
21	20	a1i	⊢ ( 𝜑 → ¬ ( ♯ ‘ 𝐹 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
22		eleq1	⊢ ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ ( ♯ ‘ 𝐹 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
23	22	notbid	⊢ ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( ¬ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ ¬ ( ♯ ‘ 𝐹 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
24	21 23	imbitrrid	⊢ ( 𝑁 = ( ♯ ‘ 𝐹 ) → ( 𝜑 → ¬ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
25	9 24	ax-mp	⊢ ( 𝜑 → ¬ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
26		wrdfn	⊢ ( 𝐹 ∈ Word dom 𝐼 → 𝐹 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
27		fnop	⊢ ( ( 𝐹 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ⟨ 𝑁 , 𝐵 ⟩ ∈ 𝐹 ) → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
28	27	ex	⊢ ( 𝐹 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ⟨ 𝑁 , 𝐵 ⟩ ∈ 𝐹 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
29	8 17 26 28	4syl	⊢ ( 𝜑 → ( ⟨ 𝑁 , 𝐵 ⟩ ∈ 𝐹 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
30	25 29	mtod	⊢ ( 𝜑 → ¬ ⟨ 𝑁 , 𝐵 ⟩ ∈ 𝐹 )
31	19 30	jca	⊢ ( 𝜑 → ( 𝐹 ∈ Fin ∧ ¬ ⟨ 𝑁 , 𝐵 ⟩ ∈ 𝐹 ) )
32		hashunsng	⊢ ( ⟨ 𝑁 , 𝐵 ⟩ ∈ V → ( ( 𝐹 ∈ Fin ∧ ¬ ⟨ 𝑁 , 𝐵 ⟩ ∈ 𝐹 ) → ( ♯ ‘ ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
33	16 31 32	mpsyl	⊢ ( 𝜑 → ( ♯ ‘ ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
34	9	eqcomi	⊢ ( ♯ ‘ 𝐹 ) = 𝑁
35	34	a1i	⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) = 𝑁 )
36	35	oveq1d	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐹 ) + 1 ) = ( 𝑁 + 1 ) )
37	15 33 36	3eqtrd	⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) = ( 𝑁 + 1 ) )