Description: The identity relation restricted to the set of vertices of a graph is a graph isomorphism between the graph and itself. (Contributed by AV, 29-Apr-2025) (Prove shortened by AV, 5-May-2025.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | grimid | |- ( G e. UHGraph -> ( _I |` ( Vtx ` G ) ) e. ( G GraphIso G ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | |- ( G e. UHGraph -> G e. UHGraph ) |
|
| 2 | eqidd | |- ( G e. UHGraph -> ( Vtx ` G ) = ( Vtx ` G ) ) |
|
| 3 | eqidd | |- ( G e. UHGraph -> ( iEdg ` G ) = ( iEdg ` G ) ) |
|
| 4 | 1 1 2 3 | grimidvtxedg | |- ( G e. UHGraph -> ( _I |` ( Vtx ` G ) ) e. ( G GraphIso G ) ) |