Definition df-grisom

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 = ( x e. _V , y e. _V |-> { <. f , g >. | ( f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y ) /\ g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y ) /\ A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgrisom	|- GraphIsom
1		vx	|- x
2		cvv	|- _V
3		vy	|- y
4		vf	|- f
5		vg	|- g
6	4	cv	|- f
7		cvtx	|- Vtx
8	1	cv	|- x
9	8 7	cfv	|- ( Vtx ` x )
10	3	cv	|- y
11	10 7	cfv	|- ( Vtx ` y )
12	9 11 6	wf1o	|- f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y )
13	5	cv	|- g
14		ciedg	|- iEdg
15	8 14	cfv	|- ( iEdg ` x )
16	15	cdm	|- dom ( iEdg ` x )
17	10 14	cfv	|- ( iEdg ` y )
18	17	cdm	|- dom ( iEdg ` y )
19	16 18 13	wf1o	|- g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y )
20		vi	|- i
21	20	cv	|- i
22	21 15	cfv	|- ( ( iEdg ` x ) ` i )
23	6 22	cima	|- ( f " ( ( iEdg ` x ) ` i ) )
24	21 13	cfv	|- ( g ` i )
25	24 17	cfv	|- ( ( iEdg ` y ) ` ( g ` i ) )
26	23 25	wceq	|- ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) )
27	26 20 16	wral	|- A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) )
28	12 19 27	w3a	|- ( f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y ) /\ g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y ) /\ A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) ) )
29	28 4 5	copab	|- { <. f , g >. | ( f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y ) /\ g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y ) /\ A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) ) ) }
30	1 3 2 2 29	cmpo	|- ( x e. _V , y e. _V |-> { <. f , g >. | ( f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y ) /\ g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y ) /\ A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) ) ) } )
31	0 30	wceq	|- GraphIsom = ( x e. _V , y e. _V |-> { <. f , g >. | ( f : ( Vtx ` x ) -1-1-onto-> ( Vtx ` y ) /\ g : dom ( iEdg ` x ) -1-1-onto-> dom ( iEdg ` y ) /\ A. i e. dom ( iEdg ` x ) ( f " ( ( iEdg ` x ) ` i ) ) = ( ( iEdg ` y ) ` ( g ` i ) ) ) } )