let T be non empty TopSpace; :: thesis: for B being prebasis of T
for x, y being Element of (InclPoset the topology of T) st x c= y holds
( x << y iff for F being Subset of B st y c= union F holds
ex G being finite Subset of F st x c= union G )
let B be prebasis of T; :: thesis: for x, y being Element of (InclPoset the topology of T) st x c= y holds
( x << y iff for F being Subset of B st y c= union F holds
ex G being finite Subset of F st x c= union G )
consider BB being Basis of T such that
A1: BB c= FinMeetCl B by CANTOR_1:def 4;
set BT = BoolePoset the carrier of T;
set L = InclPoset the topology of T;
let x, y be Element of (InclPoset the topology of T); :: thesis: ( x c= y implies ( x << y iff for F being Subset of B st y c= union F holds
ex G being finite Subset of F st x c= union G ) )
assume A2: x c= y ; :: thesis: ( x << y iff for F being Subset of B st y c= union F holds
ex G being finite Subset of F st x c= union G )
A3: B c= the topology of T by TOPS_2:64;
hereby :: thesis: ( ( for F being Subset of B st y c= union F holds
ex G being finite Subset of F st x c= union G ) implies x << y )
assume A4: x << y ; :: thesis: for F being Subset of B st y c= union F holds
ex G being finite Subset of F st x c= union G
let F be Subset of B; :: thesis: ( y c= union F implies ex G being finite Subset of F st x c= union G )
assume A5: y c= union F ; :: thesis: ex G being finite Subset of F st x c= union G
reconsider FF = F as Subset-Family of T by XBOOLE_1:1;
FF is open
proof
let a be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not a in FF or a is open )
assume a in FF ; :: thesis: a is open
then a in B ;
hence a in the topology of T by A3; :: according to PRE_TOPC:def 2 :: thesis: verum
end;
hence ex G being finite Subset of F st x c= union G by A4, A5, WAYBEL_3:34; :: thesis: verum
end;
BoolePoset the carrier of T = InclPoset (bool the carrier of T) by YELLOW_1:4;
then A6: BoolePoset the carrier of T = RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) by YELLOW_1:def 1;
InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) by YELLOW_1:def 1;
then ( x in the topology of T & y in the topology of T ) ;
then reconsider X = x, Y = y as Subset of T ;
assume A7: for F being Subset of B st y c= union F holds
ex G being finite Subset of F st x c= union G ; :: thesis: x << y
A8: the topology of T c= UniCl BB by CANTOR_1:def 2;
now :: thesis: for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds
ex p being Element of T st
( p in y & p is_a_convergence_point_of F,T )
deffunc H1( set ) -> Element of bool x = x \ $1;
let F be ultra Filter of (BoolePoset the carrier of T); :: thesis: ( x in F implies ex p being Element of T st
( p in y & p is_a_convergence_point_of F,T ) )
assume that
A9: x in F and
A10: for p being Element of T holds
( not p in y or not p is_a_convergence_point_of F,T ) ; :: thesis: contradiction
defpred S1[ object , object ] means ex A being set st
( A = $2 & $1 in A & not $2 in F );
A11: now :: thesis: for p being object st p in y holds
ex r being object st
( r in B & S1[p,r] )
let p be object ; :: thesis: ( p in y implies ex r being object st
( r in B & S1[p,r] ) )
assume A12: p in y ; :: thesis: ex r being object st
( r in B & S1[p,r] )
then p in Y ;
then reconsider q = p as Element of T ;
not q is_a_convergence_point_of F,T by A10, A12;
then consider A being Subset of T such that
A13: A is open and
A14: q in A and
A15: not A in F ;
A in the topology of T by A13;
then consider AY being Subset-Family of T such that
A16: AY c= BB and
A17: A = union AY by A8, CANTOR_1:def 1;
consider ay being set such that
A18: q in ay and
A19: ay in AY by A14, A17, TARSKI:def 4;
reconsider ay = ay as Subset of T by A19;
ay in BB by A16, A19;
then consider BY being Subset-Family of T such that
A20: BY c= B and
A21: BY is finite and
A22: ay = Intersect BY by A1, CANTOR_1:def 3;
ay c= A by A17, A19, ZFMISC_1:74;
then not ay in F by A15, Th7;
then BY is not Subset of F by A21, A22, Th11;
then consider r being object such that
A23: ( r in BY & not r in F ) by TARSKI:def 3;
reconsider A = r as set by TARSKI:1;
take r = r; :: thesis: ( r in B & S1[p,r] )
thus r in B by A20, A23; :: thesis: S1[p,r]
thus S1[p,r] :: thesis: verum
proof
take A ; :: thesis: ( A = r & p in A & not r in F )
thus ( A = r & p in A & not r in F ) by A18, A22, A23, SETFAM_1:43; :: thesis: verum
end;
end;
consider f being Function such that
A24: ( dom f = y & rng f c= B ) and
A25: for p being object st p in y holds
S1[p,f . p] from FUNCT_1:sch 6(A11);
reconsider FF = rng f as Subset of B by A24;
y c= union FF
proof
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in y or p in union FF )
assume A26: p in y ; :: thesis: p in union FF
then consider A being set such that
A27: ( A = f . p & p in A & not f . p in F ) by A25;
( f . p in FF & p in f . p ) by A24, FUNCT_1:def 3, A27, A26;
hence p in union FF by TARSKI:def 4; :: thesis: verum
end;
then consider G being finite Subset of FF such that
A28: x c= union G by A7;
set gg = the Element of G;
consider g being Function such that
A29: ( dom g = G & ( for z being set st z in G holds
g . z = H1(z) ) ) from FUNCT_1:sch 5();
A30: rng g c= F
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng g or a in F )
A31: F is prime by Th22;
assume a in rng g ; :: thesis: a in F
then consider b being object such that
A32: b in G and
A33: a = g . b by A29, FUNCT_1:def 3;
b in FF by A32;
then b in B ;
then reconsider b = b as Subset of T ;
consider p being object such that
A34: ( p in y & b = f . p ) by A24, A32, FUNCT_1:def 3;
S1[p,f . p] by A25, A34;
then not b in F by A34;
then A35: the carrier of T \ b in F by A31, Th21;
a = x \ b by A29, A32, A33
.= X /\ (b `) by SUBSET_1:13
.= x /\ ( the carrier of T \ b) ;
hence a in F by A9, A35, Th9; :: thesis: verum
end;
then reconsider GG = rng g as finite Subset-Family of T by A6, A29, FINSET_1:8, XBOOLE_1:1;
x <> Bottom (BoolePoset the carrier of T) by A9, Th4;
then x <> {} by YELLOW_1:18;
then A36: G <> {} by A28, ZFMISC_1:2;
now :: thesis: for a being object holds not a in Intersect GG
let a be object ; :: thesis: not a in Intersect GG
assume A37: a in Intersect GG ; :: thesis: contradiction
now :: thesis: for z being set st z in G holds
not a in z
let z be set ; :: thesis: ( z in G implies not a in z )
assume z in G ; :: thesis: not a in z
then ( g . z in GG & g . z = x \ z ) by A29, FUNCT_1:def 3;
then a in x \ z by A37, SETFAM_1:43;
hence not a in z by XBOOLE_0:def 5; :: thesis: verum
end;
then for z being set holds
( not a in z or not z in G ) ;
then A38: not a in x by A28, TARSKI:def 4;
( g . the Element of G in GG & g . the Element of G = x \ the Element of G ) by A36, A29, FUNCT_1:def 3;
then a in x \ the Element of G by A37, SETFAM_1:43;
hence contradiction by A38; :: thesis: verum
end;
then A39: Intersect GG = {} by XBOOLE_0:def 1;
Intersect GG in F by A30, Th11;
then Bottom (BoolePoset the carrier of T) in F by A39, YELLOW_1:18;
hence contradiction by Th4; :: thesis: verum
end;
hence x << y by A2, Th30; :: thesis: verum