let S be Graph-membered set ; :: thesis: ( card (the_Vertices_of S) c= card S & card (the_Edges_of S) c= card S & card (the_Source_of S) c= card S & card (the_Target_of S) c= card S )
defpred S1[ object , object ] means ex G being _Graph st
( $1 = G & $2 = the_Vertices_of G );
A1: for x, y1, y2 being object st x in S & S1[x,y1] & S1[x,y2] holds
y1 = y2 ;
A2: for x being object st x in S holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in S implies ex y being object st S1[x,y] )
assume x in S ; :: thesis: ex y being object st S1[x,y]
then reconsider G = x as _Graph ;
take the_Vertices_of G ; :: thesis: S1[x, the_Vertices_of G]
take G ; :: thesis: ( x = G & the_Vertices_of G = the_Vertices_of G )
thus ( x = G & the_Vertices_of G = the_Vertices_of G ) ; :: thesis: verum
end;
consider f1 being Function such that
A3: ( dom f1 = S & ( for x being object st x in S holds
S1[x,f1 . x] ) ) from FUNCT_1:sch 2(A1, A2);
now :: thesis: for x being object st x in the_Vertices_of S holds
x in rng f1
let x be object ; :: thesis: ( x in the_Vertices_of S implies x in rng f1 )
assume x in the_Vertices_of S ; :: thesis: x in rng f1
then consider G being _Graph such that
A4: ( G in S & x = the_Vertices_of G ) by Def14;
consider G0 being _Graph such that
A5: ( G = G0 & f1 . G = the_Vertices_of G0 ) by A3, A4;
thus x in rng f1 by A3, A4, A5, FUNCT_1:3; :: thesis: verum
end;
hence card (the_Vertices_of S) c= card S by A3, CARD_1:12, TARSKI:def 3; :: thesis: ( card (the_Edges_of S) c= card S & card (the_Source_of S) c= card S & card (the_Target_of S) c= card S )
defpred S2[ object , object ] means ex G being _Graph st
( $1 = G & $2 = the_Edges_of G );
A6: for x, y1, y2 being object st x in S & S2[x,y1] & S2[x,y2] holds
y1 = y2 ;
A7: for x being object st x in S holds
ex y being object st S2[x,y]
proof
let x be object ; :: thesis: ( x in S implies ex y being object st S2[x,y] )
assume x in S ; :: thesis: ex y being object st S2[x,y]
then reconsider G = x as _Graph ;
take the_Edges_of G ; :: thesis: S2[x, the_Edges_of G]
take G ; :: thesis: ( x = G & the_Edges_of G = the_Edges_of G )
thus ( x = G & the_Edges_of G = the_Edges_of G ) ; :: thesis: verum
end;
consider f2 being Function such that
A8: ( dom f2 = S & ( for x being object st x in S holds
S2[x,f2 . x] ) ) from FUNCT_1:sch 2(A6, A7);
now :: thesis: for x being object st x in the_Edges_of S holds
x in rng f2
let x be object ; :: thesis: ( x in the_Edges_of S implies x in rng f2 )
assume x in the_Edges_of S ; :: thesis: x in rng f2
then consider G being _Graph such that
A9: ( G in S & x = the_Edges_of G ) by Def15;
consider G0 being _Graph such that
A10: ( G = G0 & f2 . G = the_Edges_of G0 ) by A8, A9;
thus x in rng f2 by A8, A9, A10, FUNCT_1:3; :: thesis: verum
end;
hence card (the_Edges_of S) c= card S by A8, CARD_1:12, TARSKI:def 3; :: thesis: ( card (the_Source_of S) c= card S & card (the_Target_of S) c= card S )
defpred S3[ object , object ] means ex G being _Graph st
( $1 = G & $2 = the_Source_of G );
A11: for x, y1, y2 being object st x in S & S3[x,y1] & S3[x,y2] holds
y1 = y2 ;
A12: for x being object st x in S holds
ex y being object st S3[x,y]
proof
let x be object ; :: thesis: ( x in S implies ex y being object st S3[x,y] )
assume x in S ; :: thesis: ex y being object st S3[x,y]
then reconsider G = x as _Graph ;
take the_Source_of G ; :: thesis: S3[x, the_Source_of G]
take G ; :: thesis: ( x = G & the_Source_of G = the_Source_of G )
thus ( x = G & the_Source_of G = the_Source_of G ) ; :: thesis: verum
end;
consider f3 being Function such that
A13: ( dom f3 = S & ( for x being object st x in S holds
S3[x,f3 . x] ) ) from FUNCT_1:sch 2(A11, A12);
now :: thesis: for x being object st x in the_Source_of S holds
x in rng f3
let x be object ; :: thesis: ( x in the_Source_of S implies x in rng f3 )
assume x in the_Source_of S ; :: thesis: x in rng f3
then consider G being _Graph such that
A14: ( G in S & x = the_Source_of G ) by Def16;
consider G0 being _Graph such that
A15: ( G = G0 & f3 . G = the_Source_of G0 ) by A13, A14;
thus x in rng f3 by A13, A14, A15, FUNCT_1:3; :: thesis: verum
end;
hence card (the_Source_of S) c= card S by A13, CARD_1:12, TARSKI:def 3; :: thesis: card (the_Target_of S) c= card S
defpred S4[ object , object ] means ex G being _Graph st
( $1 = G & $2 = the_Target_of G );
A16: for x, y1, y2 being object st x in S & S4[x,y1] & S4[x,y2] holds
y1 = y2 ;
A17: for x being object st x in S holds
ex y being object st S4[x,y]
proof
let x be object ; :: thesis: ( x in S implies ex y being object st S4[x,y] )
assume x in S ; :: thesis: ex y being object st S4[x,y]
then reconsider G = x as _Graph ;
take the_Target_of G ; :: thesis: S4[x, the_Target_of G]
take G ; :: thesis: ( x = G & the_Target_of G = the_Target_of G )
thus ( x = G & the_Target_of G = the_Target_of G ) ; :: thesis: verum
end;
consider f4 being Function such that
A18: ( dom f4 = S & ( for x being object st x in S holds
S4[x,f4 . x] ) ) from FUNCT_1:sch 2(A16, A17);
now :: thesis: for x being object st x in the_Target_of S holds
x in rng f4
let x be object ; :: thesis: ( x in the_Target_of S implies x in rng f4 )
assume x in the_Target_of S ; :: thesis: x in rng f4
then consider G being _Graph such that
A19: ( G in S & x = the_Target_of G ) by Def17;
consider G0 being _Graph such that
A20: ( G = G0 & f4 . G = the_Target_of G0 ) by A18, A19;
thus x in rng f4 by A18, A19, A20, FUNCT_1:3; :: thesis: verum
end;
hence card (the_Target_of S) c= card S by A18, CARD_1:12, TARSKI:def 3; :: thesis: verum