Definition df-grim

Description: An isomorphism between two graphs is a bijection between the sets of vertices of the two graphs that preserves adjacency, see definition in Diestel p. 3. (Contributed by AV, 19-Apr-2025)

	Ref	Expression
Assertion	df-grim	⊢ GraphIso = ( 𝑔 ∈ V , ℎ ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∃ 𝑗 [ ( iEdg ‘ 𝑔 ) / 𝑒 ] [ ( iEdg ‘ ℎ ) / 𝑑 ] ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ∧ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgrim	⊢ GraphIso
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		vh	⊢ ℎ
4		vf	⊢ 𝑓
5	4	cv	⊢ 𝑓
6		cvtx	⊢ Vtx
7	1	cv	⊢ 𝑔
8	7 6	cfv	⊢ ( Vtx ‘ 𝑔 )
9	3	cv	⊢ ℎ
10	9 6	cfv	⊢ ( Vtx ‘ ℎ )
11	8 10 5	wf1o	⊢ 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ )
12		vj	⊢ 𝑗
13		ciedg	⊢ iEdg
14	7 13	cfv	⊢ ( iEdg ‘ 𝑔 )
15		ve	⊢ 𝑒
16	9 13	cfv	⊢ ( iEdg ‘ ℎ )
17		vd	⊢ 𝑑
18	12	cv	⊢ 𝑗
19	15	cv	⊢ 𝑒
20	19	cdm	⊢ dom 𝑒
21	17	cv	⊢ 𝑑
22	21	cdm	⊢ dom 𝑑
23	20 22 18	wf1o	⊢ 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑
24		vi	⊢ 𝑖
25	24	cv	⊢ 𝑖
26	25 18	cfv	⊢ ( 𝑗 ‘ 𝑖 )
27	26 21	cfv	⊢ ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) )
28	25 19	cfv	⊢ ( 𝑒 ‘ 𝑖 )
29	5 28	cima	⊢ ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) )
30	27 29	wceq	⊢ ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) )
31	30 24 20	wral	⊢ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) )
32	23 31	wa	⊢ ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ∧ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) )
33	32 17 16	wsbc	⊢ [ ( iEdg ‘ ℎ ) / 𝑑 ] ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ∧ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) )
34	33 15 14	wsbc	⊢ [ ( iEdg ‘ 𝑔 ) / 𝑒 ] [ ( iEdg ‘ ℎ ) / 𝑑 ] ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ∧ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) )
35	34 12	wex	⊢ ∃ 𝑗 [ ( iEdg ‘ 𝑔 ) / 𝑒 ] [ ( iEdg ‘ ℎ ) / 𝑑 ] ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ∧ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) )
36	11 35	wa	⊢ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∃ 𝑗 [ ( iEdg ‘ 𝑔 ) / 𝑒 ] [ ( iEdg ‘ ℎ ) / 𝑑 ] ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ∧ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) ) )
37	36 4	cab	⊢ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∃ 𝑗 [ ( iEdg ‘ 𝑔 ) / 𝑒 ] [ ( iEdg ‘ ℎ ) / 𝑑 ] ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ∧ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) ) ) }
38	1 3 2 2 37	cmpo	⊢ ( 𝑔 ∈ V , ℎ ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∃ 𝑗 [ ( iEdg ‘ 𝑔 ) / 𝑒 ] [ ( iEdg ‘ ℎ ) / 𝑑 ] ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ∧ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) ) ) } )
39	0 38	wceq	⊢ GraphIso = ( 𝑔 ∈ V , ℎ ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∃ 𝑗 [ ( iEdg ‘ 𝑔 ) / 𝑒 ] [ ( iEdg ‘ ℎ ) / 𝑑 ] ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ∧ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) ) ) } )