Metamath Proof Explorer

Theorem grilcbri

Description: Implications of two graphs being locally isomorphic. (Contributed by AV, 9-Jun-2025)

Ref Expression
Hypotheses dfgrlic2.v ⊢ V = Vtx ⁡ G
dfgrlic2.w ⊢ W = Vtx ⁡ H
Assertion grilcbri ⊢ 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 grlicrcl ⊢ G ≃ 𝑙𝑔𝑟 H → G ∈ V ∧ H ∈ V
4 1 2 dfgrlic2 ⊢ G ∈ V ∧ H ∈ V → G ≃ 𝑙𝑔𝑟 H ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∀ v ∈ V G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx f ⁡ v
5 3 4 syl ⊢ G ≃ 𝑙𝑔𝑟 H → G ≃ 𝑙𝑔𝑟 H ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∀ v ∈ V G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx f ⁡ v
6 5 ibi ⊢ G ≃ 𝑙𝑔𝑟 H → ∃ f f : V ⟶ 1-1 onto W ∧ ∀ v ∈ V G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx f ⁡ v