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 )