| 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 |
|
isubgr3stgr.i |
⊢ 𝐼 = ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) |
| 9 |
|
isubgr3stgr.h |
⊢ 𝐻 = ( 𝑖 ∈ 𝐼 ↦ ( 𝐹 “ 𝑖 ) ) |
| 10 |
|
imaeq2 |
⊢ ( 𝑖 = 𝑘 → ( 𝐹 “ 𝑖 ) = ( 𝐹 “ 𝑘 ) ) |
| 11 |
10
|
cbvmptv |
⊢ ( 𝑖 ∈ 𝐼 ↦ ( 𝐹 “ 𝑖 ) ) = ( 𝑘 ∈ 𝐼 ↦ ( 𝐹 “ 𝑘 ) ) |
| 12 |
9 11
|
eqtri |
⊢ 𝐻 = ( 𝑘 ∈ 𝐼 ↦ ( 𝐹 “ 𝑘 ) ) |
| 13 |
|
f1of |
⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 → 𝐹 : 𝐶 ⟶ 𝑊 ) |
| 14 |
13
|
ad2antrl |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → 𝐹 : 𝐶 ⟶ 𝑊 ) |
| 15 |
1 2 3 4 5 6 7 8 9
|
isubgr3stgrlem5 |
⊢ ( ( 𝐹 : 𝐶 ⟶ 𝑊 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐻 ‘ 𝑘 ) = ( 𝐹 “ 𝑘 ) ) |
| 16 |
14 15
|
sylan |
⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐻 ‘ 𝑘 ) = ( 𝐹 “ 𝑘 ) ) |
| 17 |
1 2 3 4 5 6 7 8 9
|
isubgr3stgrlem6 |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → 𝐻 : 𝐼 ⟶ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) |
| 18 |
17
|
ffvelcdmda |
⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐻 ‘ 𝑘 ) ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) |
| 19 |
16 18
|
eqeltrrd |
⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 “ 𝑘 ) ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) |
| 20 |
1 2 3 4 5 6 7 8 9
|
isubgr3stgrlem7 |
⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) → ( ◡ 𝐹 “ 𝑗 ) ∈ 𝐼 ) |
| 21 |
20
|
ad4ant134 |
⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) → ( ◡ 𝐹 “ 𝑗 ) ∈ 𝐼 ) |
| 22 |
|
f1ofo |
⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 → 𝐹 : 𝐶 –onto→ 𝑊 ) |
| 23 |
22
|
ad2antrl |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → 𝐹 : 𝐶 –onto→ 𝑊 ) |
| 24 |
|
stgrusgra |
⊢ ( 𝑁 ∈ ℕ0 → ( StarGr ‘ 𝑁 ) ∈ USGraph ) |
| 25 |
4 24
|
mp1i |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → ( StarGr ‘ 𝑁 ) ∈ USGraph ) |
| 26 |
|
simpr |
⊢ ( ( 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) → 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) |
| 27 |
5
|
fveq2i |
⊢ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) |
| 28 |
6 27
|
eqtri |
⊢ 𝑊 = ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) |
| 29 |
|
eqid |
⊢ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) = ( Edg ‘ ( StarGr ‘ 𝑁 ) ) |
| 30 |
28 29
|
edgssv2 |
⊢ ( ( ( StarGr ‘ 𝑁 ) ∈ USGraph ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) → ( 𝑗 ⊆ 𝑊 ∧ ( ♯ ‘ 𝑗 ) = 2 ) ) |
| 31 |
30
|
simpld |
⊢ ( ( ( StarGr ‘ 𝑁 ) ∈ USGraph ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) → 𝑗 ⊆ 𝑊 ) |
| 32 |
25 26 31
|
syl2an |
⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ ( 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) → 𝑗 ⊆ 𝑊 ) |
| 33 |
|
foimacnv |
⊢ ( ( 𝐹 : 𝐶 –onto→ 𝑊 ∧ 𝑗 ⊆ 𝑊 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑗 ) ) = 𝑗 ) |
| 34 |
23 32 33
|
syl2an2r |
⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ ( 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑗 ) ) = 𝑗 ) |
| 35 |
|
imaeq2 |
⊢ ( 𝑘 = ( ◡ 𝐹 “ 𝑗 ) → ( 𝐹 “ 𝑘 ) = ( 𝐹 “ ( ◡ 𝐹 “ 𝑗 ) ) ) |
| 36 |
35
|
eqcomd |
⊢ ( 𝑘 = ( ◡ 𝐹 “ 𝑗 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑗 ) ) = ( 𝐹 “ 𝑘 ) ) |
| 37 |
34 36
|
sylan9req |
⊢ ( ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ ( 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) ∧ 𝑘 = ( ◡ 𝐹 “ 𝑗 ) ) → 𝑗 = ( 𝐹 “ 𝑘 ) ) |
| 38 |
|
imaeq2 |
⊢ ( 𝑗 = ( 𝐹 “ 𝑘 ) → ( ◡ 𝐹 “ 𝑗 ) = ( ◡ 𝐹 “ ( 𝐹 “ 𝑘 ) ) ) |
| 39 |
|
f1of1 |
⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 → 𝐹 : 𝐶 –1-1→ 𝑊 ) |
| 40 |
39
|
ad2antrl |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → 𝐹 : 𝐶 –1-1→ 𝑊 ) |
| 41 |
|
usgruhgr |
⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UHGraph ) |
| 42 |
41
|
ad2antrr |
⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → 𝐺 ∈ UHGraph ) |
| 43 |
1
|
clnbgrssvtx |
⊢ ( 𝐺 ClNeighbVtx 𝑋 ) ⊆ 𝑉 |
| 44 |
3 43
|
eqsstri |
⊢ 𝐶 ⊆ 𝑉 |
| 45 |
44
|
a1i |
⊢ ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) → 𝐶 ⊆ 𝑉 ) |
| 46 |
|
eqid |
⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 ) |
| 47 |
|
eqid |
⊢ ( 𝐺 ISubGr 𝐶 ) = ( 𝐺 ISubGr 𝐶 ) |
| 48 |
1 46 47 8
|
isubgredg |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐶 ⊆ 𝑉 ) → ( 𝑘 ∈ 𝐼 ↔ ( 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑘 ⊆ 𝐶 ) ) ) |
| 49 |
42 45 48
|
syl2an |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → ( 𝑘 ∈ 𝐼 ↔ ( 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑘 ⊆ 𝐶 ) ) ) |
| 50 |
|
simpr |
⊢ ( ( 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑘 ⊆ 𝐶 ) → 𝑘 ⊆ 𝐶 ) |
| 51 |
50
|
a1d |
⊢ ( ( 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑘 ⊆ 𝐶 ) → ( 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) → 𝑘 ⊆ 𝐶 ) ) |
| 52 |
49 51
|
biimtrdi |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → ( 𝑘 ∈ 𝐼 → ( 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) → 𝑘 ⊆ 𝐶 ) ) ) |
| 53 |
52
|
imp32 |
⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ ( 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) → 𝑘 ⊆ 𝐶 ) |
| 54 |
|
f1imacnv |
⊢ ( ( 𝐹 : 𝐶 –1-1→ 𝑊 ∧ 𝑘 ⊆ 𝐶 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑘 ) ) = 𝑘 ) |
| 55 |
40 53 54
|
syl2an2r |
⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ ( 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑘 ) ) = 𝑘 ) |
| 56 |
38 55
|
sylan9eqr |
⊢ ( ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ ( 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) ∧ 𝑗 = ( 𝐹 “ 𝑘 ) ) → ( ◡ 𝐹 “ 𝑗 ) = 𝑘 ) |
| 57 |
56
|
eqcomd |
⊢ ( ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ ( 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) ∧ 𝑗 = ( 𝐹 “ 𝑘 ) ) → 𝑘 = ( ◡ 𝐹 “ 𝑗 ) ) |
| 58 |
37 57
|
impbida |
⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ ( 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) → ( 𝑘 = ( ◡ 𝐹 “ 𝑗 ) ↔ 𝑗 = ( 𝐹 “ 𝑘 ) ) ) |
| 59 |
12 19 21 58
|
f1o2d |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → 𝐻 : 𝐼 –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) |