Metamath Proof Explorer

Theorem dfgrlic3

Description: Alternate, explicit definition of the "is locally isomorphic to" relation for two graphs. (Contributed by AV, 9-Jun-2025)

Ref Expression
Hypotheses dfgrlic2.v ⊢ V = Vtx ⁡ G
dfgrlic2.w ⊢ W = Vtx ⁡ H
dfgrlic3.i ⊢ I = iEdg ⁡ G
dfgrlic3.j ⊢ J = iEdg ⁡ H
dfgrlic3.n ⊢ N = G ClNeighbVtx v
dfgrlic3.m ⊢ M = H ClNeighbVtx f ⁡ v
dfgrlic3.k ⊢ K = x ∈ dom ⁡ I | I ⁡ x ⊆ N
dfgrlic3.l ⊢ L = x ∈ dom ⁡ J | J ⁡ x ⊆ M
Assertion dfgrlic3 ⊢ G ∈ X ∧ H ∈ Y → G ≃ 𝑙𝑔𝑟 H ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∀ v ∈ V ∃ j j : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K j I ⁡ i = J ⁡ g ⁡ i

Proof

Step Hyp Ref Expression
1 dfgrlic2.v ⊢ V = Vtx ⁡ G
2 dfgrlic2.w ⊢ W = Vtx ⁡ H
3 dfgrlic3.i ⊢ I = iEdg ⁡ G
4 dfgrlic3.j ⊢ J = iEdg ⁡ H
5 dfgrlic3.n ⊢ N = G ClNeighbVtx v
6 dfgrlic3.m ⊢ M = H ClNeighbVtx f ⁡ v
7 dfgrlic3.k ⊢ K = x ∈ dom ⁡ I | I ⁡ x ⊆ N
8 dfgrlic3.l ⊢ L = x ∈ dom ⁡ J | J ⁡ x ⊆ M
9 brgrlic ⊢ G ≃ 𝑙𝑔𝑟 H ↔ G GraphLocIso H ≠ ∅
10 n0 ⊢ G GraphLocIso H ≠ ∅ ↔ ∃ f f ∈ G GraphLocIso H
11 9 10 bitri ⊢ G ≃ 𝑙𝑔𝑟 H ↔ ∃ f f ∈ G GraphLocIso H
12 1 2 5 6 3 4 7 8 isgrlim2 ⊢ G ∈ X ∧ H ∈ Y ∧ f ∈ V → f ∈ G GraphLocIso H ↔ f : V ⟶ 1-1 onto W ∧ ∀ v ∈ V ∃ j j : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K j I ⁡ i = J ⁡ g ⁡ i
13 12 el3v3 ⊢ G ∈ X ∧ H ∈ Y → f ∈ G GraphLocIso H ↔ f : V ⟶ 1-1 onto W ∧ ∀ v ∈ V ∃ j j : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K j I ⁡ i = J ⁡ g ⁡ i
14 13 exbidv ⊢ G ∈ X ∧ H ∈ Y → ∃ f f ∈ G GraphLocIso H ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∀ v ∈ V ∃ j j : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K j I ⁡ i = J ⁡ g ⁡ i
15 11 14 bitrid ⊢ G ∈ X ∧ H ∈ Y → G ≃ 𝑙𝑔𝑟 H ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∀ v ∈ V ∃ j j : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K j I ⁡ i = J ⁡ g ⁡ i