| Step |
Hyp |
Ref |
Expression |
| 1 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
| 2 |
|
eqid |
⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 ) |
| 3 |
1 2
|
grimf1o |
⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ) |
| 4 |
3
|
3ad2ant3 |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ) |
| 5 |
|
simpl1 |
⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → 𝐺 ∈ UHGraph ) |
| 6 |
|
simpl3 |
⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) |
| 7 |
1
|
clnbgrssvtx |
⊢ ( 𝐺 ClNeighbVtx 𝑣 ) ⊆ ( Vtx ‘ 𝐺 ) |
| 8 |
7
|
a1i |
⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ClNeighbVtx 𝑣 ) ⊆ ( Vtx ‘ 𝐺 ) ) |
| 9 |
1
|
uhgrimisgrgric |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐺 ClNeighbVtx 𝑣 ) ⊆ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐹 “ ( 𝐺 ClNeighbVtx 𝑣 ) ) ) ) |
| 10 |
5 6 8 9
|
syl3anc |
⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐹 “ ( 𝐺 ClNeighbVtx 𝑣 ) ) ) ) |
| 11 |
|
df-3an |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ↔ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ) |
| 12 |
1
|
clnbgrgrim |
⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) = ( 𝐹 “ ( 𝐺 ClNeighbVtx 𝑣 ) ) ) |
| 13 |
11 12
|
sylanb |
⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) = ( 𝐹 “ ( 𝐺 ClNeighbVtx 𝑣 ) ) ) |
| 14 |
13
|
oveq2d |
⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) = ( 𝐻 ISubGr ( 𝐹 “ ( 𝐺 ClNeighbVtx 𝑣 ) ) ) ) |
| 15 |
10 14
|
breqtrrd |
⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ) |
| 16 |
15
|
ralrimiva |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ) |
| 17 |
1 2
|
isgrlim |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ) ) ) |
| 18 |
4 16 17
|
mpbir2and |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ) |