Theorem isubgr3stgr

Description: If a vertex of a simple graph has exactly N (different) neighbors, and none of these neighbors are connected by an edge, then the (closed) neighborhood of this vertex induces a subgraph which is isomorphic to an N-star. (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)$$
Assertion	isubgr3stgr	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 ) -> ( G ISubGr C ) ~=gr ( 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		simpl	$$⊢\left(G\in \mathrm{USGraph}\wedge X\in V\right)\to G\in \mathrm{USGraph}$$
9		simpr	$$⊢\left(G\in \mathrm{USGraph}\wedge X\in V\right)\to X\in V$$
10		simpl	$$⊢\left(\left|U\right|=N\wedge \forall x\in U\forall y\in U\left\{x,y\right\}\notin E\right)\to \left|U\right|=N$$
11	1 2 3 4 5 6	isubgr3stgrlem3	$$⊢\left(G\in \mathrm{USGraph}\wedge X\in V\wedge \left|U\right|=N\right)\to \exists f\left(f:C\underset{1-1\; onto}{⟶}W\wedge f\left(X\right)=0\right)$$
12	8 9 10 11	syl2an3an	$$⊢\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 \exists f\left(f:C\underset{1-1\; onto}{⟶}W\wedge f\left(X\right)=0\right)$$
13	1	clnbgrssvtx	$$⊢GClNeighbVtxX\subseteq V$$
14	3 13	eqsstri	$$⊢C\subseteq V$$
15	14	a1i	$$⊢X\in V\to C\subseteq V$$
16	15	anim2i	$$⊢\left(G\in \mathrm{USGraph}\wedge X\in V\right)\to \left(G\in \mathrm{USGraph}\wedge C\subseteq V\right)$$
17	16	adantr	$$⊢\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 \left(G\in \mathrm{USGraph}\wedge C\subseteq V\right)$$
18	1	isubgrvtx	$$⊢\left(G\in \mathrm{USGraph}\wedge C\subseteq V\right)\to \mathrm{Vtx}\left(G\mathrm{ISubGr}C\right)=C$$
19	17 18	syl	$$⊢\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 \mathrm{Vtx}\left(G\mathrm{ISubGr}C\right)=C$$
20	19	eqcomd	$$⊢\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 C=\mathrm{Vtx}\left(G\mathrm{ISubGr}C\right)$$
21	20	f1oeq2d	$$⊢\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 \left(f:C\underset{1-1\; onto}{⟶}W\leftrightarrow f:\mathrm{Vtx}\left(G\mathrm{ISubGr}C\right)\underset{1-1\; onto}{⟶}W\right)$$
22	21	biimpd	$$⊢\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 \left(f:C\underset{1-1\; onto}{⟶}W\to f:\mathrm{Vtx}\left(G\mathrm{ISubGr}C\right)\underset{1-1\; onto}{⟶}W\right)$$
23	22	adantrd	$$⊢\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 \left(\left(f:C\underset{1-1\; onto}{⟶}W\wedge f\left(X\right)=0\right)\to f:\mathrm{Vtx}\left(G\mathrm{ISubGr}C\right)\underset{1-1\; onto}{⟶}W\right)$$
24	23	imp	$$⊢\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:\mathrm{Vtx}\left(G\mathrm{ISubGr}C\right)\underset{1-1\; onto}{⟶}W$$
25		fvexd	$$⊢\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 \mathrm{Edg}\left(G\mathrm{ISubGr}C\right)\in \mathrm{V}$$
26	25	mptexd	$$⊢\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(i\in \mathrm{Edg}\left(G\mathrm{ISubGr}C\right)⟼f\left[i\right]\right)\in \mathrm{V}$$
27		eqid	$$⊢\mathrm{Edg}\left(G\mathrm{ISubGr}C\right)=\mathrm{Edg}\left(G\mathrm{ISubGr}C\right)$$
28		eqid	$$⊢\left(i\in \mathrm{Edg}\left(G\mathrm{ISubGr}C\right)⟼f\left[i\right]\right)=\left(i\in \mathrm{Edg}\left(G\mathrm{ISubGr}C\right)⟼f\left[i\right]\right)$$
29	1 2 3 4 5 6 7 27 28	isubgr3stgrlem9	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 ) ) -> ( ( i e. ( Edg ` ( G ISubGr C ) ) |-> ( f " i ) ) : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. ( Edg ` ( G ISubGr C ) ) ( f " e ) = ( ( i e. ( Edg ` ( G ISubGr C ) ) |-> ( f " i ) ) ` 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 ) ) -> ( ( i e. ( Edg ` ( G ISubGr C ) ) |-> ( f " i ) ) : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. ( Edg ` ( G ISubGr C ) ) ( f " e ) = ( ( i e. ( Edg ` ( G ISubGr C ) ) |-> ( f " i ) ) ` e ) ) ) with typecode |-
30		f1oeq1	Could not format ( g = ( i e. ( Edg ` ( G ISubGr C ) ) |-> ( f " i ) ) -> ( g : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) <-> ( i e. ( Edg ` ( G ISubGr C ) ) |-> ( f " i ) ) : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) ) ) : No typesetting found for |- ( g = ( i e. ( Edg ` ( G ISubGr C ) ) |-> ( f " i ) ) -> ( g : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) <-> ( i e. ( Edg ` ( G ISubGr C ) ) |-> ( f " i ) ) : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) ) ) with typecode |-
31		fveq1	$$⊢g=\left(i\in \mathrm{Edg}\left(G\mathrm{ISubGr}C\right)⟼f\left[i\right]\right)\to g\left(e\right)=\left(i\in \mathrm{Edg}\left(G\mathrm{ISubGr}C\right)⟼f\left[i\right]\right)\left(e\right)$$
32	31	eqeq2d	$$⊢g=\left(i\in \mathrm{Edg}\left(G\mathrm{ISubGr}C\right)⟼f\left[i\right]\right)\to \left(f\left[e\right]=g\left(e\right)\leftrightarrow f\left[e\right]=\left(i\in \mathrm{Edg}\left(G\mathrm{ISubGr}C\right)⟼f\left[i\right]\right)\left(e\right)\right)$$
33	32	ralbidv	$$⊢g=\left(i\in \mathrm{Edg}\left(G\mathrm{ISubGr}C\right)⟼f\left[i\right]\right)\to \left(\forall e\in \mathrm{Edg}\left(G\mathrm{ISubGr}C\right)f\left[e\right]=g\left(e\right)\leftrightarrow \forall e\in \mathrm{Edg}\left(G\mathrm{ISubGr}C\right)f\left[e\right]=\left(i\in \mathrm{Edg}\left(G\mathrm{ISubGr}C\right)⟼f\left[i\right]\right)\left(e\right)\right)$$
34	30 33	anbi12d	Could not format ( g = ( i e. ( Edg ` ( G ISubGr C ) ) |-> ( f " i ) ) -> ( ( g : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. ( Edg ` ( G ISubGr C ) ) ( f " e ) = ( g ` e ) ) <-> ( ( i e. ( Edg ` ( G ISubGr C ) ) |-> ( f " i ) ) : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. ( Edg ` ( G ISubGr C ) ) ( f " e ) = ( ( i e. ( Edg ` ( G ISubGr C ) ) |-> ( f " i ) ) ` e ) ) ) ) : No typesetting found for |- ( g = ( i e. ( Edg ` ( G ISubGr C ) ) |-> ( f " i ) ) -> ( ( g : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. ( Edg ` ( G ISubGr C ) ) ( f " e ) = ( g ` e ) ) <-> ( ( i e. ( Edg ` ( G ISubGr C ) ) |-> ( f " i ) ) : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. ( Edg ` ( G ISubGr C ) ) ( f " e ) = ( ( i e. ( Edg ` ( G ISubGr C ) ) |-> ( f " i ) ) ` e ) ) ) ) with typecode |-
35	26 29 34	spcedv	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 ) ) -> E. g ( g : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. ( Edg ` ( G ISubGr C ) ) ( f " e ) = ( g ` 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 ) ) -> E. g ( g : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. ( Edg ` ( G ISubGr C ) ) ( f " e ) = ( g ` e ) ) ) with typecode |-
36	24 35	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 ) ) -> ( f : ( Vtx ` ( G ISubGr C ) ) -1-1-onto-> W /\ E. g ( g : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. ( Edg ` ( G ISubGr C ) ) ( f " e ) = ( g ` 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 ) ) -> ( f : ( Vtx ` ( G ISubGr C ) ) -1-1-onto-> W /\ E. g ( g : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. ( Edg ` ( G ISubGr C ) ) ( f " e ) = ( g ` e ) ) ) ) with typecode |-
37	36	ex	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 ) -> ( f : ( Vtx ` ( G ISubGr C ) ) -1-1-onto-> W /\ E. g ( g : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. ( Edg ` ( G ISubGr C ) ) ( f " e ) = ( g ` 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 ) -> ( f : ( Vtx ` ( G ISubGr C ) ) -1-1-onto-> W /\ E. g ( g : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. ( Edg ` ( G ISubGr C ) ) ( f " e ) = ( g ` e ) ) ) ) ) with typecode |-
38	37	eximdv	Could not format ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) -> ( E. f ( f : C -1-1-onto-> W /\ ( f ` X ) = 0 ) -> E. f ( f : ( Vtx ` ( G ISubGr C ) ) -1-1-onto-> W /\ E. g ( g : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. ( Edg ` ( G ISubGr C ) ) ( f " e ) = ( g ` 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 ) ) -> ( E. f ( f : C -1-1-onto-> W /\ ( f ` X ) = 0 ) -> E. f ( f : ( Vtx ` ( G ISubGr C ) ) -1-1-onto-> W /\ E. g ( g : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. ( Edg ` ( G ISubGr C ) ) ( f " e ) = ( g ` e ) ) ) ) ) with typecode |-
39	12 38	mpd	Could not format ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) -> E. f ( f : ( Vtx ` ( G ISubGr C ) ) -1-1-onto-> W /\ E. g ( g : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. ( Edg ` ( G ISubGr C ) ) ( f " e ) = ( g ` 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 ) ) -> E. f ( f : ( Vtx ` ( G ISubGr C ) ) -1-1-onto-> W /\ E. g ( g : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. ( Edg ` ( G ISubGr C ) ) ( f " e ) = ( g ` e ) ) ) ) with typecode |-
40	1	isubgrusgr	$$⊢\left(G\in \mathrm{USGraph}\wedge C\subseteq V\right)\to G\mathrm{ISubGr}C\in \mathrm{USGraph}$$
41	16 40	syl	$$⊢\left(G\in \mathrm{USGraph}\wedge X\in V\right)\to G\mathrm{ISubGr}C\in \mathrm{USGraph}$$
42		usgruspgr	$$⊢G\mathrm{ISubGr}C\in \mathrm{USGraph}\to G\mathrm{ISubGr}C\in \mathrm{USHGraph}$$
43		uspgrushgr	$$⊢G\mathrm{ISubGr}C\in \mathrm{USHGraph}\to G\mathrm{ISubGr}C\in \mathrm{USHGraph}$$
44	41 42 43	3syl	$$⊢\left(G\in \mathrm{USGraph}\wedge X\in V\right)\to G\mathrm{ISubGr}C\in \mathrm{USHGraph}$$
45		stgrusgra	Could not format ( N e. NN0 -> ( StarGr ` N ) e. USGraph ) : No typesetting found for |- ( N e. NN0 -> ( StarGr ` N ) e. USGraph ) with typecode |-
46		usgruspgr	Could not format ( ( StarGr ` N ) e. USGraph -> ( StarGr ` N ) e. USPGraph ) : No typesetting found for |- ( ( StarGr ` N ) e. USGraph -> ( StarGr ` N ) e. USPGraph ) with typecode |-
47		uspgrushgr	Could not format ( ( StarGr ` N ) e. USPGraph -> ( StarGr ` N ) e. USHGraph ) : No typesetting found for |- ( ( StarGr ` N ) e. USPGraph -> ( StarGr ` N ) e. USHGraph ) with typecode |-
48	45 46 47	3syl	Could not format ( N e. NN0 -> ( StarGr ` N ) e. USHGraph ) : No typesetting found for |- ( N e. NN0 -> ( StarGr ` N ) e. USHGraph ) with typecode |-
49	4 48	ax-mp	Could not format ( StarGr ` N ) e. USHGraph : No typesetting found for |- ( StarGr ` N ) e. USHGraph with typecode |-
50		eqid	$$⊢\mathrm{Vtx}\left(G\mathrm{ISubGr}C\right)=\mathrm{Vtx}\left(G\mathrm{ISubGr}C\right)$$
51	5	fveq2i	Could not format ( Vtx ` S ) = ( Vtx ` ( StarGr ` N ) ) : No typesetting found for |- ( Vtx ` S ) = ( Vtx ` ( StarGr ` N ) ) with typecode |-
52	6 51	eqtri	Could not format W = ( Vtx ` ( StarGr ` N ) ) : No typesetting found for |- W = ( Vtx ` ( StarGr ` N ) ) with typecode |-
53		eqid	Could not format ( Edg ` ( StarGr ` N ) ) = ( Edg ` ( StarGr ` N ) ) : No typesetting found for |- ( Edg ` ( StarGr ` N ) ) = ( Edg ` ( StarGr ` N ) ) with typecode |-
54	50 52 27 53	gricushgr	Could not format ( ( ( G ISubGr C ) e. USHGraph /\ ( StarGr ` N ) e. USHGraph ) -> ( ( G ISubGr C ) ~=gr ( StarGr ` N ) <-> E. f ( f : ( Vtx ` ( G ISubGr C ) ) -1-1-onto-> W /\ E. g ( g : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. ( Edg ` ( G ISubGr C ) ) ( f " e ) = ( g ` e ) ) ) ) ) : No typesetting found for |- ( ( ( G ISubGr C ) e. USHGraph /\ ( StarGr ` N ) e. USHGraph ) -> ( ( G ISubGr C ) ~=gr ( StarGr ` N ) <-> E. f ( f : ( Vtx ` ( G ISubGr C ) ) -1-1-onto-> W /\ E. g ( g : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. ( Edg ` ( G ISubGr C ) ) ( f " e ) = ( g ` e ) ) ) ) ) with typecode |-
55	44 49 54	sylancl	Could not format ( ( G e. USGraph /\ X e. V ) -> ( ( G ISubGr C ) ~=gr ( StarGr ` N ) <-> E. f ( f : ( Vtx ` ( G ISubGr C ) ) -1-1-onto-> W /\ E. g ( g : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. ( Edg ` ( G ISubGr C ) ) ( f " e ) = ( g ` e ) ) ) ) ) : No typesetting found for |- ( ( G e. USGraph /\ X e. V ) -> ( ( G ISubGr C ) ~=gr ( StarGr ` N ) <-> E. f ( f : ( Vtx ` ( G ISubGr C ) ) -1-1-onto-> W /\ E. g ( g : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. ( Edg ` ( G ISubGr C ) ) ( f " e ) = ( g ` e ) ) ) ) ) with typecode |-
56	55	adantr	Could not format ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) -> ( ( G ISubGr C ) ~=gr ( StarGr ` N ) <-> E. f ( f : ( Vtx ` ( G ISubGr C ) ) -1-1-onto-> W /\ E. g ( g : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. ( Edg ` ( G ISubGr C ) ) ( f " e ) = ( g ` 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 ) ) -> ( ( G ISubGr C ) ~=gr ( StarGr ` N ) <-> E. f ( f : ( Vtx ` ( G ISubGr C ) ) -1-1-onto-> W /\ E. g ( g : ( Edg ` ( G ISubGr C ) ) -1-1-onto-> ( Edg ` ( StarGr ` N ) ) /\ A. e e. ( Edg ` ( G ISubGr C ) ) ( f " e ) = ( g ` e ) ) ) ) ) with typecode |-
57	39 56	mpbird	Could not format ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) -> ( G ISubGr C ) ~=gr ( 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 ) ) -> ( G ISubGr C ) ~=gr ( StarGr ` N ) ) with typecode |-
58	57	ex	Could not format ( ( G e. USGraph /\ X e. V ) -> ( ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) -> ( G ISubGr C ) ~=gr ( 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 ) -> ( G ISubGr C ) ~=gr ( StarGr ` N ) ) ) with typecode |-