Metamath Proof Explorer

Definition df-isomgr

Description: Define the isomorphy relation for graphs. (Contributed by AV, 11-Nov-2022)

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

Detailed syntax breakdown

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