Metamath Proof Explorer

Theorem isomgrrel

Description: The isomorphy relation for graphs is a relation. (Contributed by AV, 11-Nov-2022)

		Ref	Expression
	Assertion	isomgrrel	\|- Rel IsomGr

Proof

Step	Hyp	Ref	Expression
1		df-isomgr	\|- IsomGr = { <. x , y >. \| E. f ( f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y ) /\ E. g ( g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y ) /\ A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) ) ) ) }
2	1	relopabiv	\|- Rel IsomGr

Step

Hyp

Ref

Expression

df-isomgr

 |-  IsomGr = { <. x , y >. | E. f ( f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y ) /\ E. g ( g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y ) /\ A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) ) ) ) }

relopabiv

 |-  Rel IsomGr