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

Metamath Proof Explorer

Theorem grimf1o

Description: An isomorphism of graphs is a bijection between their vertices. (Contributed by AV, 29-Apr-2025)

Ref Expression
Hypotheses grimprop.v ⊢ V = Vtx ⁡ G
grimprop.w ⊢ W = Vtx ⁡ H
Assertion grimf1o ⊢ F ∈ G GraphIso H → F : V ⟶ 1-1 onto W

Proof

Step Hyp Ref Expression
1 grimprop.v ⊢ V = Vtx ⁡ G
2 grimprop.w ⊢ W = Vtx ⁡ H
3 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
4 eqid ⊢ iEdg ⁡ H = iEdg ⁡ H
5 1 2 3 4 grimprop ⊢ F ∈ G GraphIso H → F : V ⟶ 1-1 onto W ∧ ∃ j j : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto dom ⁡ iEdg ⁡ H ∧ ∀ i ∈ dom ⁡ iEdg ⁡ G iEdg ⁡ H ⁡ j ⁡ i = F iEdg ⁡ G ⁡ i
6 5 simpld ⊢ F ∈ G GraphIso H → F : V ⟶ 1-1 onto W