Metamath Proof Explorer

Theorem grlimfn

Description: The graph local isomorphism function is a well-defined function. (Contributed by AV, 20-May-2025)

Ref Expression
Assertion grlimfn ⊢ GraphLocIso Fn V × V

Proof

Step Hyp Ref Expression
1 df-grlim ⊢ GraphLocIso = g ∈ V , h ∈ V ⟼ f | f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∀ v ∈ Vtx ⁡ g g ISubGr g ClNeighbVtx v ≃ 𝑔𝑟 h ISubGr h ClNeighbVtx f ⁡ v
2 fvex ⊢ Vtx ⁡ h ∈ V
3 f1of ⊢ f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h → f : Vtx ⁡ g ⟶ Vtx ⁡ h
4 3 ad2antrl ⊢ Vtx ⁡ h ∈ V ∧ f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∀ v ∈ Vtx ⁡ g g ISubGr g ClNeighbVtx v ≃ 𝑔𝑟 h ISubGr h ClNeighbVtx f ⁡ v → f : Vtx ⁡ g ⟶ Vtx ⁡ h
5 fvexd ⊢ Vtx ⁡ h ∈ V → Vtx ⁡ g ∈ V
6 id ⊢ Vtx ⁡ h ∈ V → Vtx ⁡ h ∈ V
7 4 5 6 fabexd ⊢ Vtx ⁡ h ∈ V → f | f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∀ v ∈ Vtx ⁡ g g ISubGr g ClNeighbVtx v ≃ 𝑔𝑟 h ISubGr h ClNeighbVtx f ⁡ v ∈ V
8 2 7 ax-mp ⊢ f | f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∀ v ∈ Vtx ⁡ g g ISubGr g ClNeighbVtx v ≃ 𝑔𝑟 h ISubGr h ClNeighbVtx f ⁡ v ∈ V
9 1 8 fnmpoi ⊢ GraphLocIso Fn V × V