Theorem isubgr3stgrlem5

Description: Lemma 5 for isubgr3stgr . (Contributed by AV, 24-Sep-2025)

	Ref	Expression
Hypotheses	isubgr3stgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	isubgr3stgr.u	⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
	isubgr3stgr.c	⊢ 𝐶 = ( 𝐺 ClNeighbVtx 𝑋 )
	isubgr3stgr.n	⊢ 𝑁 ∈ ℕ0
	isubgr3stgr.s	⊢ 𝑆 = ( StarGr ‘ 𝑁 )
	isubgr3stgr.w	⊢ 𝑊 = ( Vtx ‘ 𝑆 )
	isubgr3stgr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	isubgr3stgr.i	⊢ 𝐼 = ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) )
	isubgr3stgr.h	⊢ 𝐻 = ( 𝑖 ∈ 𝐼 ↦ ( 𝐹 “ 𝑖 ) )
Assertion	isubgr3stgrlem5	⊢ ( ( 𝐹 : 𝐶 ⟶ 𝑊 ∧ 𝑌 ∈ 𝐼 ) → ( 𝐻 ‘ 𝑌 ) = ( 𝐹 “ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		isubgr3stgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		isubgr3stgr.u	⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
3		isubgr3stgr.c	⊢ 𝐶 = ( 𝐺 ClNeighbVtx 𝑋 )
4		isubgr3stgr.n	⊢ 𝑁 ∈ ℕ0
5		isubgr3stgr.s	⊢ 𝑆 = ( StarGr ‘ 𝑁 )
6		isubgr3stgr.w	⊢ 𝑊 = ( Vtx ‘ 𝑆 )
7		isubgr3stgr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
8		isubgr3stgr.i	⊢ 𝐼 = ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) )
9		isubgr3stgr.h	⊢ 𝐻 = ( 𝑖 ∈ 𝐼 ↦ ( 𝐹 “ 𝑖 ) )
10	9	a1i	⊢ ( ( 𝐹 : 𝐶 ⟶ 𝑊 ∧ 𝑌 ∈ 𝐼 ) → 𝐻 = ( 𝑖 ∈ 𝐼 ↦ ( 𝐹 “ 𝑖 ) ) )
11		imaeq2	⊢ ( 𝑖 = 𝑌 → ( 𝐹 “ 𝑖 ) = ( 𝐹 “ 𝑌 ) )
12	11	adantl	⊢ ( ( ( 𝐹 : 𝐶 ⟶ 𝑊 ∧ 𝑌 ∈ 𝐼 ) ∧ 𝑖 = 𝑌 ) → ( 𝐹 “ 𝑖 ) = ( 𝐹 “ 𝑌 ) )
13		simpr	⊢ ( ( 𝐹 : 𝐶 ⟶ 𝑊 ∧ 𝑌 ∈ 𝐼 ) → 𝑌 ∈ 𝐼 )
14		id	⊢ ( 𝐹 : 𝐶 ⟶ 𝑊 → 𝐹 : 𝐶 ⟶ 𝑊 )
15	3	ovexi	⊢ 𝐶 ∈ V
16	15	a1i	⊢ ( 𝐹 : 𝐶 ⟶ 𝑊 → 𝐶 ∈ V )
17	14 16	fexd	⊢ ( 𝐹 : 𝐶 ⟶ 𝑊 → 𝐹 ∈ V )
18	17	adantr	⊢ ( ( 𝐹 : 𝐶 ⟶ 𝑊 ∧ 𝑌 ∈ 𝐼 ) → 𝐹 ∈ V )
19	18	imaexd	⊢ ( ( 𝐹 : 𝐶 ⟶ 𝑊 ∧ 𝑌 ∈ 𝐼 ) → ( 𝐹 “ 𝑌 ) ∈ V )
20	10 12 13 19	fvmptd	⊢ ( ( 𝐹 : 𝐶 ⟶ 𝑊 ∧ 𝑌 ∈ 𝐼 ) → ( 𝐻 ‘ 𝑌 ) = ( 𝐹 “ 𝑌 ) )