Theorem isisomgr

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

	Ref	Expression
Hypotheses	isomgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐴 )
	isomgr.w	⊢ 𝑊 = ( Vtx ‘ 𝐵 )
	isomgr.i	⊢ 𝐼 = ( iEdg ‘ 𝐴 )
	isomgr.j	⊢ 𝐽 = ( iEdg ‘ 𝐵 )
Assertion	isisomgr	⊢ ( 𝐴 IsomGr 𝐵 → ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isomgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐴 )
2		isomgr.w	⊢ 𝑊 = ( Vtx ‘ 𝐵 )
3		isomgr.i	⊢ 𝐼 = ( iEdg ‘ 𝐴 )
4		isomgr.j	⊢ 𝐽 = ( iEdg ‘ 𝐵 )
5		isomgrrel	⊢ Rel IsomGr
6	5	brrelex12i	⊢ ( 𝐴 IsomGr 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
7	1 2 3 4	isomgr	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 IsomGr 𝐵 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
8	6 7	syl	⊢ ( 𝐴 IsomGr 𝐵 → ( 𝐴 IsomGr 𝐵 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
9	8	ibi	⊢ ( 𝐴 IsomGr 𝐵 → ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) )