let X, Y be non empty set ; :: thesis: for S being diff-c=-finite-partition-closed Subset-Family of X
for f being Function of X,Y st f is one-to-one & not f .: S is empty holds
f .: S is diff-c=-finite-partition-closed Subset-Family of Y
let S be diff-c=-finite-partition-closed Subset-Family of X; :: thesis: for f being Function of X,Y st f is one-to-one & not f .: S is empty holds
f .: S is diff-c=-finite-partition-closed Subset-Family of Y
let f be Function of X,Y; :: thesis: ( f is one-to-one & not f .: S is empty implies f .: S is diff-c=-finite-partition-closed Subset-Family of Y )
assume that
A1: f is one-to-one and
A2: not f .: S is empty ; :: thesis: f .: S is diff-c=-finite-partition-closed Subset-Family of Y
reconsider fS = f .: S as Subset-Family of Y ;
fS is diff-c=-finite-partition-closed
proof
let s1, s2 be Element of fS; :: according to SRINGS_1:def 3 :: thesis: ( not s2 c= s1 or ex b1 being Element of bool fS st b1 is a_partition of s1 \ s2 )
assume A3: s2 c= s1 ; :: thesis: ex b1 being Element of bool fS st b1 is a_partition of s1 \ s2
s1 in fS by A2;
then consider c1 being Subset of X such that
A4: c1 in S and
A5: s1 = f .: c1 by FUNCT_2:def 10;
s2 in fS by A2;
then consider c2 being Subset of X such that
A6: c2 in S and
A7: s2 = f .: c2 by FUNCT_2:def 10;
A8: f .: (c1 \ c2) = s1 \ s2 by A1, A5, A7, FUNCT_1:64;
dom f = X by PARTFUN1:def 2;
then consider y1 being finite Subset of S such that
A9: y1 is a_partition of c1 \ c2 by A3, A5, A7, A1, FUNCT_1:87, A4, A6, SRINGS_1:def 3;
( y1 c= S & S c= bool X ) ;
then y1 c= bool X ;
then reconsider y2 = y1 as Subset-Family of X ;
thus ex x being finite Subset of fS st x is a_partition of s1 \ s2 :: thesis: verum
proof
reconsider fy = f .: y2 as finite Subset of fS by FUNCT_2:103;
take fy ; :: thesis: fy is a_partition of s1 \ s2
now :: thesis: ( f .: y2 is Subset-Family of (s1 \ s2) & union (f .: y2) = s1 \ s2 & ( for A being Subset of (s1 \ s2) st A in f .: y2 holds
( A <> {} & ( for B being Subset of (s1 \ s2) holds
( not B in f .: y2 or A = B or A misses B ) ) ) ) )
f .: y2 c= bool (s1 \ s2)
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in f .: y2 or t in bool (s1 \ s2) )
assume t in f .: y2 ; :: thesis: t in bool (s1 \ s2)
then consider z1 being Subset of X such that
A10: z1 in y2 and
A11: t = f .: z1 by FUNCT_2:def 10;
reconsider t1 = t as set by A11;
f .: z1 c= f .: (c1 \ c2) by A9, A10, RELAT_1:123;
hence t in bool (s1 \ s2) by A11, A8; :: thesis: verum
end;
hence f .: y2 is Subset-Family of (s1 \ s2) ; :: thesis: ( union (f .: y2) = s1 \ s2 & ( for A being Subset of (s1 \ s2) st A in f .: y2 holds
( A <> {} & ( for B being Subset of (s1 \ s2) holds
( not B in f .: y2 or A = B or A misses B ) ) ) ) )
now :: thesis: ( ( for t being object st t in union (f .: y2) holds
t in s1 \ s2 ) & ( for t being object st t in s1 \ s2 holds
t in union (f .: y2) ) )
hereby :: thesis: for t being object st t in s1 \ s2 holds
t in union (f .: y2)
let t be object ; :: thesis: ( t in union (f .: y2) implies t in s1 \ s2 )
assume t in union (f .: y2) ; :: thesis: t in s1 \ s2
then consider u being set such that
A12: t in u and
A13: u in f .: y2 by TARSKI:def 4;
consider v being Subset of X such that
A14: v in y2 and
A15: u = f .: v by A13, FUNCT_2:def 10;
f .: v c= f .: (c1 \ c2) by A14, A9, RELAT_1:123;
hence t in s1 \ s2 by A12, A15, A8; :: thesis: verum
end;
let t be object ; :: thesis: ( t in s1 \ s2 implies t in union (f .: y2) )
assume t in s1 \ s2 ; :: thesis: t in union (f .: y2)
then t in f .: (c1 \ c2) by A1, A5, A7, FUNCT_1:64;
then consider v being object such that
A16: v in dom f and
A17: v in c1 \ c2 and
A18: t = f . v by FUNCT_1:def 6;
v in union y1 by A9, A17, EQREL_1:def 4;
then consider u being set such that
A19: v in u and
A20: u in y1 by TARSKI:def 4;
reconsider fu = f .: u as Subset of Y ;
( f . v in f .: u & f .: u in f .: y2 ) by A16, A19, FUNCT_1:def 6, A20, FUNCT_2:def 10;
hence t in union (f .: y2) by A18, TARSKI:def 4; :: thesis: verum
end;
hence union (f .: y2) = s1 \ s2 by TARSKI:def 3; :: thesis: for A being Subset of (s1 \ s2) st A in f .: y2 holds
( A <> {} & ( for B being Subset of (s1 \ s2) holds
( not B in f .: y2 or A = B or A misses B ) ) )
thus for A being Subset of (s1 \ s2) st A in f .: y2 holds
( A <> {} & ( for B being Subset of (s1 \ s2) holds
( not B in f .: y2 or A = B or A misses B ) ) ) :: thesis: verum
proof
let A be Subset of (s1 \ s2); :: thesis: ( A in f .: y2 implies ( A <> {} & ( for B being Subset of (s1 \ s2) holds
( not B in f .: y2 or A = B or A misses B ) ) ) )
assume A in f .: y2 ; :: thesis: ( A <> {} & ( for B being Subset of (s1 \ s2) holds
( not B in f .: y2 or A = B or A misses B ) ) )
then consider a0 being Subset of X such that
A23: a0 in y2 and
A24: A = f .: a0 by FUNCT_2:def 10;
thus A <> {} :: thesis: for B being Subset of (s1 \ s2) holds
( not B in f .: y2 or A = B or A misses B )
proof
assume A25: A = {} ; :: thesis: contradiction
dom f = X by PARTFUN1:def 2;
hence contradiction by A23, A9, A25, A24; :: thesis: verum
end;
let B be Subset of (s1 \ s2); :: thesis: ( not B in f .: y2 or A = B or A misses B )
assume B in f .: y2 ; :: thesis: ( A = B or A misses B )
then consider b0 being Subset of X such that
A26: b0 in y2 and
A27: B = f .: b0 by FUNCT_2:def 10;
thus ( A = B or A misses B ) by A23, A24, A26, A27, A1, A9, EQREL_1:def 4, FUNCT_1:66; :: thesis: verum
end;
end;
hence fy is a_partition of s1 \ s2 by EQREL_1:def 4; :: thesis: verum
end;
end;
hence f .: S is diff-c=-finite-partition-closed Subset-Family of Y ; :: thesis: verum