let C1, C2 be Coherence_Space; for X being Subset of [:C1,(union C2):] st ( for x being set st x in X holds
x `1 is finite ) & ( for a, b being Element of C1 st a \/ b in C1 holds
for y1, y2 being object st [a,y1] in X & [b,y2] in X holds
{y1,y2} in C2 ) & ( for a, b being Element of C1 st a \/ b in C1 holds
for y being object st [a,y] in X & [b,y] in X holds
a = b ) holds
ex f being U-stable Function of C1,C2 st
( X = Trace f & ( for a being Element of C1 holds f . a = X .: (Fin a) ) )
let X be Subset of [:C1,(union C2):]; ( ( for x being set st x in X holds
x `1 is finite ) & ( for a, b being Element of C1 st a \/ b in C1 holds
for y1, y2 being object st [a,y1] in X & [b,y2] in X holds
{y1,y2} in C2 ) & ( for a, b being Element of C1 st a \/ b in C1 holds
for y being object st [a,y] in X & [b,y] in X holds
a = b ) implies ex f being U-stable Function of C1,C2 st
( X = Trace f & ( for a being Element of C1 holds f . a = X .: (Fin a) ) ) )
assume that
A1:
for x being set st x in X holds
x `1 is finite
and
A2:
for a, b being Element of C1 st a \/ b in C1 holds
for y1, y2 being object st [a,y1] in X & [b,y2] in X holds
{y1,y2} in C2
and
A3:
for a, b being Element of C1 st a \/ b in C1 holds
for y being object st [a,y] in X & [b,y] in X holds
a = b
; ex f being U-stable Function of C1,C2 st
( X = Trace f & ( for a being Element of C1 holds f . a = X .: (Fin a) ) )
deffunc H1( set ) -> set = X .: (Fin $1);
consider f being Function such that
A4:
( dom f = C1 & ( for a being set st a in C1 holds
f . a = H1(a) ) )
from FUNCT_1:sch 5();
A5:
now for a, y being set st a in dom f & y in f . a holds
ex x being set st
( x is finite & x c= a & y in f . x & ( for c being set st c c= a & y in f . c holds
x c= c ) )let a,
y be
set ;
( a in dom f & y in f . a implies ex x being set st
( x is finite & x c= a & y in f . x & ( for c being set st c c= a & y in f . c holds
x c= c ) ) )assume that A6:
a in dom f
and A7:
y in f . a
;
ex x being set st
( x is finite & x c= a & y in f . x & ( for c being set st c c= a & y in f . c holds
x c= c ) )reconsider a9 =
a as
Element of
C1 by A4, A6;
y in X .: (Fin a)
by A4, A6, A7;
then consider x being
object such that A8:
[x,y] in X
and A9:
x in Fin a
by RELAT_1:def 13;
reconsider x =
x as
set by TARSKI:1;
x c= a
by A9, FINSUB_1:def 5;
then
x in C1
by A4, A6, CLASSES1:def 1;
then A10:
f . x = X .: (Fin x)
by A4;
take x =
x;
( x is finite & x c= a & y in f . x & ( for c being set st c c= a & y in f . c holds
x c= c ) )
x in Fin x
by A9, FINSUB_1:def 5;
hence
(
x is
finite &
x c= a &
y in f . x )
by A8, A9, A10, FINSUB_1:def 5, RELAT_1:def 13;
for c being set st c c= a & y in f . c holds
x c= clet c be
set ;
( c c= a & y in f . c implies x c= c )assume that A11:
c c= a
and A12:
y in f . c
;
x c= c
c c= a9
by A11;
then
c in dom f
by A4, CLASSES1:def 1;
then
y in X .: (Fin c)
by A4, A12;
then consider z being
object such that A13:
[z,y] in X
and A14:
z in Fin c
by RELAT_1:def 13;
A15:
Fin c c= Fin a
by A11, FINSUB_1:10;
then A16:
z in Fin a9
by A14;
reconsider z =
z as
set by TARSKI:1;
x \/ z in Fin a9
by A9, A14, A15, FINSUB_1:1;
then
x = z
by A3, A8, A9, A13, A16;
hence
x c= c
by A14, FINSUB_1:def 5;
verum end;
A17:
rng f c= C2
proof
let x be
object ;
TARSKI:def 3 ( not x in rng f or x in C2 )
reconsider xx =
x as
set by TARSKI:1;
assume
x in rng f
;
x in C2
then consider a being
object such that A18:
a in dom f
and A19:
x = f . a
by FUNCT_1:def 3;
reconsider a =
a as
Element of
C1 by A4, A18;
A20:
x = X .: (Fin a)
by A4, A19;
now for z, y being set st z in xx & y in xx holds
{z,y} in C2let z,
y be
set ;
( z in xx & y in xx implies {z,y} in C2 )assume
z in xx
;
( y in xx implies {z,y} in C2 )then consider z1 being
object such that A21:
[z1,z] in X
and A22:
z1 in Fin a
by A20, RELAT_1:def 13;
assume
y in xx
;
{z,y} in C2then consider y1 being
object such that A23:
[y1,y] in X
and A24:
y1 in Fin a
by A20, RELAT_1:def 13;
reconsider y1 =
y1,
z1 =
z1 as
set by TARSKI:1;
z1 \/ y1 in Fin a
by A22, A24, FINSUB_1:1;
hence
{z,y} in C2
by A2, A21, A22, A23, A24;
verum end;
hence
x in C2
by COH_SP:6;
verum
end;
f is c=-monotone
then reconsider f = f as U-stable Function of C1,C2 by A4, A17, A5, Th22, FUNCT_2:def 1, RELSET_1:4;
take
f
; ( X = Trace f & ( for a being Element of C1 holds f . a = X .: (Fin a) ) )
thus
X = Trace f
for a being Element of C1 holds f . a = X .: (Fin a)proof
let a,
b be
object ;
RELAT_1:def 2 ( ( not [a,b] in X or [a,b] in Trace f ) & ( not [a,b] in Trace f or [a,b] in X ) )
hereby ( not [a,b] in Trace f or [a,b] in X )
assume A28:
[a,b] in X
;
[a,b] in Trace f
[a,b] `1 = a
;
then reconsider a9 =
a as
finite Element of
C1 by A1, A28, ZFMISC_1:87;
a9 in Fin a9
by FINSUB_1:def 5;
then A29:
b in X .: (Fin a9)
by A28, RELAT_1:def 13;
A30:
now for c being set st c in dom f & c c= a9 & b in f . c holds
a9 = clet c be
set ;
( c in dom f & c c= a9 & b in f . c implies a9 = c )assume that A31:
c in dom f
and A32:
c c= a9
and A33:
b in f . c
;
a9 = creconsider c9 =
c as
Element of
C1 by A4, A31;
b in X .: (Fin c9)
by A4, A33;
then consider x being
object such that A34:
[x,b] in X
and A35:
x in Fin c9
by RELAT_1:def 13;
reconsider x =
x as
set by TARSKI:1;
A36:
x c= c
by A35, FINSUB_1:def 5;
then
x \/ a9 = a9
by A32, XBOOLE_1:1, XBOOLE_1:12;
then
x = a
by A3, A28, A34, A35;
hence
a9 = c
by A32, A36;
verum end;
f . a9 = X .: (Fin a9)
by A4;
hence
[a,b] in Trace f
by A4, A29, A30, Th31;
verum
end;
assume A37:
[a,b] in Trace f
;
[a,b] in X
reconsider a =
a,
b =
b as
set by TARSKI:1;
(
a in dom f &
b in f . a )
by Th31, A37;
then
b in X .: (Fin a)
by A4;
then consider x being
object such that A38:
[x,b] in X
and A39:
x in Fin a
by RELAT_1:def 13;
reconsider a =
a as
Element of
C1 by A4, A37, Th31;
x in Fin a
by A39;
then reconsider x =
x as
finite Element of
C1 ;
x in Fin x
by FINSUB_1:def 5;
then
b in X .: (Fin x)
by A38, RELAT_1:def 13;
then A40:
b in f . x
by A4;
x c= a
by A39, FINSUB_1:def 5;
hence
[a,b] in X
by A4, A37, A38, A40, Th31;
verum
end;
thus
for a being Element of C1 holds f . a = X .: (Fin a)
by A4; verum