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

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

hence
f .: S is diff-c=-finite-partition-closed Subset-Family of Y
; :: thesis: verum
let s1, s2 be Element of fS; :: according to SRINGS_1:def 3 :: thesis: ( not s2 c= s1 or ex b_{1} being Element of bool fS st b_{1} is a_partition of s1 \ s2 )

assume A3: s2 c= s1 ; :: thesis: ex b_{1} being Element of bool fS st b_{1} 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

end;assume A3: s2 c= s1 ; :: thesis: ex b

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

end;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 ) ) ) ) )

hence
fy is a_partition of s1 \ s2
by EQREL_1:def 4; :: thesis: verum( 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)

( A <> {} & ( for B being Subset of (s1 \ s2) holds

( not B in f .: y2 or A = B or A misses B ) ) ) ) )

( 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

end;proof

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
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;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

( 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) ) )

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 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 s1 \ s2 implies t in union (f .: y2) )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;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

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

( 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 )

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;( 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

let B be Subset of (s1 \ s2); :: thesis: ( not B in f .: y2 or A = B or A misses B )
assume A25:
A = {}
; :: thesis: contradiction

dom f = X by PARTFUN1:def 2;

hence contradiction by A23, A9, A25, A24; :: thesis: verum

end;dom f = X by PARTFUN1:def 2;

hence contradiction by A23, A9, A25, A24; :: thesis: verum

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