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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isubgr3stgr.u ⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
isubgr3stgr.c ⊢ 𝐶 = ( 𝐺 ClNeighbVtx 𝑋 )
isubgr3stgr.n ⊢ 𝑁 ∈ ℕ0
isubgr3stgr.s ⊢ 𝑆 = ( StarGr ‘ 𝑁 )
isubgr3stgr.w ⊢ 𝑊 = ( Vtx ‘ 𝑆 )
isubgr3stgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion isubgr3stgr ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) → ( ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) → ( 𝐺 ISubGr 𝐶 ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 isubgr3stgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 isubgr3stgr.u ⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
3 isubgr3stgr.c ⊢ 𝐶 = ( 𝐺 ClNeighbVtx 𝑋 )
4 isubgr3stgr.n ⊢ 𝑁 ∈ ℕ0
5 isubgr3stgr.s ⊢ 𝑆 = ( StarGr ‘ 𝑁 )
6 isubgr3stgr.w ⊢ 𝑊 = ( Vtx ‘ 𝑆 )
7 isubgr3stgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
8 simpl ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) → 𝐺 ∈ USGraph )
9 simpr ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
10 simpl ⊢ ( ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) → ( ♯ ‘ 𝑈 ) = 𝑁 )
11 1 2 3 4 5 6 isubgr3stgrlem3 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) → ∃ 𝑓 ( 𝑓 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝑓 ‘ 𝑋 ) = 0 ) )
12 8 9 10 11 syl2an3an ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → ∃ 𝑓 ( 𝑓 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝑓 ‘ 𝑋 ) = 0 ) )
13 1 clnbgrssvtx ⊢ ( 𝐺 ClNeighbVtx 𝑋 ) ⊆ 𝑉
14 3 13 eqsstri ⊢ 𝐶 ⊆ 𝑉
15 14 a1i ⊢ ( 𝑋 ∈ 𝑉 → 𝐶 ⊆ 𝑉 )
16 15 anim2i ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) → ( 𝐺 ∈ USGraph ∧ 𝐶 ⊆ 𝑉 ) )
17 16 adantr ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → ( 𝐺 ∈ USGraph ∧ 𝐶 ⊆ 𝑉 ) )
18 1 isubgrvtx ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐶 ⊆ 𝑉 ) → ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) = 𝐶 )
19 17 18 syl ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) = 𝐶 )
20 19 eqcomd ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → 𝐶 = ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) )
21 20 f1oeq2d ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → ( 𝑓 : 𝐶 –1-1-onto→ 𝑊 ↔ 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ 𝑊 ) )
22 21 biimpd ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → ( 𝑓 : 𝐶 –1-1-onto→ 𝑊 → 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ 𝑊 ) )
23 22 adantrd ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → ( ( 𝑓 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝑓 ‘ 𝑋 ) = 0 ) → 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ 𝑊 ) )
24 23 imp ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝑓 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝑓 ‘ 𝑋 ) = 0 ) ) → 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ 𝑊 )
25 fvexd ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝑓 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝑓 ‘ 𝑋 ) = 0 ) ) → ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ∈ V )
26 25 mptexd ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝑓 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝑓 ‘ 𝑋 ) = 0 ) ) → ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓 “ 𝑖 ) ) ∈ V )
27 eqid ⊢ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) = ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) )
28 eqid ⊢ ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓 “ 𝑖 ) ) = ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓 “ 𝑖 ) )
29 1 2 3 4 5 6 7 27 28 isubgr3stgrlem9 ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝑓 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝑓 ‘ 𝑋 ) = 0 ) ) → ( ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓 “ 𝑖 ) ) : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓 “ 𝑒 ) = ( ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓 “ 𝑖 ) ) ‘ 𝑒 ) ) )
30 f1oeq1 ⊢ ( 𝑔 = ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓 “ 𝑖 ) ) → ( 𝑔 : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ↔ ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓 “ 𝑖 ) ) : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) )
31 fveq1 ⊢ ( 𝑔 = ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓 “ 𝑖 ) ) → ( 𝑔 ‘ 𝑒 ) = ( ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓 “ 𝑖 ) ) ‘ 𝑒 ) )
32 31 eqeq2d ⊢ ( 𝑔 = ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓 “ 𝑖 ) ) → ( ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ↔ ( 𝑓 “ 𝑒 ) = ( ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓 “ 𝑖 ) ) ‘ 𝑒 ) ) )
33 32 ralbidv ⊢ ( 𝑔 = ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓 “ 𝑖 ) ) → ( ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ↔ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓 “ 𝑒 ) = ( ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓 “ 𝑖 ) ) ‘ 𝑒 ) ) )
34 30 33 anbi12d ⊢ ( 𝑔 = ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓 “ 𝑖 ) ) → ( ( 𝑔 : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ↔ ( ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓 “ 𝑖 ) ) : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓 “ 𝑒 ) = ( ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓 “ 𝑖 ) ) ‘ 𝑒 ) ) ) )
35 26 29 34 spcedv ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝑓 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝑓 ‘ 𝑋 ) = 0 ) ) → ∃ 𝑔 ( 𝑔 : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) )
36 24 35 jca ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝑓 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝑓 ‘ 𝑋 ) = 0 ) ) → ( 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) )
37 36 ex ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → ( ( 𝑓 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝑓 ‘ 𝑋 ) = 0 ) → ( 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )
38 37 eximdv ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → ( ∃ 𝑓 ( 𝑓 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝑓 ‘ 𝑋 ) = 0 ) → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )
39 12 38 mpd ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) )
40 1 isubgrusgr ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐶 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝐶 ) ∈ USGraph )
41 16 40 syl ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) → ( 𝐺 ISubGr 𝐶 ) ∈ USGraph )
42 usgruspgr ⊢ ( ( 𝐺 ISubGr 𝐶 ) ∈ USGraph → ( 𝐺 ISubGr 𝐶 ) ∈ USPGraph )
43 uspgrushgr ⊢ ( ( 𝐺 ISubGr 𝐶 ) ∈ USPGraph → ( 𝐺 ISubGr 𝐶 ) ∈ USHGraph )
44 41 42 43 3syl ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) → ( 𝐺 ISubGr 𝐶 ) ∈ USHGraph )
45 stgrusgra ⊢ ( 𝑁 ∈ ℕ0 → ( StarGr ‘ 𝑁 ) ∈ USGraph )
46 usgruspgr ⊢ ( ( StarGr ‘ 𝑁 ) ∈ USGraph → ( StarGr ‘ 𝑁 ) ∈ USPGraph )
47 uspgrushgr ⊢ ( ( StarGr ‘ 𝑁 ) ∈ USPGraph → ( StarGr ‘ 𝑁 ) ∈ USHGraph )
48 45 46 47 3syl ⊢ ( 𝑁 ∈ ℕ0 → ( StarGr ‘ 𝑁 ) ∈ USHGraph )
49 4 48 ax-mp ⊢ ( StarGr ‘ 𝑁 ) ∈ USHGraph
50 eqid ⊢ ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) = ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) )
51 5 fveq2i ⊢ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ ( StarGr ‘ 𝑁 ) )
52 6 51 eqtri ⊢ 𝑊 = ( Vtx ‘ ( StarGr ‘ 𝑁 ) )
53 eqid ⊢ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) = ( Edg ‘ ( StarGr ‘ 𝑁 ) )
54 50 52 27 53 gricushgr ⊢ ( ( ( 𝐺 ISubGr 𝐶 ) ∈ USHGraph ∧ ( StarGr ‘ 𝑁 ) ∈ USHGraph ) → ( ( 𝐺 ISubGr 𝐶 ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )
55 44 49 54 sylancl ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐺 ISubGr 𝐶 ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )
56 55 adantr ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → ( ( 𝐺 ISubGr 𝐶 ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )
57 39 56 mpbird ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → ( 𝐺 ISubGr 𝐶 ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) )
58 57 ex ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) → ( ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) → ( 𝐺 ISubGr 𝐶 ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) )