let A be uncountable set ; :: thesis: ex F being Subset-Family of (1TopSp [:A,A:]) st
( F is locally_finite & not F is sigma_discrete )
set TS = 1TopSp [:A,A:];
set F = { ([:{a},A:] \/ [:A,{a}:]) where a is Element of A : a in A } ;
{ ([:{a},A:] \/ [:A,{a}:]) where a is Element of A : a in A } c= bool [:A,A:]
proof
let f be set ; :: according to TARSKI:def 3 :: thesis: ( not f in { ([:{a},A:] \/ [:A,{a}:]) where a is Element of A : a in A } or f in bool [:A,A:] )
assume f in { ([:{a},A:] \/ [:A,{a}:]) where a is Element of A : a in A } ; :: thesis: f in bool [:A,A:]
then consider a being Element of A such that
A1: ( f = [:{a},A:] \/ [:A,{a}:] & a in A ) ;
( [:{a},A:] c= [:A,A:] & [:A,{a}:] c= [:A,A:] ) by ZFMISC_1:119;
then [:{a},A:] \/ [:A,{a}:] c= [:A,A:] by XBOOLE_1:8;
hence f in bool [:A,A:] by A1; :: thesis: verum
end;
then reconsider F = { ([:{a},A:] \/ [:A,{a}:]) where a is Element of A : a in A } as Subset-Family of (1TopSp [:A,A:]) ;
take F ; :: thesis: ( F is locally_finite & not F is sigma_discrete )
for z being Point of (1TopSp [:A,A:]) ex Z being Subset of (1TopSp [:A,A:]) st
( z in Z & Z is open & { O where O is Subset of (1TopSp [:A,A:]) : ( O in F & O meets Z ) } is finite )
proof
let z be Point of (1TopSp [:A,A:]); :: thesis: ex Z being Subset of (1TopSp [:A,A:]) st
( z in Z & Z is open & { O where O is Subset of (1TopSp [:A,A:]) : ( O in F & O meets Z ) } is finite )
set Z = {z};
reconsider Z = {z} as Subset of (1TopSp [:A,A:]) ;
A2: ( z in Z & Z is open ) by PRE_TOPC:def 5, ZFMISC_1:37;
consider x, y being set such that
A3: ( x in A & y in A & z = [x,y] ) by ZFMISC_1:def 2;
set UZ = { O where O is Subset of (1TopSp [:A,A:]) : ( O in F & O meets Z ) } ;
set xAAx = {([:{x},A:] \/ [:A,{x}:])};
set yAAy = {([:{y},A:] \/ [:A,{y}:])};
{ O where O is Subset of (1TopSp [:A,A:]) : ( O in F & O meets Z ) } c= {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])}
proof
let U be set ; :: according to TARSKI:def 3 :: thesis: ( not U in { O where O is Subset of (1TopSp [:A,A:]) : ( O in F & O meets Z ) } or U in {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])} )
assume U in { O where O is Subset of (1TopSp [:A,A:]) : ( O in F & O meets Z ) } ; :: thesis: U in {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])}
then consider O being Subset of (1TopSp [:A,A:]) such that
A4: ( U = O & O in F & O meets Z ) ;
consider a being Element of A such that
A5: ( O = [:{a},A:] \/ [:A,{a}:] & a in A ) by A4;
consider u being set such that
A6: ( u in O & u in Z ) by A4, XBOOLE_0:3;
now
per cases ( u in [:{a},A:] or u in [:A,{a}:] ) by A5, A6, XBOOLE_0:def 3;
end;
end;
hence U in {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])} by A4; :: thesis: verum
end;
hence ex Z being Subset of (1TopSp [:A,A:]) st
( z in Z & Z is open & { O where O is Subset of (1TopSp [:A,A:]) : ( O in F & O meets Z ) } is finite ) by A2; :: thesis: verum
end;
hence F is locally_finite by PCOMPS_1:def 2; :: thesis: not F is sigma_discrete
not F is sigma_discrete
proof
assume F is sigma_discrete ; :: thesis: contradiction
then consider f being sigma_discrete FamilySequence of (1TopSp [:A,A:]) such that
A7: F = Union f by Def4;
consider a being set such that
A8: a in A by XBOOLE_0:def 1;
reconsider a = a as Element of A by A8;
set aAAa = [:{a},A:] \/ [:A,{a}:];
defpred S1[ set , set ] means ( ( $2 in f . $1 & not f . $1 is empty ) or ( $2 = [:{a},A:] \/ [:A,{a}:] & f . $1 is empty ) );
A9: for k being set st k in NAT holds
ex f being set st
( f in F & S1[k,f] )
proof
let k be set ; :: thesis: ( k in NAT implies ex f being set st
( f in F & S1[k,f] ) )
assume k in NAT ; :: thesis: ex f being set st
( f in F & S1[k,f] )
then reconsider k = k as Element of NAT ;
now
per cases ( f . k is empty or not f . k is empty ) ;
suppose f . k is empty ; :: thesis: ex A being set st
( A in F & S1[k,A] )
then ( [:{a},A:] \/ [:A,{a}:] in F & S1[k,[:{a},A:] \/ [:A,{a}:]] ) ;
hence ex A being set st
( A in F & S1[k,A] ) ; :: thesis: verum
end;
suppose not f . k is empty ; :: thesis: ex A being set st
( A in F & S1[k,A] )
then consider A being set such that
A10: A in f . k by XBOOLE_0:def 1;
( A in F & S1[k,A] ) by A7, A10, PROB_1:25;
hence ex A being set st
( A in F & S1[k,A] ) ; :: thesis: verum
end;
end;
end;
hence ex f being set st
( f in F & S1[k,f] ) ; :: thesis: verum
end;
consider Df being Function of NAT ,F such that
A11: for k being set st k in NAT holds
S1[k,Df . k] from FUNCT_2:sch 1(A9);
 A12: for n being Element of NAT
