Metamath Proof Explorer

Theorem grimfn

Description: The graph isomorphism function is a well-defined function. (Contributed by AV, 28-Apr-2025)

Ref Expression
Assertion grimfn ⊢ GraphIso Fn V × V

Proof

Step Hyp Ref Expression
1 df-grim ⊢ GraphIso = g ∈ V , h ∈ V ⟼ f | f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∃ j [˙ iEdg ⁡ g / e]˙ [˙ iEdg ⁡ h / d]˙ j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ∧ ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i
2 f1of ⊢ f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h → f : Vtx ⁡ g ⟶ Vtx ⁡ h
3 fvex ⊢ Vtx ⁡ h ∈ V
4 fvex ⊢ Vtx ⁡ g ∈ V
5 3 4 elmap ⊢ f ∈ Vtx ⁡ h Vtx ⁡ g ↔ f : Vtx ⁡ g ⟶ Vtx ⁡ h
6 2 5 sylibr ⊢ f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h → f ∈ Vtx ⁡ h Vtx ⁡ g
7 6 adantr ⊢ f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∃ j [˙ iEdg ⁡ g / e]˙ [˙ iEdg ⁡ h / d]˙ j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ∧ ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i → f ∈ Vtx ⁡ h Vtx ⁡ g
8 ovex ⊢ Vtx ⁡ h Vtx ⁡ g ∈ V
9 7 8 abex ⊢ f | f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∃ j [˙ iEdg ⁡ g / e]˙ [˙ iEdg ⁡ h / d]˙ j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ∧ ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i ∈ V
10 1 9 fnmpoi ⊢ GraphIso Fn V × V