Description: Define the class of all isomorphisms between two graphs. In contrast to ( F GraphIso H ) , which is a set of functions between the vertices, ( F GraphIsom H ) is a set of pairs of functions: a function between the vertices, and a function between the (indices of the) edges.
It is not clear if such a definition is useful. In the definition by Diestel p. 3, for example, the bijection between the vertices is called an isomorphism, as formalized in df-grim . (Contributed by AV, 11-Dec-2022) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-grisom | ⊢ GraphIsom = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 : ( Vtx ‘ 𝑥 ) –1-1-onto→ ( Vtx ‘ 𝑦 ) ∧ 𝑔 : dom ( iEdg ‘ 𝑥 ) –1-1-onto→ dom ( iEdg ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑥 ) ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cgrisom | ⊢ GraphIsom | |
| 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 | ⊢ GraphIsom = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 : ( Vtx ‘ 𝑥 ) –1-1-onto→ ( Vtx ‘ 𝑦 ) ∧ 𝑔 : dom ( iEdg ‘ 𝑥 ) –1-1-onto→ dom ( iEdg ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑥 ) ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) } ) |