Metamath Proof Explorer

Theorem grimdmrel

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

		Ref	Expression
	Assertion	grimdmrel	\|- Rel dom GraphIso

Proof

Step	Hyp	Ref	Expression
1		df-grim	\|- GraphIso = ( g e. _V , h e. _V \|-> { f \| ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) /\ E. j [. ( iEdg ` g ) / e ]. [. ( iEdg ` h ) / d ]. ( j : dom e -1-1-onto-> dom d /\ A. i e. dom e ( d ` ( j ` i ) ) = ( f " ( e ` i ) ) ) ) } )
2	1	reldmmpo	\|- Rel dom GraphIso

Step

Hyp

Ref

Expression

df-grim

 |-  GraphIso = ( g e. _V , h e. _V |-> { f | ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) /\ E. j [. ( iEdg ` g ) / e ]. [. ( iEdg ` h ) / d ]. ( j : dom e -1-1-onto-> dom d /\ A. i e. dom e ( d ` ( j ` i ) ) = ( f " ( e ` i ) ) ) ) } )

reldmmpo

 |-  Rel dom GraphIso