This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gricbri

Description: Implications of two graphs being isomorphic. (Contributed by AV, 11-Nov-2022) (Revised by AV, 5-May-2025) (Proof shortened by AV, 12-Jun-2025)

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

Proof

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