Theorem isubgr3stgrlem9

Description: Lemma 9 for isubgr3stgr . (Contributed by AV, 29-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	isubgr3stgrlem9	Could not format assertion : No typesetting found for |- ( ( ( ( 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 ) ) ) with typecode |-

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	1 2 3 4 5 6 7 8 9	isubgr3stgrlem8	Could not format ( ( ( ( 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 ) ) ) : No typesetting found for |- ( ( ( ( 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 ) ) ) with typecode |-
11		f1of	$$⊢F:C\underset{1-1\; onto}{⟶}W\to F:C⟶W$$
12	11	ad2antrl	$$⊢\left(\left(\left(G\in \mathrm{USGraph}\wedge X\in V\right)\wedge \left(\left|U\right|=N\wedge \forall x\in U\forall y\in U\left\{x,y\right\}\notin E\right)\right)\wedge \left(F:C\underset{1-1\; onto}{⟶}W\wedge F\left(X\right)=0\right)\right)\to F:C⟶W$$
13	1 2 3 4 5 6 7 8 9	isubgr3stgrlem5	$$⊢\left(F:C⟶W\wedge e\in I\right)\to H\left(e\right)=F\left[e\right]$$
14	13	eqcomd	$$⊢\left(F:C⟶W\wedge e\in I\right)\to F\left[e\right]=H\left(e\right)$$
15	12 14	sylan	$$⊢\left(\left(\left(\left(G\in \mathrm{USGraph}\wedge X\in V\right)\wedge \left(\left|U\right|=N\wedge \forall x\in U\forall y\in U\left\{x,y\right\}\notin E\right)\right)\wedge \left(F:C\underset{1-1\; onto}{⟶}W\wedge F\left(X\right)=0\right)\right)\wedge e\in I\right)\to F\left[e\right]=H\left(e\right)$$
16	15	ralrimiva	$$⊢\left(\left(\left(G\in \mathrm{USGraph}\wedge X\in V\right)\wedge \left(\left|U\right|=N\wedge \forall x\in U\forall y\in U\left\{x,y\right\}\notin E\right)\right)\wedge \left(F:C\underset{1-1\; onto}{⟶}W\wedge F\left(X\right)=0\right)\right)\to \forall e\in IF\left[e\right]=H\left(e\right)$$
17	10 16	jca	Could not format ( ( ( ( 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 ) ) ) : No typesetting found for |- ( ( ( ( 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 ) ) ) with typecode |-