Metamath Proof Explorer


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 = Vtx G
isubgr3stgr.u U = G NeighbVtx X
isubgr3stgr.c C = G ClNeighbVtx X
isubgr3stgr.n N 0
isubgr3stgr.s No typesetting found for |- S = ( StarGr ` N ) with typecode |-
isubgr3stgr.w W = Vtx S
isubgr3stgr.e E = Edg G
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 = Vtx G
2 isubgr3stgr.u U = G NeighbVtx X
3 isubgr3stgr.c C = G ClNeighbVtx X
4 isubgr3stgr.n N 0
5 isubgr3stgr.s Could not format S = ( StarGr ` N ) : No typesetting found for |- S = ( StarGr ` N ) with typecode |-
6 isubgr3stgr.w W = Vtx S
7 isubgr3stgr.e E = Edg G
8 simpl G USGraph X V G USGraph
9 simpr G USGraph X V X V
10 simpl U = N x U y U x y E U = N
11 1 2 3 4 5 6 isubgr3stgrlem3 G USGraph X V U = N f f : C 1-1 onto W f X = 0
12 8 9 10 11 syl2an3an G USGraph X V U = N x U y U x y E f f : C 1-1 onto W f X = 0
13 1 clnbgrssvtx G ClNeighbVtx X V
14 3 13 eqsstri C V
15 14 a1i X V C V
16 15 anim2i G USGraph X V G USGraph C V
17 16 adantr G USGraph X V U = N x U y U x y E G USGraph C V
18 1 isubgrvtx G USGraph C V Vtx G ISubGr C = C
19 17 18 syl G USGraph X V U = N x U y U x y E Vtx G ISubGr C = C
20 19 eqcomd G USGraph X V U = N x U y U x y E C = Vtx G ISubGr C
21 20 f1oeq2d G USGraph X V U = N x U y U x y E f : C 1-1 onto W f : Vtx G ISubGr C 1-1 onto W
22 21 biimpd G USGraph X V U = N x U y U x y E f : C 1-1 onto W f : Vtx G ISubGr C 1-1 onto W
23 22 adantrd G USGraph X V U = N x U y U x y E f : C 1-1 onto W f X = 0 f : Vtx G ISubGr C 1-1 onto W
24 23 imp G USGraph X V U = N x U y U x y E f : C 1-1 onto W f X = 0 f : Vtx G ISubGr C 1-1 onto W
25 fvexd G USGraph X V U = N x U y U x y E f : C 1-1 onto W f X = 0 Edg G ISubGr C V
26 25 mptexd G USGraph X V U = N x U y U x y E f : C 1-1 onto W f X = 0 i Edg G ISubGr C f i V
27 eqid Edg G ISubGr C = Edg G ISubGr C
28 eqid i Edg G ISubGr C f i = i Edg G ISubGr C f i
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 = i Edg G ISubGr C f i g e = i Edg G ISubGr C f i e
32 31 eqeq2d g = i Edg G ISubGr C f i f e = g e f e = i Edg G ISubGr C f i e
33 32 ralbidv g = i Edg G ISubGr C f i e Edg G ISubGr C f e = g e e Edg G ISubGr C f e = i Edg G ISubGr C f i e
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 G USGraph C V G ISubGr C USGraph
41 16 40 syl G USGraph X V G ISubGr C USGraph
42 usgruspgr G ISubGr C USGraph G ISubGr C USHGraph
43 uspgrushgr G ISubGr C USHGraph G ISubGr C USHGraph
44 41 42 43 3syl G USGraph X V G ISubGr C 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 Vtx G ISubGr C = Vtx G ISubGr C
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 |-