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 ‘ 𝑁 ) ) ) |