let X, x0 be set ; :: thesis: ex B0 being Basis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite }
set T = DiscrWithInfin (X,x0);
set B1 = (SmallestPartition X) \ {{x0}};
set B2 = { (F `) where F is Subset of X : F is finite } ;
A1: (SmallestPartition X) \ {{x0}} c= the topology of (DiscrWithInfin (X,x0))
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (SmallestPartition X) \ {{x0}} or a in the topology of (DiscrWithInfin (X,x0)) )
reconsider aa = a as set by TARSKI:1;
assume A2: a in (SmallestPartition X) \ {{x0}} ; :: thesis: a in the topology of (DiscrWithInfin (X,x0))
then A3: a in SmallestPartition X by ZFMISC_1:56;
then reconsider X = X as non empty set ;
SmallestPartition X = { {x} where x is Element of X : verum } by EQREL_1:37;
then A4: ex x being Element of X st a = {x} by A3;
a <> {x0} by A2, ZFMISC_1:56;
then not x0 in aa by A4, TARSKI:def 1;
then a is open Subset of (DiscrWithInfin (X,x0)) by A2, Def5, Th19;
hence a in the topology of (DiscrWithInfin (X,x0)) by PRE_TOPC:def 2; :: thesis: verum
end;
A5: the carrier of (DiscrWithInfin (X,x0)) = X by Def5;
{ (F `) where F is Subset of X : F is finite } c= bool the carrier of (DiscrWithInfin (X,x0))
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (F `) where F is Subset of X : F is finite } or a in bool the carrier of (DiscrWithInfin (X,x0)) )
assume a in { (F `) where F is Subset of X : F is finite } ; :: thesis: a in bool the carrier of (DiscrWithInfin (X,x0))
then ex F being Subset of X st
( a = F ` & F is finite ) ;
hence a in bool the carrier of (DiscrWithInfin (X,x0)) by A5; :: thesis: verum
end;
then reconsider B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } as Subset-Family of (DiscrWithInfin (X,x0)) by A5, XBOOLE_1:8;
A6: now :: thesis: for A being Subset of (DiscrWithInfin (X,x0)) st A is open holds
for p being Point of (DiscrWithInfin (X,x0)) st p in A holds
ex a being Subset of (DiscrWithInfin (X,x0)) st
( a in B0 & p in a & a c= A )
let A be Subset of (DiscrWithInfin (X,x0)); :: thesis: ( A is open implies for p being Point of (DiscrWithInfin (X,x0)) st p in A holds
ex a being Subset of (DiscrWithInfin (X,x0)) st
( a in B0 & p in a & a c= A ) )
assume A is open ; :: thesis: for p being Point of (DiscrWithInfin (X,x0)) st p in A holds
ex a being Subset of (DiscrWithInfin (X,x0)) st
( a in B0 & p in a & a c= A )
then A7: ( not x0 in A or A ` is finite ) by Th19;
let p be Point of (DiscrWithInfin (X,x0)); :: thesis: ( p in A implies ex a being Subset of (DiscrWithInfin (X,x0)) st
( a in B0 & p in a & a c= A ) )
assume A8: p in A ; :: thesis: ex a being Subset of (DiscrWithInfin (X,x0)) st
( a in B0 & p in a & a c= A )
reconsider X9 = X as non empty set by A8, Def5;
reconsider p9 = p as Element of X9 by Def5;
SmallestPartition X = { {x} where x is Element of X9 : verum } by EQREL_1:37;
then A9: {p9} in SmallestPartition X ;
( {p} <> {x0} or (A `) ` in { (F `) where F is Subset of X : F is finite } ) by A5, A8, A7, ZFMISC_1:3;
then ( not {p} in {{x0}} or A in { (F `) where F is Subset of X : F is finite } ) by TARSKI:def 1;
then ( {p} in (SmallestPartition X) \ {{x0}} or A in { (F `) where F is Subset of X : F is finite } ) by A9, XBOOLE_0:def 5;
then ( ( {p} in B0 & p in {p} & {p} c= A ) or ( A in B0 & A c= A ) ) by A8, XBOOLE_0:def 3, ZFMISC_1:31;
hence ex a being Subset of (DiscrWithInfin (X,x0)) st
( a in B0 & p in a & a c= A ) by A8; :: thesis: verum
end;
{ (F `) where F is Subset of X : F is finite } c= the topology of (DiscrWithInfin (X,x0))
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (F `) where F is Subset of X : F is finite } or a in the topology of (DiscrWithInfin (X,x0)) )
assume a in { (F `) where F is Subset of X : F is finite } ; :: thesis: a in the topology of (DiscrWithInfin (X,x0))
then consider F being Subset of X such that
A10: a = F ` and
A11: F is finite ;
(F `) ` is finite by A11;
then a is open Subset of (DiscrWithInfin (X,x0)) by A5, A10, Th19;
hence a in the topology of (DiscrWithInfin (X,x0)) by PRE_TOPC:def 2; :: thesis: verum
end;
then reconsider B0 = B0 as Basis of (DiscrWithInfin (X,x0)) by A1, A6, XBOOLE_1:8, YELLOW_9:32;
take B0 ; :: thesis: B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite }
thus B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } ; :: thesis: verum