Metamath Proof Explorer

Theorem clnbgrisubgrgrim

Description: Isomorphic subgraphs induced by closed neighborhoods of vertices of two graphs. (Contributed by AV, 29-May-2025)

Ref Expression
Hypotheses clnbgrisubgrgrim.i ⊢ I = iEdg ⁡ G
clnbgrisubgrgrim.j ⊢ J = iEdg ⁡ H
clnbgrisubgrgrim.n ⊢ N = G ClNeighbVtx X
clnbgrisubgrgrim.m ⊢ M = H ClNeighbVtx Y
clnbgrisubgrgrim.k ⊢ K = x ∈ dom ⁡ I | I ⁡ x ⊆ N
clnbgrisubgrgrim.l ⊢ L = x ∈ dom ⁡ J | J ⁡ x ⊆ M
Assertion clnbgrisubgrgrim ⊢ G ∈ U ∧ H ∈ T → G ISubGr N ≃ 𝑔𝑟 H ISubGr M ↔ ∃ f f : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K f I ⁡ i = J ⁡ g ⁡ i

Proof

Step Hyp Ref Expression
1 clnbgrisubgrgrim.i ⊢ I = iEdg ⁡ G
2 clnbgrisubgrgrim.j ⊢ J = iEdg ⁡ H
3 clnbgrisubgrgrim.n ⊢ N = G ClNeighbVtx X
4 clnbgrisubgrgrim.m ⊢ M = H ClNeighbVtx Y
5 clnbgrisubgrgrim.k ⊢ K = x ∈ dom ⁡ I | I ⁡ x ⊆ N
6 clnbgrisubgrgrim.l ⊢ L = x ∈ dom ⁡ J | J ⁡ x ⊆ M
7 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
8 7 clnbgrssvtx ⊢ G ClNeighbVtx X ⊆ Vtx ⁡ G
9 3 8 eqsstri ⊢ N ⊆ Vtx ⁡ G
10 eqid ⊢ Vtx ⁡ H = Vtx ⁡ H
11 10 clnbgrssvtx ⊢ H ClNeighbVtx Y ⊆ Vtx ⁡ H
12 4 11 eqsstri ⊢ M ⊆ Vtx ⁡ H
13 7 10 1 2 5 6 isubgrgrim ⊢ G ∈ U ∧ H ∈ T ∧ N ⊆ Vtx ⁡ G ∧ M ⊆ Vtx ⁡ H → G ISubGr N ≃ 𝑔𝑟 H ISubGr M ↔ ∃ f f : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K f I ⁡ i = J ⁡ g ⁡ i
14 9 12 13 mpanr12 ⊢ G ∈ U ∧ H ∈ T → G ISubGr N ≃ 𝑔𝑟 H ISubGr M ↔ ∃ f f : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K f I ⁡ i = J ⁡ g ⁡ i