Theorem isisomgr

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

	Ref	Expression
Hypotheses	isomgr.v	$$⊢V=\mathrm{Vtx}\left(A\right)$$
	isomgr.w	$$⊢W=\mathrm{Vtx}\left(B\right)$$
	isomgr.i	$$⊢I=\mathrm{iEdg}\left(A\right)$$
	isomgr.j	$$⊢J=\mathrm{iEdg}\left(B\right)$$
Assertion	isisomgr	$$⊢A\mathrm{IsomGr}B\to \exists f\left(f:V\underset{1-1\; onto}{⟶}W\wedge \exists g\left(g:\mathrm{dom}I\underset{1-1\; onto}{⟶}\mathrm{dom}J\wedge \forall i\in \mathrm{dom}If\left[I\left(i\right)\right]=J\left(g\left(i\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isomgr.v	$$⊢V=\mathrm{Vtx}\left(A\right)$$
2		isomgr.w	$$⊢W=\mathrm{Vtx}\left(B\right)$$
3		isomgr.i	$$⊢I=\mathrm{iEdg}\left(A\right)$$
4		isomgr.j	$$⊢J=\mathrm{iEdg}\left(B\right)$$
5		isomgrrel	$$⊢\mathrm{Rel}\mathrm{IsomGr}$$
6	5	brrelex12i	$$⊢A\mathrm{IsomGr}B\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
7	1 2 3 4	isomgr	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \left(A\mathrm{IsomGr}B\leftrightarrow \exists f\left(f:V\underset{1-1\; onto}{⟶}W\wedge \exists g\left(g:\mathrm{dom}I\underset{1-1\; onto}{⟶}\mathrm{dom}J\wedge \forall i\in \mathrm{dom}If\left[I\left(i\right)\right]=J\left(g\left(i\right)\right)\right)\right)\right)$$
8	6 7	syl	$$⊢A\mathrm{IsomGr}B\to \left(A\mathrm{IsomGr}B\leftrightarrow \exists f\left(f:V\underset{1-1\; onto}{⟶}W\wedge \exists g\left(g:\mathrm{dom}I\underset{1-1\; onto}{⟶}\mathrm{dom}J\wedge \forall i\in \mathrm{dom}If\left[I\left(i\right)\right]=J\left(g\left(i\right)\right)\right)\right)\right)$$
9	8	ibi	$$⊢A\mathrm{IsomGr}B\to \exists f\left(f:V\underset{1-1\; onto}{⟶}W\wedge \exists g\left(g:\mathrm{dom}I\underset{1-1\; onto}{⟶}\mathrm{dom}J\wedge \forall i\in \mathrm{dom}If\left[I\left(i\right)\right]=J\left(g\left(i\right)\right)\right)\right)$$