Theorem isubgr3stgrlem5

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

	Ref	Expression
Hypotheses	isubgr3stgr.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	isubgr3stgr.u	$$⊢U=G\mathrm{NeighbVtx}X$$
	isubgr3stgr.c	$$⊢C=GClNeighbVtxX$$
	isubgr3stgr.n	$$⊢N\in {\mathbb{N}}_0$$
	isubgr3stgr.s	No typesetting found for |- S = ( StarGr ` N ) with typecode |-
	isubgr3stgr.w	$$⊢W=\mathrm{Vtx}\left(S\right)$$
	isubgr3stgr.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
	isubgr3stgr.i	$$⊢I=\mathrm{Edg}\left(G\mathrm{ISubGr}C\right)$$
	isubgr3stgr.h	$$⊢H=\left(i\in I⟼F\left[i\right]\right)$$
Assertion	isubgr3stgrlem5	$$⊢\left(F:C⟶W\wedge Y\in I\right)\to H\left(Y\right)=F\left[Y\right]$$

Proof

Step	Hyp	Ref	Expression
1		isubgr3stgr.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		isubgr3stgr.u	$$⊢U=G\mathrm{NeighbVtx}X$$
3		isubgr3stgr.c	$$⊢C=GClNeighbVtxX$$
4		isubgr3stgr.n	$$⊢N\in {\mathbb{N}}_0$$
5		isubgr3stgr.s	Could not format S = ( StarGr ` N ) : No typesetting found for |- S = ( StarGr ` N ) with typecode |-
6		isubgr3stgr.w	$$⊢W=\mathrm{Vtx}\left(S\right)$$
7		isubgr3stgr.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
8		isubgr3stgr.i	$$⊢I=\mathrm{Edg}\left(G\mathrm{ISubGr}C\right)$$
9		isubgr3stgr.h	$$⊢H=\left(i\in I⟼F\left[i\right]\right)$$
10	9	a1i	$$⊢\left(F:C⟶W\wedge Y\in I\right)\to H=\left(i\in I⟼F\left[i\right]\right)$$
11		imaeq2	$$⊢i=Y\to F\left[i\right]=F\left[Y\right]$$
12	11	adantl	$$⊢\left(\left(F:C⟶W\wedge Y\in I\right)\wedge i=Y\right)\to F\left[i\right]=F\left[Y\right]$$
13		simpr	$$⊢\left(F:C⟶W\wedge Y\in I\right)\to Y\in I$$
14		id	$$⊢F:C⟶W\to F:C⟶W$$
15	3	ovexi	$$⊢C\in \mathrm{V}$$
16	15	a1i	$$⊢F:C⟶W\to C\in \mathrm{V}$$
17	14 16	fexd	$$⊢F:C⟶W\to F\in \mathrm{V}$$
18	17	adantr	$$⊢\left(F:C⟶W\wedge Y\in I\right)\to F\in \mathrm{V}$$
19	18	imaexd	$$⊢\left(F:C⟶W\wedge Y\in I\right)\to F\left[Y\right]\in \mathrm{V}$$
20	10 12 13 19	fvmptd	$$⊢\left(F:C⟶W\wedge Y\in I\right)\to H\left(Y\right)=F\left[Y\right]$$