let L be complete LATTICE; :: thesis: ( ( for J being non empty set st J in the_universe_of the carrier of L holds
for K being V9() ManySortedSet of st ( for j being Element of J holds K . j in the_universe_of the carrier of L ) holds
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup ) implies L is continuous )
assume A1:
for J being non empty set st J in the_universe_of the carrier of L holds
for K being V9() ManySortedSet of st ( for j being Element of J holds K . j in the_universe_of the carrier of L ) holds
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup
; :: thesis: L is continuous
now let x be
Element of
L;
:: thesis: x = sup (waybelow x)set J =
{ j where j is non empty directed Subset of L : x <= sup j } ;
set UN =
the_universe_of the
carrier of
L;
A2:
the_universe_of the
carrier of
L = Tarski-Class (the_transitive-closure_of the carrier of L)
by YELLOW_6:def 3;
reconsider UN =
the_universe_of the
carrier of
L as
universal set ;
A3:
the
carrier of
L c= the_transitive-closure_of the
carrier of
L
by CLASSES1:59;
the_transitive-closure_of the
carrier of
L in UN
by A2, CLASSES1:5;
then A4:
the
carrier of
L in UN
by A3, CLASSES1:def 1;
then A5:
bool the
carrier of
L in UN
by CLASSES2:65;
A6:
{ j where j is non empty directed Subset of L : x <= sup j } c= bool the
carrier of
L
then A7:
{ j where j is non empty directed Subset of L : x <= sup j } in UN
by A5, CLASSES1:def 1;
A8:
{x} is non
empty directed Subset of
L
by WAYBEL_0:5;
x <= sup {x}
by YELLOW_0:39;
then A9:
{x} in { j where j is non empty directed Subset of L : x <= sup j }
by A8;
then reconsider J =
{ j where j is non empty directed Subset of L : x <= sup j } as non
empty set ;
A10:
for
j being
Element of
J holds
j is non
empty directed Subset of
L
set K =
id J;
reconsider K =
id J as
ManySortedSet of ;
A12:
for
j being
Element of
J holds
K . j in UN
for
i being
set st
i in J holds
not
K . i is
empty
then reconsider K =
K as
V9()
ManySortedSet of
by PBOOLE:def 16;
deffunc H1(
set )
-> Element of
bool [:(K . $1),(K . $1):] =
id (K . $1);
ex
F being
Function st
(
dom F = J & ( for
j being
set st
j in J holds
F . j = H1(
j) ) )
from FUNCT_1:sch 3();
then consider F being
Function such that A13:
dom F = J
and A14:
for
j being
set st
j in J holds
F . j = id (K . j)
;
reconsider F =
F as
ManySortedSet of
by A13, PARTFUN1:def 4, RELAT_1:def 18;
for
j being
set st
j in dom F holds
F . j is
Function
then reconsider F =
F as
ManySortedFunction of
by FUNCOP_1:def 6;
for
j being
set st
j in J holds
F . j is
Function of
(K . j),
((J --> the carrier of L) . j)
then reconsider F =
F as
DoubleIndexedSet of
K,
L by PBOOLE:def 18;
A18:
for
j being
Element of
J for
k being
Element of
K . j holds
(F . j) . k = k
A19:
for
j being
Element of
J holds
rng (F . j) = j
A25:
for
j being
Element of
J holds
rng (F . j) is
directed
for
f being
Function st
f in dom (Frege F) holds
//\ ((Frege F) . f),
L <= sup (waybelow x)
proof
let f be
Function;
:: thesis: ( f in dom (Frege F) implies //\ ((Frege F) . f),L <= sup (waybelow x) )
assume A26:
f in dom (Frege F)
;
:: thesis: //\ ((Frege F) . f),L <= sup (waybelow x)
set a =
//\ ((Frege F) . f),
L;
for
D being non
empty directed Subset of
L st
x <= sup D holds
ex
d being
Element of
L st
(
d in D &
//\ ((Frege F) . f),
L <= d )
proof
let D be non
empty directed Subset of
L;
:: thesis: ( x <= sup D implies ex d being Element of L st
( d in D & //\ ((Frege F) . f),L <= d ) )
assume
x <= sup D
;
:: thesis: ex d being Element of L st
( d in D & //\ ((Frege F) . f),L <= d )
then
D in J
;
then reconsider D' =
D as
Element of
J ;
A27:
for
j being
Element of
J holds
f . j in K . j
A28:
dom f =
dom F
by A26, Th8
.=
J
by PARTFUN1:def 4
;
then
rng f c= the
carrier of
L
by TARSKI:def 3;
then reconsider f =
f as
Function of
J,the
carrier of
L by A28, FUNCT_2:4;
A32:
Inf <= f . D'
by YELLOW_2:55;
A33:
dom f =
dom F
by A26, Th8
.=
dom ((Frege F) . f)
by A26, Th8
;
then A37:
//\ ((Frege F) . f),
L <= f . D'
by A32, A33, FUNCT_1:9;
f . D' in K . D'
by A27;
then
f . D' in D'
by FUNCT_1:35;
hence
ex
d being
Element of
L st
(
d in D &
//\ ((Frege F) . f),
L <= d )
by A37;
:: thesis: verum
end;
then
//\ ((Frege F) . f),
L << x
by WAYBEL_3:def 1;
then
//\ ((Frege F) . f),
L in waybelow x
by WAYBEL_3:7;
hence
//\ ((Frege F) . f),
L <= sup (waybelow x)
by YELLOW_2:24;
:: thesis: verum
end; then A38:
Sup <= sup (waybelow x)
by Th15;
x is_<=_than rng (Sups )
then
x <= inf (rng (Sups ))
by YELLOW_0:33;
then A42:
x <= Inf
by YELLOW_2:def 6;
reconsider j =
{x} as
Element of
J by A9;
Sup =
sup (rng (F . j))
by YELLOW_2:def 5
.=
sup {x}
by A19
.=
x
by YELLOW_0:39
;
then
x in rng (Sups )
by Th14;
then
inf (rng (Sups )) <= x
by YELLOW_2:24;
then
Inf <= x
by YELLOW_2:def 6;
then A43:
x =
Inf
by A42, ORDERS_2:25
.=
Sup
by A1, A7, A12, A25
;
x is_>=_than waybelow x
by WAYBEL_3:9;
then
x >= sup (waybelow x)
by YELLOW_0:32;
hence
x = sup (waybelow x)
by A38, A43, ORDERS_2:25;
:: thesis: verum end;
then A44:
( L is up-complete & L is satisfying_axiom_of_approximation )
by WAYBEL_3:def 5;
thus
L is continuous
by A44; :: thesis: verum