Theorem wlkp1lem3

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	wlkp1lem3	⊢ ( 𝜑 → ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) = ( ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) ‘ 𝐵 ) )

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	a1i	⊢ ( 𝜑 → 𝐻 = ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) )
15	14	fveq1d	⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ‘ 𝑁 ) )
16	9	fvexi	⊢ 𝑁 ∈ V
17	2	wlkf	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
18		lencl	⊢ ( 𝐹 ∈ Word dom 𝐼 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
19		wrddm	⊢ ( 𝐹 ∈ Word dom 𝐼 → dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
20		fzonel	⊢ ¬ ( ♯ ‘ 𝐹 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) )
21	9	a1i	⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑁 = ( ♯ ‘ 𝐹 ) )
22		simpr	⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
23	21 22	eleq12d	⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑁 ∈ dom 𝐹 ↔ ( ♯ ‘ 𝐹 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
24	20 23	mtbiri	⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ¬ 𝑁 ∈ dom 𝐹 )
25	18 19 24	syl2anc	⊢ ( 𝐹 ∈ Word dom 𝐼 → ¬ 𝑁 ∈ dom 𝐹 )
26	8 17 25	3syl	⊢ ( 𝜑 → ¬ 𝑁 ∈ dom 𝐹 )
27		fsnunfv	⊢ ( ( 𝑁 ∈ V ∧ 𝐵 ∈ 𝑊 ∧ ¬ 𝑁 ∈ dom 𝐹 ) → ( ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ‘ 𝑁 ) = 𝐵 )
28	16 5 26 27	mp3an2i	⊢ ( 𝜑 → ( ( 𝐹 ∪ { ⟨ 𝑁 , 𝐵 ⟩ } ) ‘ 𝑁 ) = 𝐵 )
29	15 28	eqtrd	⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) = 𝐵 )
30	12 29	fveq12d	⊢ ( 𝜑 → ( ( iEdg ‘ 𝑆 ) ‘ ( 𝐻 ‘ 𝑁 ) ) = ( ( 𝐼 ∪ { ⟨ 𝐵 , 𝐸 ⟩ } ) ‘ 𝐵 ) )