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 ⊢ V = Vtx ⁡ A
dfgric2.w ⊢ W = Vtx ⁡ B
dfgric2.i ⊢ I = iEdg ⁡ A
dfgric2.j ⊢ J = iEdg ⁡ B
Assertion gricbri ⊢ A ≃ 𝑔𝑟 B → ∃ f f : V ⟶ 1-1 onto W ∧ ∃ g g : dom ⁡ I ⟶ 1-1 onto dom ⁡ J ∧ ∀ i ∈ dom ⁡ I f I ⁡ i = J ⁡ g ⁡ i

Proof

Step Hyp Ref Expression
1 dfgric2.v ⊢ V = Vtx ⁡ A
2 dfgric2.w ⊢ W = Vtx ⁡ B
3 dfgric2.i ⊢ I = iEdg ⁡ A
4 dfgric2.j ⊢ J = iEdg ⁡ B
5 gricrcl ⊢ A ≃ 𝑔𝑟 B → A ∈ V ∧ B ∈ V
6 1 2 3 4 dfgric2 ⊢ A ∈ V ∧ B ∈ V → A ≃ 𝑔𝑟 B ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∃ g g : dom ⁡ I ⟶ 1-1 onto dom ⁡ J ∧ ∀ i ∈ dom ⁡ I f I ⁡ i = J ⁡ g ⁡ i
7 5 6 syl ⊢ A ≃ 𝑔𝑟 B → A ≃ 𝑔𝑟 B ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∃ g g : dom ⁡ I ⟶ 1-1 onto dom ⁡ J ∧ ∀ i ∈ dom ⁡ I f I ⁡ i = J ⁡ g ⁡ i
8 7 ibi ⊢ A ≃ 𝑔𝑟 B → ∃ f f : V ⟶ 1-1 onto W ∧ ∃ g g : dom ⁡ I ⟶ 1-1 onto dom ⁡ J ∧ ∀ i ∈ dom ⁡ I f I ⁡ i = J ⁡ g ⁡ i