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

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 = ( 𝑔 ∈ V , ℎ ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∃ 𝑗 [ ( iEdg ‘ 𝑔 ) / 𝑒 ] [ ( iEdg ‘ ℎ ) / 𝑑 ] ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ∧ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) ) ) } )
2 f1of ⊢ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) → 𝑓 : ( Vtx ‘ 𝑔 ) ⟶ ( Vtx ‘ ℎ ) )
3 fvex ⊢ ( Vtx ‘ ℎ ) ∈ V
4 fvex ⊢ ( Vtx ‘ 𝑔 ) ∈ V
5 3 4 elmap ⊢ ( 𝑓 ∈ ( ( Vtx ‘ ℎ ) ↑m ( Vtx ‘ 𝑔 ) ) ↔ 𝑓 : ( Vtx ‘ 𝑔 ) ⟶ ( Vtx ‘ ℎ ) )
6 2 5 sylibr ⊢ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) → 𝑓 ∈ ( ( Vtx ‘ ℎ ) ↑m ( Vtx ‘ 𝑔 ) ) )
7 6 adantr ⊢ ( ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∃ 𝑗 [ ( iEdg ‘ 𝑔 ) / 𝑒 ] [ ( iEdg ‘ ℎ ) / 𝑑 ] ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ∧ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) ) ) → 𝑓 ∈ ( ( Vtx ‘ ℎ ) ↑m ( Vtx ‘ 𝑔 ) ) )
8 ovex ⊢ ( ( Vtx ‘ ℎ ) ↑m ( Vtx ‘ 𝑔 ) ) ∈ V
9 7 8 abex ⊢ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∃ 𝑗 [ ( iEdg ‘ 𝑔 ) / 𝑒 ] [ ( iEdg ‘ ℎ ) / 𝑑 ] ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ∧ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) ) ) } ∈ V
10 1 9 fnmpoi ⊢ GraphIso Fn ( V × V )