This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 𝑔 ∈ V , ℎ ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( 𝑔 ISubGr ( 𝑔 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( ℎ ISubGr ( ℎ ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) } )
2 fvex ⊢ ( Vtx ‘ ℎ ) ∈ V
3 f1of ⊢ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) → 𝑓 : ( Vtx ‘ 𝑔 ) ⟶ ( Vtx ‘ ℎ ) )
4 3 ad2antrl ⊢ ( ( ( Vtx ‘ ℎ ) ∈ V ∧ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( 𝑔 ISubGr ( 𝑔 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( ℎ ISubGr ( ℎ ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ) → 𝑓 : ( Vtx ‘ 𝑔 ) ⟶ ( Vtx ‘ ℎ ) )
5 fvexd ⊢ ( ( Vtx ‘ ℎ ) ∈ V → ( Vtx ‘ 𝑔 ) ∈ V )
6 id ⊢ ( ( Vtx ‘ ℎ ) ∈ V → ( Vtx ‘ ℎ ) ∈ V )
7 4 5 6 fabexd ⊢ ( ( Vtx ‘ ℎ ) ∈ V → { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( 𝑔 ISubGr ( 𝑔 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( ℎ ISubGr ( ℎ ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) } ∈ V )
8 2 7 ax-mp ⊢ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( 𝑔 ISubGr ( 𝑔 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( ℎ ISubGr ( ℎ ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) } ∈ V
9 1 8 fnmpoi ⊢ GraphLocIso Fn ( V × V )