let C be Cardinal; for T being TopSpace st ( for A being Subset of T st A is discrete holds
card A c= C ) holds
for F being Subset-Family of T st F is open & not {} in F & ( for A, B being Subset of T st A in F & B in F & A <> B holds
A misses B ) holds
card F c= C
let T be TopSpace; ( ( for A being Subset of T st A is discrete holds
card A c= C ) implies for F being Subset-Family of T st F is open & not {} in F & ( for A, B being Subset of T st A in F & B in F & A <> B holds
A misses B ) holds
card F c= C )
assume A1:
for A being Subset of T st A is discrete holds
card A c= C
; for F being Subset-Family of T st F is open & not {} in F & ( for A, B being Subset of T st A in F & B in F & A <> B holds
A misses B ) holds
card F c= C
let F be Subset-Family of T; ( F is open & not {} in F & ( for A, B being Subset of T st A in F & B in F & A <> B holds
A misses B ) implies card F c= C )
assume that
A2:
F is open
and
A3:
not {} in F
and
A4:
for A, B being Subset of T st A in F & B in F & A <> B holds
A misses B
; card F c= C
per cases
( F is empty or not F is empty )
;
suppose A5:
not
F is
empty
;
card F c= Cdeffunc H1(
set )
-> Element of $1 = the
Element of $1;
A6:
for
x being
set st
x in F holds
H1(
x)
in [#] T
consider p being
Function of
F,
([#] T) such that A8:
for
x being
set st
x in F holds
p . x = H1(
x)
from FUNCT_2:sch 11(A6);
reconsider RNG =
rng p as
Subset of
T ;
ex
xx being
object st
xx in F
by A5;
then A9:
not
T is
empty
by A3;
then A10:
dom p = F
by FUNCT_2:def 1;
for
x being
Point of
T st
x in RNG holds
ex
G being
Subset of
T st
(
G is
open &
RNG /\ G = {x} )
proof
let x be
Point of
T;
( x in RNG implies ex G being Subset of T st
( G is open & RNG /\ G = {x} ) )
assume A11:
x in RNG
;
ex G being Subset of T st
( G is open & RNG /\ G = {x} )
then consider G being
object such that A12:
G in F
and A13:
p . G = x
by A10, FUNCT_1:def 3;
reconsider G =
G as
Subset of
T by A12;
A14:
RNG /\ G c= {x}
proof
let y be
object ;
TARSKI:def 3 ( not y in RNG /\ G or y in {x} )
assume A15:
y in RNG /\ G
;
y in {x}
then A16:
y in G
by XBOOLE_0:def 4;
y in RNG
by A15, XBOOLE_0:def 4;
then consider z being
object such that A17:
z in F
and A18:
p . z = y
by A10, FUNCT_1:def 3;
reconsider z =
z as
set by TARSKI:1;
y = H1(
z)
by A8, A17, A18;
then
z meets G
by A3, A16, A17, XBOOLE_0:3;
then
x = y
by A4, A12, A13, A17, A18;
hence
y in {x}
by TARSKI:def 1;
verum
end;
take
G
;
( G is open & RNG /\ G = {x} )
thus
G is
open
by A2, A12;
RNG /\ G = {x}
x = H1(
G)
by A8, A12, A13;
then
x in RNG /\ G
by A3, A11, A12, XBOOLE_0:def 4;
hence
RNG /\ G = {x}
by A14, ZFMISC_1:33;
verum
end; then A19:
card RNG c= C
by A1, A9, TEX_2:31;
for
x1,
x2 being
object st
x1 in dom p &
x2 in dom p &
p . x1 = p . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in dom p & x2 in dom p & p . x1 = p . x2 implies x1 = x2 )
assume that A20:
x1 in dom p
and A21:
x2 in dom p
and A22:
p . x1 = p . x2
;
x1 = x2
reconsider x1 =
x1,
x2 =
x2 as
set by TARSKI:1;
A23:
(
p . x2 = H1(
x2) &
x2 <> {} )
by A3, A8, A21;
(
p . x1 = H1(
x1) &
x1 <> {} )
by A3, A8, A20;
then
x1 meets x2
by A22, A23, XBOOLE_0:3;
hence
x1 = x2
by A4, A10, A20, A21;
verum
end; then
p is
one-to-one
by FUNCT_1:def 4;
then
card F c= card RNG
by A10, CARD_1:10;
hence
card F c= C
by A19;
verum end; end;