| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 2 | | eqid 2737 |
. . . 4
⊢
(Vtx‘𝐻) =
(Vtx‘𝐻) |
| 3 | 1, 2 | grimf1o 47870 |
. . 3
⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) |
| 4 | 3 | 3ad2ant3 1136 |
. 2
⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → 𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻)) |
| 5 | | simpl1 1192 |
. . . . 5
⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑣 ∈ (Vtx‘𝐺)) → 𝐺 ∈ UHGraph) |
| 6 | | simpl3 1194 |
. . . . 5
⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑣 ∈ (Vtx‘𝐺)) → 𝐹 ∈ (𝐺 GraphIso 𝐻)) |
| 7 | 1 | clnbgrssvtx 47818 |
. . . . . 6
⊢ (𝐺 ClNeighbVtx 𝑣) ⊆ (Vtx‘𝐺) |
| 8 | 7 | a1i 11 |
. . . . 5
⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑣 ∈ (Vtx‘𝐺)) → (𝐺 ClNeighbVtx 𝑣) ⊆ (Vtx‘𝐺)) |
| 9 | 1 | uhgrimisgrgric 47899 |
. . . . 5
⊢ ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝐺 ClNeighbVtx 𝑣) ⊆ (Vtx‘𝐺)) → (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐹 “ (𝐺 ClNeighbVtx 𝑣)))) |
| 10 | 5, 6, 8, 9 | syl3anc 1373 |
. . . 4
⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑣 ∈ (Vtx‘𝐺)) → (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐹 “ (𝐺 ClNeighbVtx 𝑣)))) |
| 11 | | df-3an 1089 |
. . . . . 6
⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ↔ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻))) |
| 12 | 1 | clnbgrgrim 47902 |
. . . . . 6
⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑣 ∈ (Vtx‘𝐺)) → (𝐻 ClNeighbVtx (𝐹‘𝑣)) = (𝐹 “ (𝐺 ClNeighbVtx 𝑣))) |
| 13 | 11, 12 | sylanb 581 |
. . . . 5
⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑣 ∈ (Vtx‘𝐺)) → (𝐻 ClNeighbVtx (𝐹‘𝑣)) = (𝐹 “ (𝐺 ClNeighbVtx 𝑣))) |
| 14 | 13 | oveq2d 7447 |
. . . 4
⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑣 ∈ (Vtx‘𝐺)) → (𝐻 ISubGr (𝐻 ClNeighbVtx (𝐹‘𝑣))) = (𝐻 ISubGr (𝐹 “ (𝐺 ClNeighbVtx 𝑣)))) |
| 15 | 10, 14 | breqtrrd 5171 |
. . 3
⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑣 ∈ (Vtx‘𝐺)) → (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝐹‘𝑣)))) |
| 16 | 15 | ralrimiva 3146 |
. 2
⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝐹‘𝑣)))) |
| 17 | 1, 2 | isgrlim 47949 |
. 2
⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐹 ∈ (𝐺 GraphLocIso 𝐻) ↔ (𝐹:(Vtx‘𝐺)–1-1-onto→(Vtx‘𝐻) ∧ ∀𝑣 ∈ (Vtx‘𝐺)(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝐹‘𝑣)))))) |
| 18 | 4, 16, 17 | mpbir2and 713 |
1
⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → 𝐹 ∈ (𝐺 GraphLocIso 𝐻)) |