Theorem isubgr3stgrlem9

Description: Lemma 9 for isubgr3stgr . (Contributed by AV, 29-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	isubgr3stgrlem9	|- ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> ( H : I -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. I ( F " e ) = ( H ` e ) ) )

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	1 2 3 4 5 6 7 8 9	isubgr3stgrlem8	|- ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> H : I -1-1-onto-> ( Edg ` ( StarGr ` N ) ) )
11		f1of	|- ( F : C -1-1-onto-> W -> F : C --> W )
12	11	ad2antrl	|- ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> F : C --> W )
13	1 2 3 4 5 6 7 8 9	isubgr3stgrlem5	|- ( ( F : C --> W /\ e e. I ) -> ( H ` e ) = ( F " e ) )
14	13	eqcomd	|- ( ( F : C --> W /\ e e. I ) -> ( F " e ) = ( H ` e ) )
15	12 14	sylan	|- ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ e e. I ) -> ( F " e ) = ( H ` e ) )
16	15	ralrimiva	|- ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> A. e e. I ( F " e ) = ( H ` e ) )
17	10 16	jca	|- ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> ( H : I -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. I ( F " e ) = ( H ` e ) ) )