for AD, BD being Element of F st S1[n,AD] & S1[n,BD] holds
AD = BD
proof
let n be Element of NAT ; :: thesis: for AD, BD being Element of F st S1[n,AD] & S1[n,BD] holds
AD = BD
let AD, BD be Element of F; :: thesis: ( S1[n,AD] & S1[n,BD] implies AD = BD )
assume A13: ( S1[n,AD] & S1[n,BD] ) ; :: thesis: AD = BD
now
per cases ( f . n is empty or not f . n is empty ) ;
suppose f . n is empty ; :: thesis: AD = BD
hence AD = BD by A13; :: thesis: verum
end;
suppose not f . n is empty ; :: thesis: AD = BD
then A14: ( AD in f . n & AD in F & BD in f . n & BD in F & f . n is discrete ) by A7, A13, Def2, PROB_1:25;
then consider a being Element of A such that
A15: ( AD = [:{a},A:] \/ [:A,{a}:] & a in A ) ;
consider b being Element of A such that
A16: ( BD = [:{b},A:] \/ [:A,{b}:] & b in A ) by A14;
AD meets BD
proof
( a in {a} & b in {b} ) by TARSKI:def 1;
then ( [a,b] in [:{a},A:] & [a,b] in [:A,{b}:] ) by ZFMISC_1:106;
then ( [a,b] in AD & [a,b] in BD ) by A15, A16, XBOOLE_0:def 3;
hence AD meets BD by XBOOLE_0:3; :: thesis: verum
end;
hence AD = BD by A14, Th6; :: thesis: verum
end;
end;
end;
hence AD = BD ; :: thesis: verum
end;
A17: F c= Df .: NAT
proof
let cAAc be set ; :: according to TARSKI:def 3 :: thesis: ( not cAAc in F or cAAc in Df .: NAT )
assume A18: cAAc in F ; :: thesis: cAAc in Df .: NAT
then consider k being Element of NAT such that
A19: cAAc in f . k by A7, PROB_1:25;
( S1[k,cAAc] & S1[k,Df . k] ) by A11, A19;
then ( cAAc = Df . k & dom Df = NAT ) by A12, A18, FUNCT_2:def 1;
hence cAAc in Df .: NAT by FUNCT_1:def 12; :: thesis: verum
end;
A20: card A c= card F
proof
deffunc H1( set ) -> set = [:{$1},A:] \/ [:A,{$1}:];
consider d being Function such that
A21: ( dom d = A & ( for x being set st x in A holds
d . x = H1(x) ) ) from FUNCT_1:sch 3();
 A22: rng d c= F
proof
let AA be set ; :: according to TARSKI:def 3 :: thesis: ( not AA in rng d or AA in F )
assume AA in rng d ; :: thesis: AA in F
then consider a being set such that
A23: ( a in dom d & AA = d . a ) by FUNCT_1:def 5;
reconsider a = a as Element of A by A21, A23;
AA = [:{a},A:] \/ [:A,{a}:] by A21, A23;
hence AA in F ; :: thesis: verum
end;
for a1, a2 being set st a1 in dom d & a2 in dom d & d . a1 = d . a2 holds
a1 = a2
proof
let a1, a2 be set ; :: thesis: ( a1 in dom d & a2 in dom d & d . a1 = d . a2 implies a1 = a2 )
assume A24: ( a1 in dom d & a2 in dom d & d . a1 = d . a2 ) ; :: thesis: a1 = a2
then A25: ( H1(a1) = d . a1 & H1(a2) = d . a2 ) by A21;
assume A26: a1 <> a2 ; :: thesis: contradiction
( a1 in {a1} & a1 in A ) by A21, A24, ZFMISC_1:37;
then [a1,a1] in [:{a1},A:] by ZFMISC_1:106;
then [a1,a1] in [:{a2},A:] \/ [:A,{a2}:] by A24, A25, XBOOLE_0:def 3;
then ( [a1,a1] in [:{a2},A:] or [a1,a1] in [:A,{a2}:] ) by XBOOLE_0:def 3;
then a1 in {a2} by ZFMISC_1:106;
hence contradiction by A26, TARSKI:def 1; :: thesis: verum
end;
then ( rng d c= F & d is one-to-one & dom d = A ) by A21, A22, FUNCT_1:def 8;
hence card A c= card F by CARD_1:26; :: thesis: verum
end;
not card A c= omega by CARD_3:def 15;
then card NAT in card A by CARD_1:14, CARD_1:84;
then ( card NAT c= card F & card NAT <> card F ) by A20, CARD_1:13;
then ( card (Df .: NAT ) c= card NAT & card NAT c< card F ) by CARD_2:3, XBOOLE_0:def 8;
then card (Df .: NAT ) c< card F by XBOOLE_1:59;
then ( card (Df .: NAT ) c= card F & card (Df .: NAT ) <> card F ) by XBOOLE_0:def 8;
then card (Df .: NAT ) in card F by CARD_1:13;
then F \ (Df .: NAT ) <> {} by CARD_2:4;
hence contradiction by A17, XBOOLE_1:37; :: thesis: verum
end;
hence not F is sigma_discrete ; :: thesis: verum