let X, Y be non empty set ; for S being diff-finite-partition-closed Subset-Family of X
for f being Function of X,Y st f is one-to-one holds
f .: S is diff-finite-partition-closed Subset-Family of Y
let S be diff-finite-partition-closed Subset-Family of X; for f being Function of X,Y st f is one-to-one holds
f .: S is diff-finite-partition-closed Subset-Family of Y
let f be Function of X,Y; ( f is one-to-one implies f .: S is diff-finite-partition-closed Subset-Family of Y )
assume A1:
f is one-to-one
; f .: S is diff-finite-partition-closed Subset-Family of Y
per cases
( f .: S is empty or not f .: S is empty )
;
suppose A2:
not
f .: S is
empty
;
f .: S is diff-finite-partition-closed Subset-Family of Yreconsider fS =
f .: S as
Subset-Family of
Y ;
now for s1, s2 being Element of fS st not s1 \ s2 is empty holds
ex x being finite Subset of fS st x is a_partition of s1 \ s2let s1,
s2 be
Element of
fS;
( not s1 \ s2 is empty implies ex x being finite Subset of fS st x is a_partition of s1 \ s2 )assume A3:
not
s1 \ s2 is
empty
;
ex x being finite Subset of fS st x is a_partition of s1 \ s2A4:
s1 in fS
by A2;
consider c1 being
Subset of
X such that A5:
c1 in S
and A6:
s1 = f .: c1
by A4, FUNCT_2:def 10;
A7:
s2 in fS
by A2;
consider c2 being
Subset of
X such that A8:
c2 in S
and A9:
s2 = f .: c2
by A7, FUNCT_2:def 10;
A10:
f .: (c1 \ c2) = s1 \ s2
by A1, A6, A9, FUNCT_1:64;
then A11:
not
c1 \ c2 is
empty
by A3;
consider x1 being
finite Subset of
S such that A12:
x1 is
a_partition of
c1 \ c2
by A5, A8, A11, SRINGS_1:def 2;
(
x1 c= S &
S c= bool X )
;
then
x1 c= bool X
;
then reconsider x2 =
x1 as
Subset-Family of
X ;
now ( f .: x2 is finite Subset of fS & f .: x2 is a_partition of s1 \ s2 )thus
f .: x2 is
finite Subset of
fS
by FUNCT_2:103;
f .: x2 is a_partition of s1 \ s2thus
f .: x2 is
a_partition of
s1 \ s2
verumproof
now ( f .: x2 is Subset-Family of (s1 \ s2) & union (f .: x2) = s1 \ s2 & ( for A being Subset of (s1 \ s2) st A in f .: x2 holds
( A <> {} & ( for B being Subset of (s1 \ s2) holds
( not B in f .: x2 or A = B or A misses B ) ) ) ) )
f .: x2 c= bool (s1 \ s2)
hence
f .: x2 is
Subset-Family of
(s1 \ s2)
;
( union (f .: x2) = s1 \ s2 & ( for A being Subset of (s1 \ s2) st A in f .: x2 holds
( A <> {} & ( for B being Subset of (s1 \ s2) holds
( not B in f .: x2 or A = B or A misses B ) ) ) ) )now ( ( for t being object st t in union (f .: x2) holds
t in s1 \ s2 ) & ( for t being object st t in s1 \ s2 holds
t in union (f .: x2) ) )let t be
object ;
( t in s1 \ s2 implies t in union (f .: x2) )assume
t in s1 \ s2
;
t in union (f .: x2)then
t in f .: (c1 \ c2)
by A1, A6, A9, FUNCT_1:64;
then consider v being
object such that A19:
v in dom f
and A20:
v in c1 \ c2
and A21:
t = f . v
by FUNCT_1:def 6;
v in union x1
by A12, A20, EQREL_1:def 4;
then consider u being
set such that A22:
v in u
and A23:
u in x1
by TARSKI:def 4;
reconsider fu =
f .: u as
Subset of
Y ;
(
f . v in f .: u &
f .: u in f .: x2 )
by A19, A22, FUNCT_1:def 6, A23, FUNCT_2:def 10;
hence
t in union (f .: x2)
by A21, TARSKI:def 4;
verum end; hence
union (f .: x2) = s1 \ s2
by TARSKI:def 3;
for A being Subset of (s1 \ s2) st A in f .: x2 holds
( A <> {} & ( for B being Subset of (s1 \ s2) holds
( not B in f .: x2 or A = B or A misses B ) ) )hence
for
A being
Subset of
(s1 \ s2) st
A in f .: x2 holds
(
A <> {} & ( for
B being
Subset of
(s1 \ s2) holds
( not
B in f .: x2 or
A = B or
A misses B ) ) )
;
verum end;
hence
f .: x2 is
a_partition of
s1 \ s2
by EQREL_1:def 4;
verum
end; end; hence
ex
x being
finite Subset of
fS st
x is
a_partition of
s1 \ s2
;
verum end; then
fS is
diff-finite-partition-closed
;
hence
f .: S is
diff-finite-partition-closed Subset-Family of
Y
;
verum end; end;