let L be complete LATTICE; ( S7[L] implies S8[L] )
assume A1:
S7[L]
; S8[L]
let SL be Scott TopAugmentation of L; for S being complete LATTICE
for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]
let S be complete LATTICE; for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]
let SS be Scott TopAugmentation of S; sigma [:S,L:] = the topology of [:SS,SL:]
A2:
RelStr(# the carrier of SS,the InternalRel of SS #) = RelStr(# the carrier of S,the InternalRel of S #)
by YELLOW_9:def 4;
UPS L,(BoolePoset 1) is non empty full SubRelStr of (BoolePoset 1) |^ the carrier of L
by WAYBEL27:def 4;
then A3:
(UPS L,(BoolePoset 1)) |^ the carrier of S is non empty full SubRelStr of ((BoolePoset 1) |^ the carrier of L) |^ the carrier of S
by YELLOW16:41;
UPS S,(UPS L,(BoolePoset 1)) is non empty full SubRelStr of (UPS L,(BoolePoset 1)) |^ the carrier of S
by WAYBEL27:def 4;
then A4:
UPS S,(UPS L,(BoolePoset 1)) is non empty full SubRelStr of ((BoolePoset 1) |^ the carrier of L) |^ the carrier of S
by A3, WAYBEL15:1;
consider f5 being Function of (UPS L,(BoolePoset 1)),(InclPoset (sigma L)) such that
A5:
f5 is isomorphic
and
A6:
for f being directed-sups-preserving Function of L,(BoolePoset 1) holds f5 . f = f " {1}
by WAYBEL27:33;
set f6 = UPS (id S),f5;
consider f3 being Function of (UPS S,(UPS L,(BoolePoset 1))),(UPS [:S,L:],(BoolePoset 1)) such that
A7:
( f3 is uncurrying & f3 is isomorphic )
by WAYBEL27:47;
set f4 = f3 " ;
set T = Sigma (InclPoset the topology of SL);
consider f1 being Function of (UPS [:S,L:],(BoolePoset 1)),(InclPoset (sigma [:S,L:])) such that
A8:
f1 is isomorphic
and
A9:
for f being directed-sups-preserving Function of [:S,L:],(BoolePoset 1) holds f1 . f = f " {1}
by WAYBEL27:33;
A10:
f3 " is isomorphic
by A7, YELLOW14:11;
set f2 = f1 " ;
set G = ((UPS (id S),f5) * (f3 " )) * (f1 " );
A11:
the topology of SL = sigma L
by YELLOW_9:51;
then A12:
RelStr(# the carrier of (Sigma (InclPoset the topology of SL)),the InternalRel of (Sigma (InclPoset the topology of SL)) #) = RelStr(# the carrier of (InclPoset (sigma L)),the InternalRel of (InclPoset (sigma L)) #)
by YELLOW_9:def 4;
A13:
the carrier of (UPS S,(InclPoset (sigma L))) = the carrier of (ContMaps SS,(Sigma (InclPoset the topology of SL)))
proof
thus
the
carrier of
(UPS S,(InclPoset (sigma L))) c= the
carrier of
(ContMaps SS,(Sigma (InclPoset the topology of SL)))
XBOOLE_0:def 10 the carrier of (ContMaps SS,(Sigma (InclPoset the topology of SL))) c= the carrier of (UPS S,(InclPoset (sigma L)))proof
let x be
set ;
TARSKI:def 3 ( not x in the carrier of (UPS S,(InclPoset (sigma L))) or x in the carrier of (ContMaps SS,(Sigma (InclPoset the topology of SL))) )
assume A14:
x in the
carrier of
(UPS S,(InclPoset (sigma L)))
;
x in the carrier of (ContMaps SS,(Sigma (InclPoset the topology of SL)))
then reconsider x1 =
x as
Function of
SS,
(Sigma (InclPoset the topology of SL)) by A2, A12, WAYBEL27:def 4;
x is
directed-sups-preserving Function of
S,
(InclPoset (sigma L))
by A14, WAYBEL27:def 4;
then
x1 is
directed-sups-preserving
by A2, A12, WAYBEL21:6;
then
x1 is
continuous
by WAYBEL17:22;
hence
x in the
carrier of
(ContMaps SS,(Sigma (InclPoset the topology of SL)))
by WAYBEL24:def 3;
verum
end;
let x be
set ;
TARSKI:def 3 ( not x in the carrier of (ContMaps SS,(Sigma (InclPoset the topology of SL))) or x in the carrier of (UPS S,(InclPoset (sigma L))) )
assume
x in the
carrier of
(ContMaps SS,(Sigma (InclPoset the topology of SL)))
;
x in the carrier of (UPS S,(InclPoset (sigma L)))
then consider x1 being
Function of
SS,
(Sigma (InclPoset the topology of SL)) such that A15:
x1 = x
and A16:
x1 is
continuous
by WAYBEL24:def 3;
reconsider x2 =
x1 as
Function of
S,
(InclPoset (sigma L)) by A2, A12;
x1 is
directed-sups-preserving
by A16, WAYBEL17:22;
then
x2 is
directed-sups-preserving
by A2, A12, WAYBEL21:6;
hence
x in the
carrier of
(UPS S,(InclPoset (sigma L)))
by A15, WAYBEL27:def 4;
verum
end;
then reconsider G = ((UPS (id S),f5) * (f3 " )) * (f1 " ) as Function of (InclPoset (sigma [:S,L:])),(ContMaps SS,(Sigma (InclPoset the topology of SL))) ;
set F = Theta SS,SL;
A17:
RelStr(# the carrier of SL,the InternalRel of SL #) = RelStr(# the carrier of L,the InternalRel of L #)
by YELLOW_9:def 4;
( (BoolePoset 1) |^ the carrier of [:S,L:] = (BoolePoset 1) |^ [:the carrier of S,the carrier of L:] & UPS [:S,L:],(BoolePoset 1) is non empty full SubRelStr of (BoolePoset 1) |^ the carrier of [:S,L:] )
by WAYBEL27:def 4, YELLOW_3:def 2;
then A18:
f3 " is currying
by A7, A4, Th3;
A19:
for V being Element of (InclPoset (sigma [:S,L:]))
for s being Element of S holds (G . V) . s = { y where y is Element of L : [s,y] in V }
proof
let V be
Element of
(InclPoset (sigma [:S,L:]));
for s being Element of S holds (G . V) . s = { y where y is Element of L : [s,y] in V } let s be
Element of
S;
(G . V) . s = { y where y is Element of L : [s,y] in V }
reconsider fff =
(f3 " ) . ((f1 " ) . V) as
directed-sups-preserving Function of
S,
(UPS L,(BoolePoset 1)) by WAYBEL27:def 4;
reconsider f2V =
(f1 " ) . V as
directed-sups-preserving Function of
[:S,L:],
(BoolePoset 1) by WAYBEL27:def 4;
A20:
(
f5 is
sups-preserving &
(f5 * fff) * (id the carrier of S) = f5 * fff )
by A5, FUNCT_2:23, WAYBEL13:20;
A21:
((f3 " ) . ((f1 " ) . V)) . s is
directed-sups-preserving Function of
L,
(BoolePoset 1)
by WAYBEL27:def 4;
then A22:
dom (((f3 " ) . ((f1 " ) . V)) . s) = the
carrier of
L
by FUNCT_2:def 1;
G . V =
((UPS (id S),f5) * (f3 " )) . ((f1 " ) . V)
by FUNCT_2:21
.=
(UPS (id S),f5) . ((f3 " ) . ((f1 " ) . V))
by FUNCT_2:21
.=
f5 * fff
by A20, WAYBEL27:def 5
;
then A23:
(G . V) . s =
f5 . (fff . s)
by FUNCT_2:21
.=
(((f3 " ) . ((f1 " ) . V)) . s) " {1}
by A6, A21
;
A24:
rng f1 = [#] (InclPoset (sigma [:S,L:]))
by A8, FUNCT_2:def 3;
dom (f3 " ) = the
carrier of
(UPS [:S,L:],(BoolePoset 1))
by FUNCT_2:def 1;
then A25:
(f3 " ) . ((f1 " ) . V) = curry ((f1 " ) . V)
by A18, WAYBEL27:def 2;
rng f1 = the
carrier of
(InclPoset (sigma [:S,L:]))
by A8, FUNCT_2:def 3;
then A26:
V =
(id (rng f1)) . V
by FUNCT_1:35
.=
(f1 * (f1 " )) . V
by A8, A24, TOPS_2:65
.=
f1 . ((f1 " ) . V)
by FUNCT_2:21
.=
f2V " {1}
by A9
;
thus
(G . V) . s c= { y where y is Element of L : [s,y] in V }
XBOOLE_0:def 10 { y where y is Element of L : [s,y] in V } c= (G . V) . sproof
let x be
set ;
TARSKI:def 3 ( not x in (G . V) . s or x in { y where y is Element of L : [s,y] in V } )
assume A27:
x in (G . V) . s
;
x in { y where y is Element of L : [s,y] in V }
then
x in dom (((f3 " ) . ((f1 " ) . V)) . s)
by A23, FUNCT_1:def 13;
then reconsider y =
x as
Element of
L by A21, FUNCT_2:def 1;
(((f3 " ) . ((f1 " ) . V)) . s) . x in {1}
by A23, A27, FUNCT_1:def 13;
then A28:
(((f3 " ) . ((f1 " ) . V)) . s) . y = 1
by TARSKI:def 1;
A29:
dom f2V = the
carrier of
[:S,L:]
by FUNCT_2:def 1;
then
[s,y] in dom ((f1 " ) . V)
;
then
((f1 " ) . V) . s,
y = 1
by A25, A28, FUNCT_5:27;
then
((f1 " ) . V) . s,
y in {1}
by TARSKI:def 1;
then
[s,y] in ((f1 " ) . V) " {1}
by A29, FUNCT_1:def 13;
hence
x in { y where y is Element of L : [s,y] in V }
by A26;
verum
end;
let x be
set ;
TARSKI:def 3 ( not x in { y where y is Element of L : [s,y] in V } or x in (G . V) . s )
assume
x in { y where y is Element of L : [s,y] in V }
;
x in (G . V) . s
then consider y being
Element of
L such that A30:
y = x
and A31:
[s,y] in V
;
dom f2V = the
carrier of
[:S,L:]
by FUNCT_2:def 1;
then A32:
[s,y] in dom ((f1 " ) . V)
;
then reconsider cs =
(curry ((f1 " ) . V)) . s as
Function by FUNCT_5:26;
((f1 " ) . V) . s,
y in {1}
by A26, A31, FUNCT_1:def 13;
then
((f1 " ) . V) . s,
y = 1
by TARSKI:def 1;
then
cs . y = 1
by A32, FUNCT_5:27;
then
(((f3 " ) . ((f1 " ) . V)) . s) . y in {1}
by A25, TARSKI:def 1;
hence
x in (G . V) . s
by A23, A30, A22, FUNCT_1:def 13;
verum
end;
S6[SL]
by A1, A11, Lm8;
then
S4[SL]
by Lm6;
then A33:
Theta SS,SL is isomorphic
by Lm3;
A34:
the carrier of (InclPoset (sigma [:S,L:])) c= the carrier of (InclPoset the topology of [:SS,SL:])
proof
let V be
set ;
TARSKI:def 3 ( not V in the carrier of (InclPoset (sigma [:S,L:])) or V in the carrier of (InclPoset the topology of [:SS,SL:]) )
assume
V in the
carrier of
(InclPoset (sigma [:S,L:]))
;
V in the carrier of (InclPoset the topology of [:SS,SL:])
then reconsider V1 =
V as
Element of
(InclPoset (sigma [:S,L:])) ;
rng (Theta SS,SL) = the
carrier of
(ContMaps SS,(Sigma (InclPoset the topology of SL)))
by A33, FUNCT_2:def 3;
then consider W being
set such that A35:
W in dom (Theta SS,SL)
and A36:
(Theta SS,SL) . W = G . V1
by FUNCT_1:def 5;
reconsider W2 =
W as
Element of
(InclPoset the topology of [:SS,SL:]) by A35;
dom (Theta SS,SL) = the
carrier of
(InclPoset the topology of [:SS,SL:])
by FUNCT_2:def 1;
then
W in the
topology of
[:SS,SL:]
by A35, YELLOW_1:1;
then reconsider W1 =
W2 as
open Subset of
[:SS,SL:] by PRE_TOPC:def 5;
A37:
V c= W
proof
let v be
set ;
TARSKI:def 3 ( not v in V or v in W )
assume A38:
v in V
;
v in W
V1 in the
carrier of
(InclPoset (sigma [:S,L:]))
;
then
V in sigma [:S,L:]
by YELLOW_1:1;
then
V c= the
carrier of
[:S,L:]
;
then
V c= [:the carrier of S,the carrier of L:]
by YELLOW_3:def 2;
then consider v1,
v2 being
set such that A39:
v1 in the
carrier of
S
and A40:
v2 in the
carrier of
L
and A41:
v = [v1,v2]
by A38, ZFMISC_1:103;
reconsider v2 =
v2 as
Element of
L by A40;
reconsider v1 =
v1 as
Element of
S by A39;
v2 in { y where y is Element of L : [v1,y] in V }
by A38, A41;
then
v2 in (G . V1) . v1
by A19;
then
v2 in (W1,the carrier of S *graph ) . v1
by A2, A36, Def3;
then
v2 in Im W1,
v1
by WAYBEL26:def 5;
then
ex
v19 being
set st
(
[v19,v2] in W &
v19 in {v1} )
by RELAT_1:def 13;
hence
v in W
by A41, TARSKI:def 1;
verum
end;
W c= V
proof
let w be
set ;
TARSKI:def 3 ( not w in W or w in V )
assume A42:
w in W
;
w in V
W1 c= the
carrier of
[:SS,SL:]
;
then
W1 c= [:the carrier of SS,the carrier of SL:]
by BORSUK_1:def 5;
then consider w1,
w2 being
set such that A43:
w1 in the
carrier of
S
and A44:
w2 in the
carrier of
L
and A45:
w = [w1,w2]
by A2, A17, A42, ZFMISC_1:103;
reconsider w2 =
w2 as
Element of
L by A44;
reconsider w1 =
w1 as
Element of
S by A43;
w1 in {w1}
by TARSKI:def 1;
then
w2 in Im W1,
w1
by A42, A45, RELAT_1:def 13;
then
w2 in (W1,the carrier of S *graph ) . w1
by WAYBEL26:def 5;
then
w2 in ((Theta SS,SL) . W2) . w1
by A2, Def3;
then
w2 in { y where y is Element of L : [w1,y] in V }
by A19, A36;
then
ex
w29 being
Element of
L st
(
w29 = w2 &
[w1,w29] in V )
;
hence
w in V
by A45;
verum
end;
then
W2 = V
by A37, XBOOLE_0:def 10;
hence
V in the
carrier of
(InclPoset the topology of [:SS,SL:])
;
verum
end;
InclPoset (sigma L) = InclPoset the topology of SL
by YELLOW_9:51;
then
UPS (id S),f5 is isomorphic
by A5, WAYBEL27:35;
then A46:
(UPS (id S),f5) * (f3 " ) is isomorphic
by A10, Th7;
A47:
f1 " is isomorphic
by A8, YELLOW14:11;
the carrier of (InclPoset the topology of [:SS,SL:]) c= the carrier of (InclPoset (sigma [:S,L:]))
proof
let W be
set ;
TARSKI:def 3 ( not W in the carrier of (InclPoset the topology of [:SS,SL:]) or W in the carrier of (InclPoset (sigma [:S,L:])) )
assume A48:
W in the
carrier of
(InclPoset the topology of [:SS,SL:])
;
W in the carrier of (InclPoset (sigma [:S,L:]))
then reconsider W2 =
W as
Element of
(InclPoset the topology of [:SS,SL:]) ;
W in the
topology of
[:SS,SL:]
by A48, YELLOW_1:1;
then reconsider W1 =
W2 as
open Subset of
[:SS,SL:] by PRE_TOPC:def 5;
G is
onto
by A47, A46, A13, Th7, YELLOW14:10;
then
rng G = the
carrier of
(ContMaps SS,(Sigma (InclPoset the topology of SL)))
by FUNCT_2:def 3;
then consider V being
set such that A49:
V in dom G
and A50:
G . V = (Theta SS,SL) . W2
by FUNCT_1:def 5;
reconsider V =
V as
Element of
(InclPoset (sigma [:S,L:])) by A49;
A51:
V c= W
proof
let v be
set ;
TARSKI:def 3 ( not v in V or v in W )
assume A52:
v in V
;
v in W
V in the
carrier of
(InclPoset (sigma [:S,L:]))
;
then
V in sigma [:S,L:]
by YELLOW_1:1;
then
V c= the
carrier of
[:S,L:]
;
then
V c= [:the carrier of S,the carrier of L:]
by YELLOW_3:def 2;
then consider v1,
v2 being
set such that A53:
v1 in the
carrier of
S
and A54:
v2 in the
carrier of
L
and A55:
v = [v1,v2]
by A52, ZFMISC_1:103;
reconsider v2 =
v2 as
Element of
L by A54;
reconsider v1 =
v1 as
Element of
S by A53;
v2 in { y where y is Element of L : [v1,y] in V }
by A52, A55;
then
v2 in (G . V) . v1
by A19;
then
v2 in (W1,the carrier of S *graph ) . v1
by A2, A50, Def3;
then
v2 in Im W1,
v1
by WAYBEL26:def 5;
then
ex
v19 being
set st
(
[v19,v2] in W &
v19 in {v1} )
by RELAT_1:def 13;
hence
v in W
by A55, TARSKI:def 1;
verum
end;
W c= V
proof
let w be
set ;
TARSKI:def 3 ( not w in W or w in V )
assume A56:
w in W
;
w in V
W1 c= the
carrier of
[:SS,SL:]
;
then
W1 c= [:the carrier of SS,the carrier of SL:]
by BORSUK_1:def 5;
then consider w1,
w2 being
set such that A57:
w1 in the
carrier of
S
and A58:
w2 in the
carrier of
L
and A59:
w = [w1,w2]
by A2, A17, A56, ZFMISC_1:103;
reconsider w2 =
w2 as
Element of
L by A58;
reconsider w1 =
w1 as
Element of
S by A57;
w1 in {w1}
by TARSKI:def 1;
then
w2 in Im W1,
w1
by A56, A59, RELAT_1:def 13;
then
w2 in (W1,the carrier of S *graph ) . w1
by WAYBEL26:def 5;
then
w2 in ((Theta SS,SL) . W2) . w1
by A2, Def3;
then
w2 in { y where y is Element of L : [w1,y] in V }
by A19, A50;
then
ex
w29 being
Element of
L st
(
w29 = w2 &
[w1,w29] in V )
;
hence
w in V
by A59;
verum
end;
then
W = V
by A51, XBOOLE_0:def 10;
hence
W in the
carrier of
(InclPoset (sigma [:S,L:]))
;
verum
end;
then
the carrier of (InclPoset (sigma [:S,L:])) = the carrier of (InclPoset the topology of [:SS,SL:])
by A34, XBOOLE_0:def 10;
hence sigma [:S,L:] =
the carrier of (InclPoset the topology of [:SS,SL:])
by YELLOW_1:1
.=
the topology of [:SS,SL:]
by YELLOW_1:1
;
verum