Metamath Proof Explorer

Theorem grimprop

Description: Properties of an isomorphism of graphs. (Contributed by AV, 29-Apr-2025)

Ref Expression
Hypotheses grimprop.v ⊢ V = Vtx ⁡ G
grimprop.w ⊢ W = Vtx ⁡ H
grimprop.e ⊢ E = iEdg ⁡ G
grimprop.d ⊢ D = iEdg ⁡ H
Assertion grimprop ⊢ F ∈ G GraphIso H → F : V ⟶ 1-1 onto W ∧ ∃ j j : dom ⁡ E ⟶ 1-1 onto dom ⁡ D ∧ ∀ i ∈ dom ⁡ E D ⁡ j ⁡ i = F E ⁡ i

Proof

Step Hyp Ref Expression
1 grimprop.v ⊢ V = Vtx ⁡ G
2 grimprop.w ⊢ W = Vtx ⁡ H
3 grimprop.e ⊢ E = iEdg ⁡ G
4 grimprop.d ⊢ D = iEdg ⁡ H
5 grimdmrel ⊢ Rel ⁡ dom ⁡ GraphIso
6 5 ovrcl ⊢ F ∈ G GraphIso H → G ∈ V ∧ H ∈ V
7 6 simpld ⊢ F ∈ G GraphIso H → G ∈ V
8 6 simprd ⊢ F ∈ G GraphIso H → H ∈ V
9 id ⊢ F ∈ G GraphIso H → F ∈ G GraphIso H
10 7 8 9 3jca ⊢ F ∈ G GraphIso H → G ∈ V ∧ H ∈ V ∧ F ∈ G GraphIso H
11 1 2 3 4 isgrim ⊢ G ∈ V ∧ H ∈ V ∧ F ∈ G GraphIso H → F ∈ G GraphIso H ↔ F : V ⟶ 1-1 onto W ∧ ∃ j j : dom ⁡ E ⟶ 1-1 onto dom ⁡ D ∧ ∀ i ∈ dom ⁡ E D ⁡ j ⁡ i = F E ⁡ i
12 11 biimpd ⊢ G ∈ V ∧ H ∈ V ∧ F ∈ G GraphIso H → F ∈ G GraphIso H → F : V ⟶ 1-1 onto W ∧ ∃ j j : dom ⁡ E ⟶ 1-1 onto dom ⁡ D ∧ ∀ i ∈ dom ⁡ E D ⁡ j ⁡ i = F E ⁡ i
13 10 12 mpcom ⊢ F ∈ G GraphIso H → F : V ⟶ 1-1 onto W ∧ ∃ j j : dom ⁡ E ⟶ 1-1 onto dom ⁡ D ∧ ∀ i ∈ dom ⁡ E D ⁡ j ⁡ i = F E ⁡ i