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:]

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 )

not F is sigma_discrete

( 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

then reconsider F = { ([:{a},A:] \/ [:A,{a}:]) where a is Element of A : a in A } as Subset-Family of (1TopSp [:A,A:]) ;
let f be object ; :: 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}:] and

a in A ;

( [:{a},A:] c= [:A,A:] & [:A,{a}:] c= [:A,A:] ) by ZFMISC_1:96;

then [:{a},A:] \/ [:A,{a}:] c= [:A,A:] by XBOOLE_1:8;

hence f in bool [:A,A:] by A1; :: thesis: verum

end;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}:] and

a in A ;

( [:{a},A:] c= [:A,A:] & [:A,{a}:] c= [:A,A:] ) by ZFMISC_1:96;

then [:{a},A:] \/ [:A,{a}:] c= [:A,A:] by XBOOLE_1:8;

hence f in bool [:A,A:] by A1; :: thesis: verum

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

hence
F is locally_finite
; :: thesis: not F is sigma_discrete
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:]) ;

consider x, y being object such that

x in A and

y in A and

A2: z = [x,y] by ZFMISC_1:def 2;

set yAAy = {([:{y},A:] \/ [:A,{y}:])};

set xAAx = {([:{x},A:] \/ [:A,{x}:])};

set UZ = { O where O is Subset of (1TopSp [:A,A:]) : ( O in F & O meets Z ) } ;

A3: { O where O is Subset of (1TopSp [:A,A:]) : ( O in F & O meets Z ) } c= {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])}

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 A3; :: thesis: verum

end;( 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:]) ;

consider x, y being object such that

x in A and

y in A and

A2: z = [x,y] by ZFMISC_1:def 2;

set yAAy = {([:{y},A:] \/ [:A,{y}:])};

set xAAx = {([:{x},A:] \/ [:A,{x}:])};

set UZ = { O where O is Subset of (1TopSp [:A,A:]) : ( O in F & O meets Z ) } ;

A3: { 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

( z in Z & Z is open )
by PRE_TOPC:def 2, ZFMISC_1:31;
let U be object ; :: 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 and

A5: O in F and

A6: O meets Z ;

consider u being object such that

A7: u in O and

A8: u in Z by A6, XBOOLE_0:3;

consider a being Element of A such that

A9: O = [:{a},A:] \/ [:A,{a}:] and

a in A by A5;

end;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 and

A5: O in F and

A6: O meets Z ;

consider u being object such that

A7: u in O and

A8: u in Z by A6, XBOOLE_0:3;

consider a being Element of A such that

A9: O = [:{a},A:] \/ [:A,{a}:] and

a in A by A5;

now :: thesis: O in {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])}end;

hence
U in {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])}
by A4; :: thesis: verumper cases
( u in [:{a},A:] or u in [:A,{a}:] )
by A9, A7, XBOOLE_0:def 3;

end;

suppose
u in [:{a},A:]
; :: thesis: O in {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])}

then
[x,y] in [:{a},A:]
by A2, A8, TARSKI:def 1;

then x in {a} by ZFMISC_1:87;

then x = a by TARSKI:def 1;

then O in {([:{x},A:] \/ [:A,{x}:])} by A9, TARSKI:def 1;

hence O in {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])} by XBOOLE_0:def 3; :: thesis: verum

end;then x in {a} by ZFMISC_1:87;

then x = a by TARSKI:def 1;

then O in {([:{x},A:] \/ [:A,{x}:])} by A9, TARSKI:def 1;

hence O in {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])} by XBOOLE_0:def 3; :: thesis: verum

suppose
u in [:A,{a}:]
; :: thesis: O in {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])}

then
[x,y] in [:A,{a}:]
by A2, A8, TARSKI:def 1;

then y in {a} by ZFMISC_1:87;

then y = a by TARSKI:def 1;

then O in {([:{y},A:] \/ [:A,{y}:])} by A9, TARSKI:def 1;

hence O in {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])} by XBOOLE_0:def 3; :: thesis: verum

end;then y in {a} by ZFMISC_1:87;

then y = a by TARSKI:def 1;

then O in {([:{y},A:] \/ [:A,{y}:])} by A9, TARSKI:def 1;

hence O in {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])} by XBOOLE_0:def 3; :: thesis: verum

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 A3; :: thesis: verum

not F is sigma_discrete

proof

hence
not F is sigma_discrete
; :: thesis: verum
consider a being object such that

A10: a in A by XBOOLE_0:def 1;

reconsider a = a as Element of A by A10;

set aAAa = [:{a},A:] \/ [:A,{a}:];

A11: card A c= card F

then consider f being sigma_discrete FamilySequence of (1TopSp [:A,A:]) such that

A21: F = Union f ;

defpred S_{1}[ object , object ] means ( ( $2 in f . $1 & not f . $1 is empty ) or ( $2 = [:{a},A:] \/ [:A,{a}:] & f . $1 is empty ) );

