environ
vocabularies HIDDEN, XBOOLE_0, PRE_TOPC, RLVECT_3, SUBSET_1, TARSKI, SETFAM_1, RCOMP_1, YELLOW_8, PBOOLE, FUNCT_1, CARD_3, ZFMISC_1, STRUCT_0, RELAT_1, CARD_1, ORDINAL1, FRECHET, WAYBEL23, FINSET_1, EQREL_1, NATTRA_1, CARD_2, CANTOR_1, TOPS_1, FINSUB_1, FINSEQ_1, PCOMPS_1, YELLOW_9, TOPGEN_2;
notations HIDDEN, TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, DOMAIN_1, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, CARD_1, FINSEQ_1, CARD_3, EQREL_1, ORDINAL1, FINSET_1, FINSUB_1, CARD_2, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, TDLAT_3, PCOMPS_1, CANTOR_1, FRECHET, YELLOW_8, YELLOW_9, WAYBEL23;
definitions TARSKI, XBOOLE_0, FUNCT_1, CARD_3, STRUCT_0, PRE_TOPC, FRECHET, YELLOW_8, YELLOW_9;
theorems XBOOLE_1, ZFMISC_1, SETFAM_1, CANTOR_1, CARD_5, YELLOW_8, YELLOW_9, TOPS_1, CARD_1, CARD_4, CARD_LAR, XBOOLE_0, TSEP_1, PRE_TOPC, TARSKI, TOPS_2, FUNCT_1, CARD_3, FINSET_1, TDLAT_3, CARD_2, EQREL_1, FUNCT_2, WELLORD2, WAYBEL23, SUBSET_1, FINSEQ_1, FINSUB_1, WAYBEL19, PCOMPS_1, MSSUBFAM, ENUMSET1, PARTFUN1;
schemes ORDINAL1, PBOOLE, FUNCT_1, FUNCT_2;
registrations SUBSET_1, FINSET_1, CARD_1, EQREL_1, CARD_5, CARD_FIL, STRUCT_0, PRE_TOPC, TOPS_1, TDLAT_3, YELLOW12, ORDINAL1, COMPTS_1, RELSET_1;
constructors HIDDEN, DOMAIN_1, FINSUB_1, CARD_2, TOPS_1, TOPS_2, TDLAT_3, CANTOR_1, YELLOW_8, YELLOW_9, FRECHET, WAYBEL23, RELSET_1, FINSEQ_2, XTUPLE_0;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS;
equalities XBOOLE_0, CARD_3, STRUCT_0, SUBSET_1;
expansions TARSKI, CARD_3, PRE_TOPC;
Lm1:
now for T being non empty TopStruct holds
( union { (Chi (x,T)) where x is Point of T : verum } is cardinal number & ( for m being cardinal number st m = union { (Chi (x,T)) where x is Point of T : verum } holds
( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
m c= M ) ) ) )
let T be non
empty TopStruct ;
( union { (Chi (x,T)) where x is Point of T : verum } is cardinal number & ( for m being cardinal number st m = union { (Chi (x,T)) where x is Point of T : verum } holds
( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
m c= M ) ) ) )set X =
{ (Chi (x,T)) where x is Point of T : verum } ;
hence
union { (Chi (x,T)) where x is Point of T : verum } is
cardinal number
by Th3;
for m being cardinal number st m = union { (Chi (x,T)) where x is Point of T : verum } holds
( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
m c= M ) )let m be
cardinal number ;
( m = union { (Chi (x,T)) where x is Point of T : verum } implies ( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
m c= M ) ) )assume A1:
m = union { (Chi (x,T)) where x is Point of T : verum }
;
( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
m c= M ) )
let M be
cardinal number ;
( ( for x being Point of T holds Chi (x,T) c= M ) implies m c= M )assume A2:
for
x being
Point of
T holds
Chi (
x,
T)
c= M
;
m c= M
now for a being set st a in { (Chi (x,T)) where x is Point of T : verum } holds
a c= M
let a be
set ;
( a in { (Chi (x,T)) where x is Point of T : verum } implies a c= M )assume
a in { (Chi (x,T)) where x is Point of T : verum }
;
a c= Mthen
ex
x being
Point of
T st
a = Chi (
x,
T)
;
hence
a c= M
by A2;
verum
end;
hence
m c= M
by A1, ZFMISC_1:76;
verum
end;
Lm4:
for T being infinite-weight TopSpace
for B being Basis of T ex B1 being Basis of T st
( B1 c= B & card B1 = weight T )
Lm5:
for T being non empty finite-weight TopSpace
for B being Basis of T ex B1 being Basis of T st
( B1 c= B & card B1 = weight T )