Metamath Proof Explorer

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 = ( g e. _V , h e. _V \|-> { f \| ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) /\ A. v e. ( Vtx ` g ) ( g ISubGr ( g ClNeighbVtx v ) ) ~=gr ( h ISubGr ( h ClNeighbVtx ( f ` v ) ) ) ) } )
2	1	reldmmpo	\|- Rel dom GraphLocIso

Step

Hyp

Ref

Expression

df-grlim

 |-  GraphLocIso = ( g e. _V , h e. _V |-> { f | ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) /\ A. v e. ( Vtx ` g ) ( g ISubGr ( g ClNeighbVtx v ) ) ~=gr ( h ISubGr ( h ClNeighbVtx ( f ` v ) ) ) ) } )

reldmmpo

 |-  Rel dom GraphLocIso