A22: for k being object st k in NAT holds

ex f being object st

( f in F & S_{1}[k,f] )

A25: for k being object st k in NAT holds

S_{1}[k,Df . k]
from FUNCT_2:sch 1(A22);

A26: for n being Element of NAT

for AD, BD being Element of F st S_{1}[n,AD] & S_{1}[n,BD] holds

AD = BD

then card NAT in card A by CARD_1:4, CARD_1:47;

then card NAT c= card F by A11, CARD_1:3;

then card NAT c< card F by A11, A38, CARD_1:47, XBOOLE_0:def 8;

then A39: card (Df .: NAT) c< card F by CARD_1:67, XBOOLE_1:59;

then card (Df .: NAT) c= card F by XBOOLE_0:def 8;

then card (Df .: NAT) in card F by A39, CARD_1:3;

then F \ (Df .: NAT) <> {} by CARD_1:68;

hence contradiction by A33, XBOOLE_1:37; :: thesis: verum

end;A10: a in A by XBOOLE_0:def 1;

reconsider a = a as Element of A by A10;

set aAAa = [:{a},A:] \/ [:A,{a}:];

A11: card A c= card F

proof

assume
F is sigma_discrete
; :: thesis: contradiction
deffunc H_{1}( object ) -> set = [:{$1},A:] \/ [:A,{$1}:];

consider d being Function such that

A12: ( dom d = A & ( for x being object st x in A holds

d . x = H_{1}(x) ) )
from FUNCT_1:sch 3();

for a1, a2 being object st a1 in dom d & a2 in dom d & d . a1 = d . a2 holds

a1 = a2

rng d c= F

end;consider d being Function such that

