Theorem isubgr3stgrlem8

Description: Lemma 8 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	isubgr3stgrlem8	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 ) ) ) 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		imaeq2	$$⊢i=k\to F\left[i\right]=F\left[k\right]$$
11	10	cbvmptv	$$⊢\left(i\in I⟼F\left[i\right]\right)=\left(k\in I⟼F\left[k\right]\right)$$
12	9 11	eqtri	$$⊢H=\left(k\in I⟼F\left[k\right]\right)$$
13		f1of	$$⊢F:C\underset{1-1\; onto}{⟶}W\to F:C⟶W$$
14	13	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$$
15	1 2 3 4 5 6 7 8 9	isubgr3stgrlem5	$$⊢\left(F:C⟶W\wedge k\in I\right)\to H\left(k\right)=F\left[k\right]$$
16	14 15	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 k\in I\right)\to H\left(k\right)=F\left[k\right]$$
17	1 2 3 4 5 6 7 8 9	isubgr3stgrlem6	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 --> ( 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 --> ( Edg ` ( StarGr ` N ) ) ) with typecode |-
18	17	ffvelcdmda	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 ) ) /\ k e. I ) -> ( H ` k ) e. ( 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 ) ) /\ k e. I ) -> ( H ` k ) e. ( Edg ` ( StarGr ` N ) ) ) with typecode |-
19	16 18	eqeltrrd	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 ) ) /\ k e. I ) -> ( F " k ) e. ( 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 ) ) /\ k e. I ) -> ( F " k ) e. ( Edg ` ( StarGr ` N ) ) ) with typecode |-
20	1 2 3 4 5 6 7 8 9	isubgr3stgrlem7	Could not format ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ j e. ( Edg ` ( StarGr ` N ) ) ) -> ( `' F " j ) e. I ) : No typesetting found for |- ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ j e. ( Edg ` ( StarGr ` N ) ) ) -> ( `' F " j ) e. I ) with typecode |-
21	20	ad4ant134	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 ) ) /\ j e. ( Edg ` ( StarGr ` N ) ) ) -> ( `' F " j ) e. I ) : 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 ) ) /\ j e. ( Edg ` ( StarGr ` N ) ) ) -> ( `' F " j ) e. I ) with typecode |-
22		f1ofo	$$⊢F:C\underset{1-1\; onto}{⟶}W\to F:C\underset{onto}{⟶}W$$
23	22	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\underset{onto}{⟶}W$$
24		stgrusgra	Could not format ( N e. NN0 -> ( StarGr ` N ) e. USGraph ) : No typesetting found for |- ( N e. NN0 -> ( StarGr ` N ) e. USGraph ) with typecode |-
25	4 24	mp1i	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 ) ) -> ( StarGr ` N ) e. USGraph ) : 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 ) ) -> ( StarGr ` N ) e. USGraph ) with typecode |-
26		simpr	Could not format ( ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) -> j e. ( Edg ` ( StarGr ` N ) ) ) : No typesetting found for |- ( ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) -> j e. ( Edg ` ( StarGr ` N ) ) ) with typecode |-
27	5	fveq2i	Could not format ( Vtx ` S ) = ( Vtx ` ( StarGr ` N ) ) : No typesetting found for |- ( Vtx ` S ) = ( Vtx ` ( StarGr ` N ) ) with typecode |-
28	6 27	eqtri	Could not format W = ( Vtx ` ( StarGr ` N ) ) : No typesetting found for |- W = ( Vtx ` ( StarGr ` N ) ) with typecode |-
29		eqid	Could not format ( Edg ` ( StarGr ` N ) ) = ( Edg ` ( StarGr ` N ) ) : No typesetting found for |- ( Edg ` ( StarGr ` N ) ) = ( Edg ` ( StarGr ` N ) ) with typecode |-
30	28 29	edgssv2	Could not format ( ( ( StarGr ` N ) e. USGraph /\ j e. ( Edg ` ( StarGr ` N ) ) ) -> ( j C_ W /\ ( # ` j ) = 2 ) ) : No typesetting found for |- ( ( ( StarGr ` N ) e. USGraph /\ j e. ( Edg ` ( StarGr ` N ) ) ) -> ( j C_ W /\ ( # ` j ) = 2 ) ) with typecode |-
31	30	simpld	Could not format ( ( ( StarGr ` N ) e. USGraph /\ j e. ( Edg ` ( StarGr ` N ) ) ) -> j C_ W ) : No typesetting found for |- ( ( ( StarGr ` N ) e. USGraph /\ j e. ( Edg ` ( StarGr ` N ) ) ) -> j C_ W ) with typecode |-
32	25 26 31	syl2an	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 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) -> j C_ W ) : 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 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) -> j C_ W ) with typecode |-
33		foimacnv	$$⊢\left(F:C\underset{onto}{⟶}W\wedge j\subseteq W\right)\to F\left[F^{-1}\left[j\right]\right]=j$$
34	23 32 33	syl2an2r	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 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) -> ( F " ( `' F " j ) ) = j ) : 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 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) -> ( F " ( `' F " j ) ) = j ) with typecode |-
35		imaeq2	$$⊢k=F^{-1}\left[j\right]\to F\left[k\right]=F\left[F^{-1}\left[j\right]\right]$$
36	35	eqcomd	$$⊢k=F^{-1}\left[j\right]\to F\left[F^{-1}\left[j\right]\right]=F\left[k\right]$$
37	34 36	sylan9req	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 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) /\ k = ( `' F " j ) ) -> j = ( F " k ) ) : 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 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) /\ k = ( `' F " j ) ) -> j = ( F " k ) ) with typecode |-
38		imaeq2	$$⊢j=F\left[k\right]\to F^{-1}\left[j\right]=F^{-1}\left[F\left[k\right]\right]$$
39		f1of1	$$⊢F:C\underset{1-1\; onto}{⟶}W\to F:C\underset{1-1}{⟶}W$$
40	39	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\underset{1-1}{⟶}W$$
41		usgruhgr	$$⊢G\in \mathrm{USGraph}\to G\in \mathrm{UHGraph}$$
42	41	ad2antrr	$$⊢\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)\to G\in \mathrm{UHGraph}$$
43	1	clnbgrssvtx	$$⊢GClNeighbVtxX\subseteq V$$
44	3 43	eqsstri	$$⊢C\subseteq V$$
45	44	a1i	$$⊢\left(F:C\underset{1-1\; onto}{⟶}W\wedge F\left(X\right)=0\right)\to C\subseteq V$$
46		eqid	$$⊢\mathrm{Edg}\left(G\right)=\mathrm{Edg}\left(G\right)$$
47		eqid	$$⊢G\mathrm{ISubGr}C=G\mathrm{ISubGr}C$$
48	1 46 47 8	isubgredg	$$⊢\left(G\in \mathrm{UHGraph}\wedge C\subseteq V\right)\to \left(k\in I\leftrightarrow \left(k\in \mathrm{Edg}\left(G\right)\wedge k\subseteq C\right)\right)$$
49	42 45 48	syl2an	$$⊢\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 \left(k\in I\leftrightarrow \left(k\in \mathrm{Edg}\left(G\right)\wedge k\subseteq C\right)\right)$$
50		simpr	$$⊢\left(k\in \mathrm{Edg}\left(G\right)\wedge k\subseteq C\right)\to k\subseteq C$$
51	50	a1d	Could not format ( ( k e. ( Edg ` G ) /\ k C_ C ) -> ( j e. ( Edg ` ( StarGr ` N ) ) -> k C_ C ) ) : No typesetting found for |- ( ( k e. ( Edg ` G ) /\ k C_ C ) -> ( j e. ( Edg ` ( StarGr ` N ) ) -> k C_ C ) ) with typecode |-
52	49 51	biimtrdi	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 ) ) -> ( k e. I -> ( j e. ( Edg ` ( StarGr ` N ) ) -> k C_ C ) ) ) : 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 ) ) -> ( k e. I -> ( j e. ( Edg ` ( StarGr ` N ) ) -> k C_ C ) ) ) with typecode |-
53	52	imp32	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 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) -> k C_ C ) : 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 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) -> k C_ C ) with typecode |-
54		f1imacnv	$$⊢\left(F:C\underset{1-1}{⟶}W\wedge k\subseteq C\right)\to F^{-1}\left[F\left[k\right]\right]=k$$
55	40 53 54	syl2an2r	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 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) -> ( `' F " ( F " k ) ) = k ) : 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 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) -> ( `' F " ( F " k ) ) = k ) with typecode |-
56	38 55	sylan9eqr	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 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) /\ j = ( F " k ) ) -> ( `' F " j ) = k ) : 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 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) /\ j = ( F " k ) ) -> ( `' F " j ) = k ) with typecode |-
57	56	eqcomd	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 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) /\ j = ( F " k ) ) -> k = ( `' F " j ) ) : 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 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) /\ j = ( F " k ) ) -> k = ( `' F " j ) ) with typecode |-
58	37 57	impbida	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 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) -> ( k = ( `' F " j ) <-> j = ( F " k ) ) ) : 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 ) ) /\ ( k e. I /\ j e. ( Edg ` ( StarGr ` N ) ) ) ) -> ( k = ( `' F " j ) <-> j = ( F " k ) ) ) with typecode |-
59	12 19 21 58	f1o2d	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 |-