let X be non empty set ; :: thesis: for x0 being set ex B0 being prebasis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { ({x} `) where x is Element of X : verum }
let x0 be set ; :: thesis: ex B0 being prebasis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { ({x} `) where x is Element of X : verum }
set T = DiscrWithInfin (X,x0);
set SX = SmallestPartition X;
set FX = { (F `) where F is Subset of X : F is finite } ;
set AX = { ({x} `) where x is Element of X : verum } ;
reconsider SX = SmallestPartition X as Subset-Family of (DiscrWithInfin (X,x0)) by Def5;
{ ({x} `) where x is Element of X : verum } c= bool X
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ({x} `) where x is Element of X : verum } or a in bool X )
assume a in { ({x} `) where x is Element of X : verum } ; :: thesis: a in bool X
then ex x being Element of X st a = {x} ` ;
hence a in bool X ; :: thesis: verum
end;
then reconsider AX = { ({x} `) where x is Element of X : verum } as Subset-Family of (DiscrWithInfin (X,x0)) by Def5;
reconsider pB = (SX \ {{x0}}) \/ AX as Subset-Family of (DiscrWithInfin (X,x0)) ;
consider B0 being Basis of (DiscrWithInfin (X,x0)) such that
A1: B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } by Th29;
A2: the carrier of (DiscrWithInfin (X,x0)) = X by Def5;
A3: { (F `) where F is Subset of X : F is finite } c= FinMeetCl pB
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 FinMeetCl pB )
assume a in { (F `) where F is Subset of X : F is finite } ; :: thesis: a in FinMeetCl pB
then consider F being Subset of (DiscrWithInfin (X,x0)) such that
A4: a = F ` and
A5: F is finite by A2;
set SF = SmallestPartition F;
bool F c= bool X by A2, ZFMISC_1:67;
then reconsider SF = SmallestPartition F as Subset-Family of (DiscrWithInfin (X,x0)) by A2, XBOOLE_1:1;
per cases ( F = {} or F <> {} ) ;
suppose F <> {} ; :: thesis: a in FinMeetCl pB
then reconsider F = F as non empty Subset of (DiscrWithInfin (X,x0)) ;
SF is a_partition of F ;
then reconsider SF = SF as non empty Subset-Family of (DiscrWithInfin (X,x0)) ;
A6: COMPLEMENT SF c= pB
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in COMPLEMENT SF or a in pB )
assume A7: a in COMPLEMENT SF ; :: thesis: a in pB
then reconsider a = a as Subset of (DiscrWithInfin (X,x0)) ;
a ` in SF by A7, SETFAM_1:def 7;
then a ` in { {b} where b is Element of F : verum } by EQREL_1:37;
then consider b being Element of F such that
A8: a ` = {b} ;
reconsider b = b as Element of X by Def5;
{b} ` in AX ;
hence a in pB by A2, A8, XBOOLE_0:def 3; :: thesis: verum
end;
F = union SF by EQREL_1:def 4;
then A9: a = meet (COMPLEMENT SF) by A4, TOPS_2:6;
COMPLEMENT SF is finite by A5, TOPS_2:8;
then Intersect (COMPLEMENT SF) in FinMeetCl pB by A6, CANTOR_1:def 3;
hence a in FinMeetCl pB by A9, SETFAM_1:def 9; :: thesis: verum
end;
end;
end;
A10: pB c= FinMeetCl pB by CANTOR_1:4;
A11: B0 c= FinMeetCl pB
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in B0 or a in FinMeetCl pB )
assume a in B0 ; :: thesis: a in FinMeetCl pB
then ( a in SX \ {{x0}} or a in { (F `) where F is Subset of X : F is finite } ) by A1, XBOOLE_0:def 3;
then ( a in pB or a in { (F `) where F is Subset of X : F is finite } ) by XBOOLE_0:def 3;
hence a in FinMeetCl pB by A10, A3; :: thesis: verum
end;
A12: B0 c= the topology of (DiscrWithInfin (X,x0)) by TOPS_2:64;
AX c= { (F `) where F is Subset of X : F is finite }
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in AX or a in { (F `) where F is Subset of X : F is finite } )
assume a in AX ; :: thesis: a in { (F `) where F is Subset of X : F is finite }
then ex x being Element of X st a = {x} ` ;
hence a in { (F `) where F is Subset of X : F is finite } ; :: thesis: verum
end;
then pB c= B0 by A1, XBOOLE_1:9;
then pB c= the topology of (DiscrWithInfin (X,x0)) by A12;
then FinMeetCl pB c= FinMeetCl the topology of (DiscrWithInfin (X,x0)) by CANTOR_1:14;
then FinMeetCl pB c= the topology of (DiscrWithInfin (X,x0)) by CANTOR_1:5;
then FinMeetCl pB is Basis of (DiscrWithInfin (X,x0)) by A11, WAYBEL19:22;
then pB is prebasis of (DiscrWithInfin (X,x0)) by YELLOW_9:23;
hence ex B0 being prebasis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { ({x} `) where x is Element of X : verum } ; :: thesis: verum