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 )