Theorem isubgr3stgrlem5

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

	Ref	Expression
Hypotheses	isubgr3stgr.v	|- V = ( Vtx ` G )
	isubgr3stgr.u	|- U = ( G NeighbVtx X )
	isubgr3stgr.c	|- C = ( G ClNeighbVtx X )
	isubgr3stgr.n	|- N e. NN0
	isubgr3stgr.s	|- S = ( StarGr ` N )
	isubgr3stgr.w	|- W = ( Vtx ` S )
	isubgr3stgr.e	|- E = ( Edg ` G )
	isubgr3stgr.i	|- I = ( Edg ` ( G ISubGr C ) )
	isubgr3stgr.h	|- H = ( i e. I |-> ( F " i ) )
Assertion	isubgr3stgrlem5	|- ( ( F : C --> W /\ Y e. I ) -> ( H ` Y ) = ( F " Y ) )

Proof

Step	Hyp	Ref	Expression
1		isubgr3stgr.v	|- V = ( Vtx ` G )
2		isubgr3stgr.u	|- U = ( G NeighbVtx X )
3		isubgr3stgr.c	|- C = ( G ClNeighbVtx X )
4		isubgr3stgr.n	|- N e. NN0
5		isubgr3stgr.s	|- S = ( StarGr ` N )
6		isubgr3stgr.w	|- W = ( Vtx ` S )
7		isubgr3stgr.e	|- E = ( Edg ` G )
8		isubgr3stgr.i	|- I = ( Edg ` ( G ISubGr C ) )
9		isubgr3stgr.h	|- H = ( i e. I |-> ( F " i ) )
10	9	a1i	|- ( ( F : C --> W /\ Y e. I ) -> H = ( i e. I |-> ( F " i ) ) )
11		imaeq2	|- ( i = Y -> ( F " i ) = ( F " Y ) )
12	11	adantl	|- ( ( ( F : C --> W /\ Y e. I ) /\ i = Y ) -> ( F " i ) = ( F " Y ) )
13		simpr	|- ( ( F : C --> W /\ Y e. I ) -> Y e. I )
14		id	|- ( F : C --> W -> F : C --> W )
15	3	ovexi	|- C e. _V
16	15	a1i	|- ( F : C --> W -> C e. _V )
17	14 16	fexd	|- ( F : C --> W -> F e. _V )
18	17	adantr	|- ( ( F : C --> W /\ Y e. I ) -> F e. _V )
19	18	imaexd	|- ( ( F : C --> W /\ Y e. I ) -> ( F " Y ) e. _V )
20	10 12 13 19	fvmptd	|- ( ( F : C --> W /\ Y e. I ) -> ( H ` Y ) = ( F " Y ) )