A12: ( dom d = A & ( for x being object st x in A holds

d . x = H

for a1, a2 being object st a1 in dom d & a2 in dom d & d . a1 = d . a2 holds

a1 = a2

proof

then A18:
d is one-to-one
by FUNCT_1:def 4;
let a1, a2 be object ; :: thesis: ( a1 in dom d & a2 in dom d & d . a1 = d . a2 implies a1 = a2 )

assume that

A13: a1 in dom d and

A14: a2 in dom d and

A15: d . a1 = d . a2 ; :: thesis: a1 = a2

a1 in {a1} by ZFMISC_1:31;

then A16: [a1,a1] in [:{a1},A:] by A12, A13, ZFMISC_1:87;

( H_{1}(a1) = d . a1 & H_{1}(a2) = d . a2 )
by A12, A13, A14;

then [a1,a1] in [:{a2},A:] \/ [:A,{a2}:] by A15, A16, XBOOLE_0:def 3;

then ( [a1,a1] in [:{a2},A:] or [a1,a1] in [:A,{a2}:] ) by XBOOLE_0:def 3;

then A17: a1 in {a2} by ZFMISC_1:87;

assume a1 <> a2 ; :: thesis: contradiction

hence contradiction by A17, TARSKI:def 1; :: thesis: verum

end;assume that

A13: a1 in dom d and

A14: a2 in dom d and

A15: d . a1 = d . a2 ; :: thesis: a1 = a2

a1 in {a1} by ZFMISC_1:31;

then A16: [a1,a1] in [:{a1},A:] by A12, A13, ZFMISC_1:87;

( H

then [a1,a1] in [:{a2},A:] \/ [:A,{a2}:] by A15, A16, XBOOLE_0:def 3;

then ( [a1,a1] in [:{a2},A:] or [a1,a1] in [:A,{a2}:] ) by XBOOLE_0:def 3;

then A17: a1 in {a2} by ZFMISC_1:87;

assume a1 <> a2 ; :: thesis: contradiction

hence contradiction by A17, TARSKI:def 1; :: thesis: verum

rng d c= F

proof

hence
card A c= card F
by A12, A18, CARD_1:10; :: thesis: verum
let AA be object ; :: 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 object such that

A19: a in dom d and

A20: AA = d . a by FUNCT_1:def 3;

reconsider a = a as Element of A by A12, A19;

AA = [:{a},A:] \/ [:A,{a}:] by A12, A20;

hence AA in F ; :: thesis: verum

end;assume AA in rng d ; :: thesis: AA in F

then consider a being object such that

A19: a in dom d and

A20: AA = d . a by FUNCT_1:def 3;

reconsider a = a as Element of A by A12, A19;

AA = [:{a},A:] \/ [:A,{a}:] by A12, A20;

hence AA in F ; :: thesis: verum

then consider f being sigma_discrete FamilySequence of (1TopSp [:A,A:]) such that

A21: F = Union f ;

defpred S

A22: for k being object st k in NAT holds

ex f being object st

( f in F & S

proof

consider Df being sequence of F such that
let k be object ; :: thesis: ( k in NAT implies ex f being object st

( f in F & S_{1}[k,f] ) )

assume k in NAT ; :: thesis: ex f being object st

( f in F & S_{1}[k,f] )

then reconsider k = k as Element of NAT ;

( f in F & S_{1}[k,f] )
; :: thesis: verum

end;( f in F & S

assume k in NAT ; :: thesis: ex f being object st

( f in F & S

then reconsider k = k as Element of NAT ;

now :: thesis: ex A being set st

( A in F & S_{1}[k,A] )

hence
ex f being object st ( A in F & S

end;

( f in F & S

A25: for k being object st k in NAT holds

S

A26: for n being Element of NAT

for AD, BD being Element of F st S

AD = BD

proof

A33:
F c= Df .: NAT
let n be Element of NAT ; :: thesis: for AD, BD being Element of F st S_{1}[n,AD] & S_{1}[n,BD] holds

AD = BD

let AD, BD be Element of F; :: thesis: ( S_{1}[n,AD] & S_{1}[n,BD] implies AD = BD )

assume that

A27: S_{1}[n,AD]
and

A28: S_{1}[n,BD]
; :: thesis: AD = BD

end;AD = BD

let AD, BD be Element of F; :: thesis: ( S

assume that

A27: S

A28: S

now :: thesis: AD = BD

hence
AD = BD
; :: thesis: verumA29:
f . n is discrete
by Def2;

BD in F by A21, A28, PROB_1:12;

then consider b being Element of A such that

A30: BD = [:{b},A:] \/ [:A,{b}:] and

b in A ;

AD in F by A21, A27, PROB_1:12;

then consider a being Element of A such that

A31: AD = [:{a},A:] \/ [:A,{a}:] and

a in A ;

b in {b} by TARSKI:def 1;

then [a,b] in [:A,{b}:] by ZFMISC_1:87;

then A32: [a,b] in BD by A30, XBOOLE_0:def 3;

a in {a} by TARSKI:def 1;

then [a,b] in [:{a},A:] by ZFMISC_1:87;

then [a,b] in AD by A31, XBOOLE_0:def 3;

then AD meets BD by A32, XBOOLE_0:3;

hence AD = BD by A27, A28, A29, Th6; :: thesis: verum

end;BD in F by A21, A28, PROB_1:12;

then consider b being Element of A such that

A30: BD = [:{b},A:] \/ [:A,{b}:] and

b in A ;

AD in F by A21, A27, PROB_1:12;

then consider a being Element of A such that

A31: AD = [:{a},A:] \/ [:A,{a}:] and

a in A ;

b in {b} by TARSKI:def 1;

then [a,b] in [:A,{b}:] by ZFMISC_1:87;

then A32: [a,b] in BD by A30, XBOOLE_0:def 3;

a in {a} by TARSKI:def 1;

then [a,b] in [:{a},A:] by ZFMISC_1:87;

then [a,b] in AD by A31, XBOOLE_0:def 3;

then AD meets BD by A32, XBOOLE_0:3;

hence AD = BD by A27, A28, A29, Th6; :: thesis: verum

proof

A38:
not card A c= omega
by CARD_3:def 14;
let cAAc be object ; :: according to TARSKI:def 3 :: thesis: ( not cAAc in F or cAAc in Df .: NAT )

assume A34: cAAc in F ; :: thesis: cAAc in Df .: NAT

then consider k being Nat such that

A35: cAAc in f . k by A21, PROB_1:12;

A36: k in NAT by ORDINAL1:def 12;

S_{1}[k,Df . k]
by A25, A36;

then A37: cAAc = Df . k by A26, A34, A35, A36;

dom Df = NAT by A34, FUNCT_2:def 1;

hence cAAc in Df .: NAT by A37, FUNCT_1:def 6, A36; :: thesis: verum

end;assume A34: cAAc in F ; :: thesis: cAAc in Df .: NAT

then consider k being Nat such that

A35: cAAc in f . k by A21, PROB_1:12;

A36: k in NAT by ORDINAL1:def 12;

S

then A37: cAAc = Df . k by A26, A34, A35, A36;

dom Df = NAT by A34, FUNCT_2:def 1;

hence cAAc in Df .: NAT by A37, FUNCT_1:def 6, A36; :: thesis: verum

then card NAT in card A by CARD_1:4, CARD_1:47;

then card NAT c= card F by A11, CARD_1:3;

then card NAT c< card F by A11, A38, CARD_1:47, XBOOLE_0:def 8;

then A39: card (Df .: NAT) c< card F by CARD_1:67, XBOOLE_1:59;

then card (Df .: NAT) c= card F by XBOOLE_0:def 8;

then card (Df .: NAT) in card F by A39, CARD_1:3;

then F \ (Df .: NAT) <> {} by CARD_1:68;

hence contradiction by A33, XBOOLE_1:37; :: thesis: verum