| 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 |
9
|
a1i |
⊢ ( ( 𝐹 : 𝐶 ⟶ 𝑊 ∧ 𝑌 ∈ 𝐼 ) → 𝐻 = ( 𝑖 ∈ 𝐼 ↦ ( 𝐹 “ 𝑖 ) ) ) |
| 11 |
|
imaeq2 |
⊢ ( 𝑖 = 𝑌 → ( 𝐹 “ 𝑖 ) = ( 𝐹 “ 𝑌 ) ) |
| 12 |
11
|
adantl |
⊢ ( ( ( 𝐹 : 𝐶 ⟶ 𝑊 ∧ 𝑌 ∈ 𝐼 ) ∧ 𝑖 = 𝑌 ) → ( 𝐹 “ 𝑖 ) = ( 𝐹 “ 𝑌 ) ) |
| 13 |
|
simpr |
⊢ ( ( 𝐹 : 𝐶 ⟶ 𝑊 ∧ 𝑌 ∈ 𝐼 ) → 𝑌 ∈ 𝐼 ) |
| 14 |
|
id |
⊢ ( 𝐹 : 𝐶 ⟶ 𝑊 → 𝐹 : 𝐶 ⟶ 𝑊 ) |
| 15 |
3
|
ovexi |
⊢ 𝐶 ∈ V |
| 16 |
15
|
a1i |
⊢ ( 𝐹 : 𝐶 ⟶ 𝑊 → 𝐶 ∈ V ) |
| 17 |
14 16
|
fexd |
⊢ ( 𝐹 : 𝐶 ⟶ 𝑊 → 𝐹 ∈ V ) |
| 18 |
17
|
adantr |
⊢ ( ( 𝐹 : 𝐶 ⟶ 𝑊 ∧ 𝑌 ∈ 𝐼 ) → 𝐹 ∈ V ) |
| 19 |
18
|
imaexd |
⊢ ( ( 𝐹 : 𝐶 ⟶ 𝑊 ∧ 𝑌 ∈ 𝐼 ) → ( 𝐹 “ 𝑌 ) ∈ V ) |
| 20 |
10 12 13 19
|
fvmptd |
⊢ ( ( 𝐹 : 𝐶 ⟶ 𝑊 ∧ 𝑌 ∈ 𝐼 ) → ( 𝐻 ‘ 𝑌 ) = ( 𝐹 “ 𝑌 ) ) |