let G be non-Dmulti _Graph; :: thesis: ex F being PGraphMapping of G, createGraph ((the_Vertices_of G),(VertexDomRel G)) st
( F is Disomorphism & F _V = id (the_Vertices_of G) & ( for e being object st e in the_Edges_of G holds
(F _E) . e = [((the_Source_of G) . e),((the_Target_of G) . e)] ) )
set G9 = createGraph ((the_Vertices_of G),(VertexDomRel G));
reconsider f = id (the_Vertices_of G) as PartFunc of (the_Vertices_of G),(the_Vertices_of (createGraph ((the_Vertices_of G),(VertexDomRel G)))) ;
deffunc H1( object ) -> object = [((the_Source_of G) . $1),((the_Target_of G) . $1)];
consider g being Function such that
A1: dom g = the_Edges_of G and
A2: for x being object st x in the_Edges_of G holds
g . x = H1(x) from FUNCT_1:sch 3();
now :: thesis: for y being object holds
( ( y in rng g implies y in the_Edges_of (createGraph ((the_Vertices_of G),(VertexDomRel G))) ) & ( y in the_Edges_of (createGraph ((the_Vertices_of G),(VertexDomRel G))) implies y in rng g ) )
let y be object ; :: thesis: ( ( y in rng g implies y in the_Edges_of (createGraph ((the_Vertices_of G),(VertexDomRel G))) ) & ( y in the_Edges_of (createGraph ((the_Vertices_of G),(VertexDomRel G))) implies y in rng g ) )
hereby :: thesis: ( y in the_Edges_of (createGraph ((the_Vertices_of G),(VertexDomRel G))) implies y in rng g )
assume y in rng g ; :: thesis: y in the_Edges_of (createGraph ((the_Vertices_of G),(VertexDomRel G)))
then consider x being object such that
A3: ( x in dom g & g . x = y ) by FUNCT_1:def 3;
A4: y = [((the_Source_of G) . x),((the_Target_of G) . x)] by A1, A2, A3;
x DJoins (the_Source_of G) . x,(the_Target_of G) . x,G by A1, A3, GLIB_000:def 14;
then y in VertexDomRel G by A4, Th1;
hence y in the_Edges_of (createGraph ((the_Vertices_of G),(VertexDomRel G))) ; :: thesis: verum
end;
assume y in the_Edges_of (createGraph ((the_Vertices_of G),(VertexDomRel G))) ; :: thesis: y in rng g
then A5: y in VertexDomRel G ;
then consider v, w being object such that
A6: y = [v,w] by RELAT_1:def 1;
consider e being object such that
A7: e DJoins v,w,G by A5, A6, Th1;
A8: ( e in the_Edges_of G & (the_Source_of G) . e = v & (the_Target_of G) . e = w ) by A7, GLIB_000:def 14;
then g . e = y by A2, A6;
hence y in rng g by A1, A8, FUNCT_1:3; :: thesis: verum
end;
then A9: rng g = the_Edges_of (createGraph ((the_Vertices_of G),(VertexDomRel G))) by TARSKI:2;
then reconsider g = g as PartFunc of (the_Edges_of G),(the_Edges_of (createGraph ((the_Vertices_of G),(VertexDomRel G)))) by A1, RELSET_1:4;
now :: thesis: ( ( for e being object st e in dom g holds
( (the_Source_of G) . e in dom f & (the_Target_of G) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e DJoins v,w,G holds
g . e DJoins f . v,f . w, createGraph ((the_Vertices_of G),(VertexDomRel G)) ) )
thus for e being object st e in dom g holds
( (the_Source_of G) . e in dom f & (the_Target_of G) . e in dom f ) by FUNCT_2:5; :: thesis: for e, v, w being object st e in dom g & v in dom f & w in dom f & e DJoins v,w,G holds
g . e DJoins f . v,f . w, createGraph ((the_Vertices_of G),(VertexDomRel G))
let e, v, w be object ; :: thesis: ( e in dom g & v in dom f & w in dom f & e DJoins v,w,G implies g . e DJoins f . v,f . w, createGraph ((the_Vertices_of G),(VertexDomRel G)) )
assume A10: ( e in dom g & v in dom f & w in dom f & e DJoins v,w,G ) ; :: thesis: g . e DJoins f . v,f . w, createGraph ((the_Vertices_of G),(VertexDomRel G))
then A11: ( (the_Source_of G) . e = v & (the_Target_of G) . e = w ) by GLIB_000:def 14;
A12: g . e = [v,w] by A2, A10, A11;
g . e in rng g by A10, FUNCT_1:3;
then g . e in the_Edges_of (createGraph ((the_Vertices_of G),(VertexDomRel G))) ;
then g . e in VertexDomRel G ;
then g . e DJoins v,w, createGraph ((the_Vertices_of G),(VertexDomRel G)) by A12, Th63;
then g . e DJoins f . v,w, createGraph ((the_Vertices_of G),(VertexDomRel G)) by A10, FUNCT_1:18;
hence g . e DJoins f . v,f . w, createGraph ((the_Vertices_of G),(VertexDomRel G)) by A10, FUNCT_1:18; :: thesis: verum
end;
then reconsider F = [f,g] as directed PGraphMapping of G, createGraph ((the_Vertices_of G),(VertexDomRel G)) by GLIB_010:30;
take F ; :: thesis: ( F is Disomorphism & F _V = id (the_Vertices_of G) & ( for e being object st e in the_Edges_of G holds
(F _E) . e = [((the_Source_of G) . e),((the_Target_of G) . e)] ) )
now :: thesis: for x1, x2 being object st x1 in dom g & x2 in dom g & g . x1 = g . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in dom g & x2 in dom g & g . x1 = g . x2 implies x1 = x2 )
assume A13: ( x1 in dom g & x2 in dom g & g . x1 = g . x2 ) ; :: thesis: x1 = x2
then ( g . x1 = [((the_Source_of G) . x1),((the_Target_of G) . x1)] & g . x2 = [((the_Source_of G) . x2),((the_Target_of G) . x2)] ) by A2;
then ( (the_Source_of G) . x1 = (the_Source_of G) . x2 & (the_Target_of G) . x1 = (the_Target_of G) . x2 ) by A13, XTUPLE_0:1;
then ( x1 DJoins (the_Source_of G) . x1,(the_Target_of G) . x1,G & x2 DJoins (the_Source_of G) . x1,(the_Target_of G) . x1,G ) by A13, GLIB_000:def 14;
hence x1 = x2 by GLIB_000:def 21; :: thesis: verum
end;
then A14: g is one-to-one by FUNCT_1:def 4;
( f is one-to-one & F _V = f & F _E = g ) ;
then A15: F is one-to-one by A14, GLIB_010:def 13;
A16: ( dom f = the_Vertices_of G & rng f = the_Vertices_of (createGraph ((the_Vertices_of G),(VertexDomRel G))) ) ;
( F _V = f & F _E = g ) ;
then A17: ( F is total & F is onto ) by A1, A9, A16, GLIB_010:def 11, GLIB_010:def 12;
thus F is Disomorphism by A15, A17; :: thesis: ( F _V = id (the_Vertices_of G) & ( for e being object st e in the_Edges_of G holds
(F _E) . e = [((the_Source_of G) . e),((the_Target_of G) . e)] ) )
thus F _V = id (the_Vertices_of G) ; :: thesis: for e being object st e in the_Edges_of G holds
(F _E) . e = [((the_Source_of G) . e),((the_Target_of G) . e)]
let e be object ; :: thesis: ( e in the_Edges_of G implies (F _E) . e = [((the_Source_of G) . e),((the_Target_of G) . e)] )
assume e in the_Edges_of G ; :: thesis: (F _E) . e = [((the_Source_of G) . e),((the_Target_of G) . e)]
hence (F _E) . e = [((the_Source_of G) . e),((the_Target_of G) . e)] by A2; :: thesis: verum