let T be non empty up-complete TopPoset; :: thesis: ( T is upper implies T is order_consistent )
assume A1:
T is upper
; :: thesis: T is order_consistent
then reconsider BB = { ((downarrow x) ` ) where x is Element of T : verum } as prebasis of T by Def1;
for x being Element of T holds
( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V ) )
proof
let x be
Element of
T;
:: thesis: ( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V ) )
thus
downarrow x = Cl {x}
:: thesis: for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V
thus
for
N being
eventually-directed net of
T st
x = sup N holds
for
V being
a_neighborhood of
x holds
N is_eventually_in V
:: thesis: verumproof
let N be
eventually-directed net of
T;
:: thesis: ( x = sup N implies for V being a_neighborhood of x holds N is_eventually_in V )
assume A11:
x = sup N
;
:: thesis: for V being a_neighborhood of x holds N is_eventually_in V
A12:
x =
Sup
by A11, WAYBEL_2:def 1
.=
sup (rng (netmap N,T))
by YELLOW_2:def 5
;
let V be
a_neighborhood of
x;
:: thesis: N is_eventually_in V
A13:
x in Int V
by CONNSP_2:def 1;
FinMeetCl BB is
Basis of
T
by YELLOW_9:23;
then A14:
the
topology of
T = UniCl (FinMeetCl BB)
by YELLOW_9:22;
Int V is
open
by TOPS_1:51;
then
Int V in the
topology of
T
by PRE_TOPC:def 5;
then consider Y being
Subset-Family of
T such that A15:
(
Y c= FinMeetCl BB &
Int V = union Y )
by A14, CANTOR_1:def 1;
consider Y1 being
set such that A16:
(
x in Y1 &
Y1 in Y )
by A13, A15, TARSKI:def 4;
consider Z being
Subset-Family of
T such that A17:
(
Z c= BB &
Z is
finite &
Y1 = Intersect Z )
by A15, A16, CANTOR_1:def 4;
reconsider rngN =
rng (netmap N,T) as
Subset of
T ;
rngN is
directed
by WAYBEL_2:18;
then
ex
a being
Element of
T st
(
a is_>=_than rngN & ( for
b being
Element of
T st
b is_>=_than rngN holds
a <= b ) )
by WAYBEL_0:def 39;
then A18:
ex_sup_of rngN,
T
by YELLOW_0:15;
defpred S1[
set ,
set ]
means for
i,
j being
Element of
N st
i = $2 &
j >= i holds
N . j in $1;
A19:
for
Q being
set st
Q in Z holds
ex
b being
set st
(
b in the
carrier of
N &
S1[
Q,
b] )
proof
let Q be
set ;
:: thesis: ( Q in Z implies ex b being set st
( b in the carrier of N & S1[Q,b] ) )
assume A20:
Q in Z
;
:: thesis: ex b being set st
( b in the carrier of N & S1[Q,b] )
then
Q in BB
by A17;
then consider v1 being
Element of
T such that A21:
Q = (downarrow v1) `
;
x in (downarrow v1) `
by A16, A17, A20, A21, SETFAM_1:58;
then
(
x in [#] T & not
x in downarrow v1 )
by XBOOLE_0:def 5;
then A22:
(
x in [#] T & not
x <= v1 )
by WAYBEL_0:17;
not
rngN c= downarrow v1
then consider w being
set such that A24:
(
w in rngN & not
w in downarrow v1 )
by TARSKI:def 3;
reconsider w' =
w as
Element of
T by A24;
consider i being
set such that A25:
i in dom the
mapping of
N
and A26:
w' = the
mapping of
N . i
by A24, FUNCT_1:def 5;
reconsider i =
i as
Element of
N by A25;
consider b being
Element of
N such that A27:
for
l being
Element of
N st
b <= l holds
N . i <= N . l
by WAYBEL_0:11;
take
b
;
:: thesis: ( b in the carrier of N & S1[Q,b] )
thus
b in the
carrier of
N
;
:: thesis: S1[Q,b]
thus
for
j,
k being
Element of
N st
j = b &
k >= j holds
N . k in Q
:: thesis: verum
end;
consider f being
Function such that A30:
(
dom f = Z &
rng f c= the
carrier of
N )
and A31:
for
Q being
set st
Q in Z holds
S1[
Q,
f . Q]
from WELLORD2:sch 1(A19);
reconsider rngf =
rng f as
finite Subset of
([#] N) by A17, A30, FINSET_1:26;
[#] N is
directed
by WAYBEL_0:def 6;
then consider k being
Element of
N such that A32:
(
k in [#] N &
k is_>=_than rngf )
by WAYBEL_0:1;
take
k
;
:: according to WAYBEL_0:def 11 :: thesis: for b1 being Element of the carrier of N holds
( not k <= b1 or N . b1 in V )
let k1 be
Element of
N;
:: thesis: ( not k <= k1 or N . k1 in V )
assume A33:
k <= k1
;
:: thesis: N . k1 in V
then
(
N . k1 in Y1 &
Y1 c= union Y )
by A16, A17, SETFAM_1:58, ZFMISC_1:92;
then
(
N . k1 in Int V &
Int V c= V )
by A15, TOPS_1:44;
hence
N . k1 in V
;
:: thesis: verum
end;
end;
hence
T is order_consistent
by Def2; :: thesis: verum