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 ‘ 𝑦 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) } )