Metamath Proof Explorer

Theorem dfgrlic2

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
Assertion dfgrlic2 ⊢ G ∈ X ∧ H ∈ Y → G ≃ 𝑙𝑔𝑟 H ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∀ v ∈ V G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx f ⁡ v

Proof

Step Hyp Ref Expression
1 dfgrlic2.v ⊢ V = Vtx ⁡ G
2 dfgrlic2.w ⊢ W = Vtx ⁡ H
3 brgrlic ⊢ G ≃ 𝑙𝑔𝑟 H ↔ G GraphLocIso H ≠ ∅
4 n0 ⊢ G GraphLocIso H ≠ ∅ ↔ ∃ f f ∈ G GraphLocIso H
5 3 4 bitri ⊢ G ≃ 𝑙𝑔𝑟 H ↔ ∃ f f ∈ G GraphLocIso H
6 1 2 isgrlim ⊢ G ∈ X ∧ H ∈ Y ∧ f ∈ V → f ∈ G GraphLocIso H ↔ f : V ⟶ 1-1 onto W ∧ ∀ v ∈ V G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx f ⁡ v
7 6 el3v3 ⊢ G ∈ X ∧ H ∈ Y → f ∈ G GraphLocIso H ↔ f : V ⟶ 1-1 onto W ∧ ∀ v ∈ V G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx f ⁡ v
8 7 exbidv ⊢ G ∈ X ∧ H ∈ Y → ∃ f f ∈ G GraphLocIso H ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∀ v ∈ V G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx f ⁡ v
9 5 8 bitrid ⊢ G ∈ X ∧ H ∈ Y → G ≃ 𝑙𝑔𝑟 H ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∀ v ∈ V G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx f ⁡ v