Metamath Proof Explorer

Theorem grlimprop2

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

Ref Expression
Hypotheses grlimprop.v ⊢ V = Vtx ⁡ G
grlimprop.w ⊢ W = Vtx ⁡ H
grlimprop2.n ⊢ N = G ClNeighbVtx v
grlimprop2.m ⊢ M = H ClNeighbVtx F ⁡ v
grlimprop2.i ⊢ I = iEdg ⁡ G
grlimprop2.j ⊢ J = iEdg ⁡ H
grlimprop2.k ⊢ K = x ∈ dom ⁡ I | I ⁡ x ⊆ N
grlimprop2.l ⊢ L = x ∈ dom ⁡ J | J ⁡ x ⊆ M
Assertion grlimprop2 ⊢ 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 grlimprop.v ⊢ V = Vtx ⁡ G
2 grlimprop.w ⊢ W = Vtx ⁡ H
3 grlimprop2.n ⊢ N = G ClNeighbVtx v
4 grlimprop2.m ⊢ M = H ClNeighbVtx F ⁡ v
5 grlimprop2.i ⊢ I = iEdg ⁡ G
6 grlimprop2.j ⊢ J = iEdg ⁡ H
7 grlimprop2.k ⊢ K = x ∈ dom ⁡ I | I ⁡ x ⊆ N
8 grlimprop2.l ⊢ L = x ∈ dom ⁡ J | J ⁡ x ⊆ M
9 grlimdmrel ⊢ Rel ⁡ dom ⁡ GraphLocIso
10 9 ovrcl ⊢ F ∈ G GraphLocIso H → G ∈ V ∧ H ∈ V
11 id ⊢ F ∈ G GraphLocIso H → F ∈ G GraphLocIso H
12 df-3an ⊢ G ∈ V ∧ H ∈ V ∧ F ∈ G GraphLocIso H ↔ G ∈ V ∧ H ∈ V ∧ F ∈ G GraphLocIso H
13 10 11 12 sylanbrc ⊢ F ∈ G GraphLocIso H → G ∈ V ∧ H ∈ V ∧ F ∈ G GraphLocIso H
14 1 2 3 4 5 6 7 8 isgrlim2 ⊢ G ∈ V ∧ H ∈ V ∧ F ∈ G GraphLocIso H → 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
15 13 14 syl ⊢ F ∈ G GraphLocIso H → 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
16 15 ibi ⊢ 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