Metamath Proof Explorer

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 → ∃ 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 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 ∈ V ∧ B ∈ V
7 1 2 3 4 isomgr ⊢ A ∈ V ∧ B ∈ V → A IsomGr 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 6 7 syl ⊢ A IsomGr B → A IsomGr 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
9 8 ibi ⊢ A IsomGr 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