Metamath Proof Explorer

Theorem isgrlim2

Description: A local isomorphism of graphs is a bijection between their vertices that preserves neighborhoods. Definitions expanded. (Contributed by AV, 29-May-2025)

Ref Expression
Hypotheses isgrlim.v ⊢ V = Vtx ⁡ G
isgrlim.w ⊢ W = Vtx ⁡ H
isgrlim2.n ⊢ N = G ClNeighbVtx v
isgrlim2.m ⊢ M = H ClNeighbVtx F ⁡ v
isgrlim2.i ⊢ I = iEdg ⁡ G
isgrlim2.j ⊢ J = iEdg ⁡ H
isgrlim2.k ⊢ K = x ∈ dom ⁡ I | I ⁡ x ⊆ N
isgrlim2.l ⊢ L = x ∈ dom ⁡ J | J ⁡ x ⊆ M
Assertion isgrlim2 ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → F ∈ G GraphLocIso H ↔ F : V ⟶ 1-1 onto W ∧ ∀ v ∈ V ∃ 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 isgrlim.v ⊢ V = Vtx ⁡ G
2 isgrlim.w ⊢ W = Vtx ⁡ H
3 isgrlim2.n ⊢ N = G ClNeighbVtx v
4 isgrlim2.m ⊢ M = H ClNeighbVtx F ⁡ v
5 isgrlim2.i ⊢ I = iEdg ⁡ G
6 isgrlim2.j ⊢ J = iEdg ⁡ H
7 isgrlim2.k ⊢ K = x ∈ dom ⁡ I | I ⁡ x ⊆ N
8 isgrlim2.l ⊢ L = x ∈ dom ⁡ J | J ⁡ x ⊆ M
9 1 2 isgrlim ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → F ∈ G GraphLocIso H ↔ F : V ⟶ 1-1 onto W ∧ ∀ v ∈ V G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx F ⁡ v
10 3 eqcomi ⊢ G ClNeighbVtx v = N
11 10 oveq2i ⊢ G ISubGr G ClNeighbVtx v = G ISubGr N
12 4 eqcomi ⊢ H ClNeighbVtx F ⁡ v = M
13 12 oveq2i ⊢ H ISubGr H ClNeighbVtx F ⁡ v = H ISubGr M
14 11 13 breq12i ⊢ G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx F ⁡ v ↔ G ISubGr N ≃ 𝑔𝑟 H ISubGr M
15 14 a1i ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx F ⁡ v ↔ G ISubGr N ≃ 𝑔𝑟 H ISubGr M
16 5 6 3 4 7 8 clnbgrisubgrgrim ⊢ G ∈ X ∧ H ∈ Y → 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
17 16 3adant3 ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → 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
18 15 17 bitrd ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx F ⁡ v ↔ ∃ f f : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K f I ⁡ i = J ⁡ g ⁡ i
19 18 ralbidv ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → ∀ v ∈ V G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx F ⁡ v ↔ ∀ v ∈ V ∃ f f : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K f I ⁡ i = J ⁡ g ⁡ i
20 19 anbi2d ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → F : V ⟶ 1-1 onto W ∧ ∀ v ∈ V G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx F ⁡ v ↔ F : V ⟶ 1-1 onto W ∧ ∀ v ∈ V ∃ f f : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K f I ⁡ i = J ⁡ g ⁡ i
21 9 20 bitrd ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → F ∈ G GraphLocIso H ↔ F : V ⟶ 1-1 onto W ∧ ∀ v ∈ V ∃ f f : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K f I ⁡ i = J ⁡ g ⁡ i