Metamath Proof Explorer

Theorem grlimprop

Description: Properties of a local isomorphism of graphs. (Contributed by AV, 21-May-2025)

Ref Expression
Hypotheses grlimprop.v ⊢ V = Vtx ⁡ G
grlimprop.w ⊢ W = Vtx ⁡ H
Assertion grlimprop ⊢ F ∈ G GraphLocIso H → 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 grlimprop.v ⊢ V = Vtx ⁡ G
2 grlimprop.w ⊢ W = Vtx ⁡ H
3 grlimdmrel ⊢ Rel ⁡ dom ⁡ GraphLocIso
4 3 ovrcl ⊢ F ∈ G GraphLocIso H → G ∈ V ∧ H ∈ V
5 4 simpld ⊢ F ∈ G GraphLocIso H → G ∈ V
6 4 simprd ⊢ F ∈ G GraphLocIso H → H ∈ V
7 id ⊢ F ∈ G GraphLocIso H → F ∈ G GraphLocIso H
8 5 6 7 3jca ⊢ F ∈ G GraphLocIso H → G ∈ V ∧ H ∈ V ∧ F ∈ G GraphLocIso H
9 1 2 isgrlim ⊢ G ∈ V ∧ H ∈ V ∧ F ∈ G GraphLocIso H → F ∈ G GraphLocIso H ↔ F : V ⟶ 1-1 onto W ∧ ∀ v ∈ V G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx F ⁡ v
10 9 biimpd ⊢ G ∈ V ∧ H ∈ V ∧ F ∈ G GraphLocIso H → F ∈ G GraphLocIso H → F : V ⟶ 1-1 onto W ∧ ∀ v ∈ V G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx F ⁡ v
11 8 10 mpcom ⊢ F ∈ G GraphLocIso H → F : V ⟶ 1-1 onto W ∧ ∀ v ∈ V G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx F ⁡ v