Metamath Proof Explorer

Theorem usgrlimprop

Description: Properties of a local isomorphism of simple pseudographs. (Contributed by AV, 17-Aug-2025)

Ref Expression
Hypotheses usgrlimprop.v ⊢ V = Vtx ⁡ G
usgrlimprop.w ⊢ W = Vtx ⁡ H
usgrlimprop.n ⊢ N = G ClNeighbVtx v
usgrlimprop.m ⊢ M = H ClNeighbVtx F ⁡ v
usgrlimprop.i ⊢ I = Edg ⁡ G
usgrlimprop.j ⊢ J = Edg ⁡ H
usgrlimprop.k ⊢ K = x ∈ I | x ⊆ N
usgrlimprop.l ⊢ L = x ∈ J | x ⊆ M
Assertion usgrlimprop ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ 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 ∧ ∀ e ∈ K f e = g ⁡ e

Proof

Step Hyp Ref Expression
1 usgrlimprop.v ⊢ V = Vtx ⁡ G
2 usgrlimprop.w ⊢ W = Vtx ⁡ H
3 usgrlimprop.n ⊢ N = G ClNeighbVtx v
4 usgrlimprop.m ⊢ M = H ClNeighbVtx F ⁡ v
5 usgrlimprop.i ⊢ I = Edg ⁡ G
6 usgrlimprop.j ⊢ J = Edg ⁡ H
7 usgrlimprop.k ⊢ K = x ∈ I | x ⊆ N
8 usgrlimprop.l ⊢ L = x ∈ J | x ⊆ M
9 simp3 ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F ∈ G GraphLocIso H → F ∈ G GraphLocIso H
10 1 2 3 4 5 6 7 8 uspgrlim ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ 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 ∧ ∀ e ∈ K f e = g ⁡ e
11 9 10 mpbid ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ 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 ∧ ∀ e ∈ K f e = g ⁡ e