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