Theorem grlimdmrel

Description: The domain of the graph local isomorphism function is a relation. (Contributed by AV, 20-May-2025)

	Ref	Expression
Assertion	grlimdmrel	⊢ Rel dom GraphLocIso

Proof

Step	Hyp	Ref	Expression
1		df-grlim	⊢ GraphLocIso = ( 𝑔 ∈ V , ℎ ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( 𝑔 ISubGr ( 𝑔 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( ℎ ISubGr ( ℎ ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) } )
2	1	reldmmpo	⊢ Rel dom GraphLocIso