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

Metamath Proof Explorer

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 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) ) ) } )