Theorem isisomgr

Description: Implications of two graphs being isomorphic. (Contributed by AV, 11-Nov-2022)

	Ref	Expression
Hypotheses	isomgr.v	|- V = ( Vtx ` A )
	isomgr.w	|- W = ( Vtx ` B )
	isomgr.i	|- I = ( iEdg ` A )
	isomgr.j	|- J = ( iEdg ` B )
Assertion	isisomgr	|- ( A IsomGr B -> E. f ( f : V -1-1-onto-> W /\ E. g ( g : dom I -1-1-onto-> dom J /\ A. i e. dom I ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isomgr.v	|- V = ( Vtx ` A )
2		isomgr.w	|- W = ( Vtx ` B )
3		isomgr.i	|- I = ( iEdg ` A )
4		isomgr.j	|- J = ( iEdg ` B )
5		isomgrrel	|- Rel IsomGr
6	5	brrelex12i	|- ( A IsomGr B -> ( A e. _V /\ B e. _V ) )
7	1 2 3 4	isomgr	|- ( ( A e. _V /\ B e. _V ) -> ( A IsomGr B <-> E. f ( f : V -1-1-onto-> W /\ E. g ( g : dom I -1-1-onto-> dom J /\ A. i e. dom I ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) )
8	6 7	syl	|- ( A IsomGr B -> ( A IsomGr B <-> E. f ( f : V -1-1-onto-> W /\ E. g ( g : dom I -1-1-onto-> dom J /\ A. i e. dom I ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) )
9	8	ibi	|- ( A IsomGr B -> E. f ( f : V -1-1-onto-> W /\ E. g ( g : dom I -1-1-onto-> dom J /\ A. i e. dom I ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) )