# Metamath Proof Explorer

## Definition df-grisom

Description: Define the class of all isomorphisms between two graphs. (Contributed by AV, 11-Dec-2022)

Ref Expression
Assertion df-grisom GrIsom = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 : ( Vtx ‘ 𝑥 ) –1-1-onto→ ( Vtx ‘ 𝑦 ) ∧ 𝑔 : dom ( iEdg ‘ 𝑥 ) –1-1-onto→ dom ( iEdg ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑥 ) ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔𝑖 ) ) ) } )

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cgrisom GrIsom
1 vx 𝑥
2 cvv V
3 vy 𝑦
4 vf 𝑓
5 vg 𝑔
6 4 cv 𝑓
7 cvtx Vtx
8 1 cv 𝑥
9 8 7 cfv ( Vtx ‘ 𝑥 )
10 3 cv 𝑦
11 10 7 cfv ( Vtx ‘ 𝑦 )
12 9 11 6 wf1o 𝑓 : ( Vtx ‘ 𝑥 ) –1-1-onto→ ( Vtx ‘ 𝑦 )
13 5 cv 𝑔
14 ciedg iEdg
15 8 14 cfv ( iEdg ‘ 𝑥 )
16 15 cdm dom ( iEdg ‘ 𝑥 )
17 10 14 cfv ( iEdg ‘ 𝑦 )
18 17 cdm dom ( iEdg ‘ 𝑦 )
19 16 18 13 wf1o 𝑔 : dom ( iEdg ‘ 𝑥 ) –1-1-onto→ dom ( iEdg ‘ 𝑦 )
20 vi 𝑖
21 20 cv 𝑖
22 21 15 cfv ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 )
23 6 22 cima ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) )
24 21 13 cfv ( 𝑔𝑖 )
25 24 17 cfv ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔𝑖 ) )
26 23 25 wceq ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔𝑖 ) )
27 26 20 16 wral 𝑖 ∈ dom ( iEdg ‘ 𝑥 ) ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔𝑖 ) )
28 12 19 27 w3a ( 𝑓 : ( Vtx ‘ 𝑥 ) –1-1-onto→ ( Vtx ‘ 𝑦 ) ∧ 𝑔 : dom ( iEdg ‘ 𝑥 ) –1-1-onto→ dom ( iEdg ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑥 ) ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔𝑖 ) ) )
29 28 4 5 copab { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 : ( Vtx ‘ 𝑥 ) –1-1-onto→ ( Vtx ‘ 𝑦 ) ∧ 𝑔 : dom ( iEdg ‘ 𝑥 ) –1-1-onto→ dom ( iEdg ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑥 ) ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔𝑖 ) ) ) }
30 1 3 2 2 29 cmpo ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 : ( Vtx ‘ 𝑥 ) –1-1-onto→ ( Vtx ‘ 𝑦 ) ∧ 𝑔 : dom ( iEdg ‘ 𝑥 ) –1-1-onto→ dom ( iEdg ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑥 ) ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔𝑖 ) ) ) } )
31 0 30 wceq GrIsom = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 : ( Vtx ‘ 𝑥 ) –1-1-onto→ ( Vtx ‘ 𝑦 ) ∧ 𝑔 : dom ( iEdg ‘ 𝑥 ) –1-1-onto→ dom ( iEdg ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑥 ) ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔𝑖 ) ) ) } )