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 |
1 2 3 4 5 6 7 8 9
|
isubgr3stgrlem8 |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → 𝐻 : 𝐼 –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) |
11 |
|
f1of |
⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 → 𝐹 : 𝐶 ⟶ 𝑊 ) |
12 |
11
|
ad2antrl |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → 𝐹 : 𝐶 ⟶ 𝑊 ) |
13 |
1 2 3 4 5 6 7 8 9
|
isubgr3stgrlem5 |
⊢ ( ( 𝐹 : 𝐶 ⟶ 𝑊 ∧ 𝑒 ∈ 𝐼 ) → ( 𝐻 ‘ 𝑒 ) = ( 𝐹 “ 𝑒 ) ) |
14 |
13
|
eqcomd |
⊢ ( ( 𝐹 : 𝐶 ⟶ 𝑊 ∧ 𝑒 ∈ 𝐼 ) → ( 𝐹 “ 𝑒 ) = ( 𝐻 ‘ 𝑒 ) ) |
15 |
12 14
|
sylan |
⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑒 ∈ 𝐼 ) → ( 𝐹 “ 𝑒 ) = ( 𝐻 ‘ 𝑒 ) ) |
16 |
15
|
ralrimiva |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → ∀ 𝑒 ∈ 𝐼 ( 𝐹 “ 𝑒 ) = ( 𝐻 ‘ 𝑒 ) ) |
17 |
10 16
|
jca |
⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → ( 𝐻 : 𝐼 –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ 𝐼 ( 𝐹 “ 𝑒 ) = ( 𝐻 ‘ 𝑒 ) ) ) |