let G2, H be _Graph; for F being PGraphMapping of G2,H st F is directed & F is weak_SG-embedding holds
ex G1 being Supergraph of G2 st G1 is H -Disomorphic
let F be PGraphMapping of G2,H; ( F is directed & F is weak_SG-embedding implies ex G1 being Supergraph of G2 st G1 is H -Disomorphic )
assume A1:
( F is directed & F is weak_SG-embedding )
; ex G1 being Supergraph of G2 st G1 is H -Disomorphic
then reconsider F = F as one-to-one PGraphMapping of G2,H ;
set c = (the_Vertices_of H) --> (the_Vertices_of G2);
set V = <:((the_Vertices_of H) --> (the_Vertices_of G2)),(id (the_Vertices_of H)):> +* ((F _V) ");
A2: dom <:((the_Vertices_of H) --> (the_Vertices_of G2)),(id (the_Vertices_of H)):> =
(dom ((the_Vertices_of H) --> (the_Vertices_of G2))) /\ (dom (id (the_Vertices_of H)))
by FUNCT_3:def 7
.=
(the_Vertices_of H) /\ (the_Vertices_of H)
;
dom ((F _V) ") = rng (F _V)
by FUNCT_1:33;
then A3:
dom ((F _V) ") c= the_Vertices_of H
;
A4: dom (<:((the_Vertices_of H) --> (the_Vertices_of G2)),(id (the_Vertices_of H)):> +* ((F _V) ")) =
(the_Vertices_of H) \/ (dom ((F _V) "))
by A2, FUNCT_4:def 1
.=
the_Vertices_of H
by A3, XBOOLE_1:12
;
then reconsider V = <:((the_Vertices_of H) --> (the_Vertices_of G2)),(id (the_Vertices_of H)):> +* ((F _V) ") as ManySortedSet of the_Vertices_of H by RELAT_1:def 18, PARTFUN1:def 2;
A5:
not V is empty
by A4;
A6:
(rng <:((the_Vertices_of H) --> (the_Vertices_of G2)),(id (the_Vertices_of H)):>) /\ (rng ((F _V) ")) = {}
proof
assume A7:
(rng <:((the_Vertices_of H) --> (the_Vertices_of G2)),(id (the_Vertices_of H)):>) /\ (rng ((F _V) ")) <> {}
;
contradiction
set y = the
Element of
(rng <:((the_Vertices_of H) --> (the_Vertices_of G2)),(id (the_Vertices_of H)):>) /\ (rng ((F _V) "));
reconsider Y = the
Element of
(rng <:((the_Vertices_of H) --> (the_Vertices_of G2)),(id (the_Vertices_of H)):>) /\ (rng ((F _V) ")) as
set ;
A8:
( the
Element of
(rng <:((the_Vertices_of H) --> (the_Vertices_of G2)),(id (the_Vertices_of H)):>) /\ (rng ((F _V) ")) in rng <:((the_Vertices_of H) --> (the_Vertices_of G2)),(id (the_Vertices_of H)):> & the
Element of
(rng <:((the_Vertices_of H) --> (the_Vertices_of G2)),(id (the_Vertices_of H)):>) /\ (rng ((F _V) ")) in rng ((F _V) ") )
by A7, XBOOLE_0:def 4;
then consider x being
object such that A9:
x in dom <:((the_Vertices_of H) --> (the_Vertices_of G2)),(id (the_Vertices_of H)):>
and A10:
<:((the_Vertices_of H) --> (the_Vertices_of G2)),(id (the_Vertices_of H)):> . x = the
Element of
(rng <:((the_Vertices_of H) --> (the_Vertices_of G2)),(id (the_Vertices_of H)):>) /\ (rng ((F _V) "))
by FUNCT_1:def 3;
A11: the
Element of
(rng <:((the_Vertices_of H) --> (the_Vertices_of G2)),(id (the_Vertices_of H)):>) /\ (rng ((F _V) ")) =
[(((the_Vertices_of H) --> (the_Vertices_of G2)) . x),((id (the_Vertices_of H)) . x)]
by A9, A10, FUNCT_3:def 7
.=
[(((the_Vertices_of H) --> (the_Vertices_of G2)) . x),x]
by A9, FUNCT_1:18
.=
[(the_Vertices_of G2),x]
by A9, FUNCOP_1:7
;
the
Element of
(rng <:((the_Vertices_of H) --> (the_Vertices_of G2)),(id (the_Vertices_of H)):>) /\ (rng ((F _V) ")) in dom (F _V)
by A8, FUNCT_1:33;
then A12:
the
Element of
(rng <:((the_Vertices_of H) --> (the_Vertices_of G2)),(id (the_Vertices_of H)):>) /\ (rng ((F _V) ")) in the_Vertices_of G2
;
A13:
the_Vertices_of G2 in {(the_Vertices_of G2)}
by TARSKI:def 1;
{(the_Vertices_of G2)} in {{(the_Vertices_of G2),x},{(the_Vertices_of G2)}}
by TARSKI:def 2;
then
{(the_Vertices_of G2)} in Y
by A11, TARSKI:def 5;
hence
contradiction
by A12, A13, XREGULAR:7;
verum
end;
reconsider V = V as non empty one-to-one ManySortedSet of the_Vertices_of H by A5, A6, FUNCT_4:92, XBOOLE_0:def 7;
set d = (the_Edges_of H) --> (the_Edges_of G2);
set E = <:((the_Edges_of H) --> (the_Edges_of G2)),(id (the_Edges_of H)):> +* ((F _E) ");
A14: dom <:((the_Edges_of H) --> (the_Edges_of G2)),(id (the_Edges_of H)):> =
(dom ((the_Edges_of H) --> (the_Edges_of G2))) /\ (dom (id (the_Edges_of H)))
by FUNCT_3:def 7
.=
(the_Edges_of H) /\ (the_Edges_of H)
;
dom ((F _E) ") = rng (F _E)
by FUNCT_1:33;
then A15:
dom ((F _E) ") c= the_Edges_of H
;
dom (<:((the_Edges_of H) --> (the_Edges_of G2)),(id (the_Edges_of H)):> +* ((F _E) ")) =
(the_Edges_of H) \/ (dom ((F _E) "))
by A14, FUNCT_4:def 1
.=
the_Edges_of H
by A15, XBOOLE_1:12
;
then reconsider E = <:((the_Edges_of H) --> (the_Edges_of G2)),(id (the_Edges_of H)):> +* ((F _E) ") as ManySortedSet of the_Edges_of H by RELAT_1:def 18, PARTFUN1:def 2;
A16:
(rng <:((the_Edges_of H) --> (the_Edges_of G2)),(id (the_Edges_of H)):>) /\ (rng ((F _E) ")) = {}
proof
assume A17:
(rng <:((the_Edges_of H) --> (the_Edges_of G2)),(id (the_Edges_of H)):>) /\ (rng ((F _E) ")) <> {}
;
contradiction
set y = the
Element of
(rng <:((the_Edges_of H) --> (the_Edges_of G2)),(id (the_Edges_of H)):>) /\ (rng ((F _E) "));
reconsider Y = the
Element of
(rng <:((the_Edges_of H) --> (the_Edges_of G2)),(id (the_Edges_of H)):>) /\ (rng ((F _E) ")) as
set ;
A18:
( the
Element of
(rng <:((the_Edges_of H) --> (the_Edges_of G2)),(id (the_Edges_of H)):>) /\ (rng ((F _E) ")) in rng <:((the_Edges_of H) --> (the_Edges_of G2)),(id (the_Edges_of H)):> & the
Element of
(rng <:((the_Edges_of H) --> (the_Edges_of G2)),(id (the_Edges_of H)):>) /\ (rng ((F _E) ")) in rng ((F _E) ") )
by A17, XBOOLE_0:def 4;
then consider x being
object such that A19:
x in dom <:((the_Edges_of H) --> (the_Edges_of G2)),(id (the_Edges_of H)):>
and A20:
<:((the_Edges_of H) --> (the_Edges_of G2)),(id (the_Edges_of H)):> . x = the
Element of
(rng <:((the_Edges_of H) --> (the_Edges_of G2)),(id (the_Edges_of H)):>) /\ (rng ((F _E) "))
by FUNCT_1:def 3;
A21:
x in the_Edges_of H
by A14, A19;
A22: the
Element of
(rng <:((the_Edges_of H) --> (the_Edges_of G2)),(id (the_Edges_of H)):>) /\ (rng ((F _E) ")) =
[(((the_Edges_of H) --> (the_Edges_of G2)) . x),((id (the_Edges_of H)) . x)]
by A19, A20, FUNCT_3:def 7
.=
[(((the_Edges_of H) --> (the_Edges_of G2)) . x),x]
by A21, FUNCT_1:18
.=
[(the_Edges_of G2),x]
by A21, FUNCOP_1:7
;
A23:
the
Element of
(rng <:((the_Edges_of H) --> (the_Edges_of G2)),(id (the_Edges_of H)):>) /\ (rng ((F _E) ")) in dom (F _E)
by A18, FUNCT_1:33;
A24:
the_Edges_of G2 in {(the_Edges_of G2)}
by TARSKI:def 1;
{(the_Edges_of G2)} in {{(the_Edges_of G2),x},{(the_Edges_of G2)}}
by TARSKI:def 2;
then
{(the_Edges_of G2)} in Y
by A22, TARSKI:def 5;
hence
contradiction
by A23, A24, XREGULAR:7;
verum
end;
reconsider E = E as one-to-one ManySortedSet of the_Edges_of H by A16, FUNCT_4:92, XBOOLE_0:def 7;
set G1 = replaceVerticesEdges (V,E);
now ( the_Vertices_of G2 c= the_Vertices_of (replaceVerticesEdges (V,E)) & the_Edges_of G2 c= the_Edges_of (replaceVerticesEdges (V,E)) & ( for e being set st e in the_Edges_of G2 holds
( (the_Source_of G2) . e = (the_Source_of (replaceVerticesEdges (V,E))) . e & (the_Target_of G2) . e = (the_Target_of (replaceVerticesEdges (V,E))) . e ) ) ) the_Vertices_of G2 =
dom (F _V)
by A1, GLIB_010:def 11
.=
rng ((F _V) ")
by FUNCT_1:33
;
then
the_Vertices_of G2 c= rng V
by FUNCT_4:18;
hence
the_Vertices_of G2 c= the_Vertices_of (replaceVerticesEdges (V,E))
by Th1;
( the_Edges_of G2 c= the_Edges_of (replaceVerticesEdges (V,E)) & ( for e being set st e in the_Edges_of G2 holds
( (the_Source_of G2) . e = (the_Source_of (replaceVerticesEdges (V,E))) . e & (the_Target_of G2) . e = (the_Target_of (replaceVerticesEdges (V,E))) . e ) ) ) the_Edges_of G2 =
dom (F _E)
by A1, GLIB_010:def 11
.=
rng ((F _E) ")
by FUNCT_1:33
;
then
the_Edges_of G2 c= rng E
by FUNCT_4:18;
hence
the_Edges_of G2 c= the_Edges_of (replaceVerticesEdges (V,E))
by Th1;
for e being set st e in the_Edges_of G2 holds
( (the_Source_of G2) . e = (the_Source_of (replaceVerticesEdges (V,E))) . e & (the_Target_of G2) . e = (the_Target_of (replaceVerticesEdges (V,E))) . e )let e be
set ;
( e in the_Edges_of G2 implies ( (the_Source_of G2) . e = (the_Source_of (replaceVerticesEdges (V,E))) . e & (the_Target_of G2) . e = (the_Target_of (replaceVerticesEdges (V,E))) . e ) )assume A25:
e in the_Edges_of G2
;
( (the_Source_of G2) . e = (the_Source_of (replaceVerticesEdges (V,E))) . e & (the_Target_of G2) . e = (the_Target_of (replaceVerticesEdges (V,E))) . e )then A26:
e in dom (the_Source_of G2)
by FUNCT_2:def 1;
A27:
e in dom (the_Target_of G2)
by A25, FUNCT_2:def 1;
A28:
e in dom (F _E)
by A1, A25, GLIB_010:def 11;
then A29:
e in rng ((F _E) ")
by FUNCT_1:33;
then
e in rng E
by TARSKI:def 3, FUNCT_4:18;
then A30:
e in dom (E ")
by FUNCT_1:33;
A31:
dom (F _V) = dom (id (rng ((F _V) ")))
by FUNCT_1:33;
A32:
(the_Source_of G2) . e in dom (id (rng ((F _V) ")))
by A28, A31, GLIB_010:5;
A33:
(the_Target_of G2) . e in dom (id (rng ((F _V) ")))
by A28, A31, GLIB_010:5;
thus (the_Source_of G2) . e =
(id (rng ((F _V) "))) . ((the_Source_of G2) . e)
by A32, FUNCT_1:18
.=
(V * (((F _V) ") ")) . ((the_Source_of G2) . e)
by GLIBPRE1:9
.=
((V * (((F _V) ") ")) * (the_Source_of G2)) . e
by A26, FUNCT_1:13
.=
((V * (F _V)) * (the_Source_of G2)) . e
by FUNCT_1:43
.=
(V * ((F _V) * ((the_Source_of G2) | (the_Edges_of G2)))) . e
by RELAT_1:36
.=
(V * ((F _V) * ((the_Source_of G2) | (dom (F _E))))) . e
by A1, GLIB_010:def 11
.=
(V * ((the_Source_of H) * (F _E))) . e
by A1, GLIB_010:14
.=
((V * (the_Source_of H)) * (F _E)) . e
by RELAT_1:36
.=
(V * (the_Source_of H)) . ((F _E) . e)
by A28, FUNCT_1:13
.=
(V * (the_Source_of H)) . ((((F _E) ") ") . e)
by FUNCT_1:43
.=
(V * (the_Source_of H)) . (((E ") | (rng ((F _E) "))) . e)
by GLIBPRE1:7
.=
(V * (the_Source_of H)) . ((E ") . e)
by A29, FUNCT_1:49
.=
((V * (the_Source_of H)) * (E ")) . e
by A30, FUNCT_1:13
.=
(the_Source_of (replaceVerticesEdges (V,E))) . e
by Th1
;
(the_Target_of G2) . e = (the_Target_of (replaceVerticesEdges (V,E))) . ethus (the_Target_of G2) . e =
(id (rng ((F _V) "))) . ((the_Target_of G2) . e)
by A33, FUNCT_1:18
.=
(V * (((F _V) ") ")) . ((the_Target_of G2) . e)
by GLIBPRE1:9
.=
((V * (((F _V) ") ")) * (the_Target_of G2)) . e
by A27, FUNCT_1:13
.=
((V * (F _V)) * (the_Target_of G2)) . e
by FUNCT_1:43
.=
(V * ((F _V) * ((the_Target_of G2) | (the_Edges_of G2)))) . e
by RELAT_1:36
.=
(V * ((F _V) * ((the_Target_of G2) | (dom (F _E))))) . e
by A1, GLIB_010:def 11
.=
(V * ((the_Target_of H) * (F _E))) . e
by A1, GLIB_010:14
.=
((V * (the_Target_of H)) * (F _E)) . e
by RELAT_1:36
.=
(V * (the_Target_of H)) . ((F _E) . e)
by A28, FUNCT_1:13
.=
(V * (the_Target_of H)) . ((((F _E) ") ") . e)
by FUNCT_1:43
.=
(V * (the_Target_of H)) . (((E ") | (rng ((F _E) "))) . e)
by GLIBPRE1:7
.=
(V * (the_Target_of H)) . ((E ") . e)
by A29, FUNCT_1:49
.=
((V * (the_Target_of H)) * (E ")) . e
by A30, FUNCT_1:13
.=
(the_Target_of (replaceVerticesEdges (V,E))) . e
by Th1
;
verum end;
then reconsider G1 = replaceVerticesEdges (V,E) as Supergraph of G2 by GLIB_006:def 9;
take
G1
; G1 is H -Disomorphic
thus
G1 is H -Disomorphic
by Th17; verum