:: On Paracompactness of Metrizable Spaces :: by Leszek Borys :: :: Received July 23, 1992 :: Copyright (c) 1992-2012 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, RELAT_1, WELLORD1, RELAT_2, ZFMISC_1, TARSKI, XBOOLE_0, FUNCT_1, FINSEQ_1, PRE_TOPC, METRIC_1, SETFAM_1, CARD_5, RCOMP_1, STRUCT_0, PCOMPS_1, CARD_1, ARYTM_3, XXREAL_0, ORDINAL4, PARTFUN1, NEWTON, NAT_1, REAL_1, FINSET_1, ARYTM_1, PCOMPS_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, REAL_1, TOPS_2, FUNCT_1, PARTFUN1, FUNCT_2, NAT_1, SETFAM_1, STRUCT_0, NEWTON, METRIC_1, PRE_TOPC, PCOMPS_1, WELLORD1, RELAT_1, FINSEQ_1, FINSET_1, RELAT_2, FINSEQ_2, XXREAL_0; constructors SETFAM_1, RELAT_2, WELLORD1, WELLORD2, REAL_1, NAT_1, MEMBERED, NEWTON, TOPS_2, PCOMPS_1, FINSEQ_2; registrations SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, XXREAL_0, NAT_1, MEMBERED, FINSEQ_1, STRUCT_0, PRE_TOPC, METRIC_1, TOPS_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, WELLORD1, RELAT_2, SETFAM_1, XBOOLE_0, STRUCT_0; theorems PCOMPS_1, COMPTS_1, SETFAM_1, TOPS_1, TOPS_2, PRE_TOPC, SUBSET_1, TARSKI, WELLORD2, ZFMISC_1, NAT_1, PREPOWER, WELLORD1, RELAT_1, RELAT_2, FUNCT_1, METRIC_1, FINSEQ_1, CARD_1, FINSEQ_2, FINSEQ_4, TBSP_1, NEWTON, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1; schemes NAT_1, FUNCT_2, SUBSET_1, RECDEF_1, TREES_2, FRAENKEL, XBOOLE_0; begin :: 1. Selected properties of real numbers reserve i for Element of NAT; begin :: 2. Certain functions defined on families of sets reserve R for Relation; reserve A for set; theorem Th1: R well_orders A implies R |_2 A well_orders A & A = field (R |_2 A) proof assume A1: R well_orders A; then A2: R is_reflexive_in A by WELLORD1:def 5; A3: R |_2 A is_reflexive_in A proof let x be set; assume x in A; then [x,x] in R & [x,x] in [:A,A:] by A2,RELAT_2:def 1,ZFMISC_1:87; hence thesis by XBOOLE_0:def 4; end; A4: R |_2 A is_connected_in A proof let x,y be set; assume that A5: x in A & y in A and A6: x <>y; A7: R is_connected_in A by A1,WELLORD1:def 5; now per cases by A5,A6,A7,RELAT_2:def 6; case A8: [x,y] in R; [x,y] in [:A,A:] by A5,ZFMISC_1:87; hence [x,y] in R |_2 A by A8,XBOOLE_0:def 4; end; case A9: [y,x] in R; [y,x] in [:A,A:] by A5,ZFMISC_1:87; hence [y,x] in R |_2 A by A9,XBOOLE_0:def 4; end; end; hence thesis; end; A10: R |_2 A c= R by XBOOLE_1:17; A11: R |_2 A is_antisymmetric_in A proof let x,y be set; assume A12: x in A & y in A & [x,y] in R |_2 A & [y,x] in R |_2 A; R is_antisymmetric_in A by A1,WELLORD1:def 5; hence thesis by A10,A12,RELAT_2:def 4; end; A13: R |_2 A is_well_founded_in A proof let Y be set; assume A14: Y c= A & Y <> {}; R is_well_founded_in A by A1,WELLORD1:def 5; then consider a be set such that A15: a in Y & R-Seg(a) misses Y by A14,WELLORD1:def 3; (R |_2 A)-Seg(a) c= R-Seg(a) by WELLORD1:14; hence thesis by A15,XBOOLE_1:63; end; A16: A c= field (R |_2 A) proof let x be set; assume x in A; then [x,x] in [:A,A:] & [x,x] in R by A2,RELAT_2:def 1,ZFMISC_1:87; then [x,x] in R |_2 A by XBOOLE_0:def 4; hence thesis by RELAT_1:15; end; A17: R |_2 A is_transitive_in A proof let x,y,z be set; assume that A18: x in A and A19: y in A and A20: z in A and A21: [x,y] in R |_2 A & [y,z] in R |_2 A; A22: [x,z] in [:A,A:] by A18,A20,ZFMISC_1:87; R is_transitive_in A by A1,WELLORD1:def 5; then [x,z] in R by A10,A18,A19,A20,A21,RELAT_2:def 8; hence thesis by A22,XBOOLE_0:def 4; end; field (R |_2 A) c= A by WELLORD1:13; hence thesis by A16,A3,A17,A11,A4,A13,WELLORD1:def 5,XBOOLE_0:def 10; end; scheme MinSet{A()->set,R()->Relation,P[set]}: ex X be set st X in A() & P[X] & for Y be set st Y in A() & P[Y] holds [X,Y] in R() provided A1: R() well_orders A() and A2: ex X be set st X in A() & P[X] proof consider Y be set such that A3: for x be set holds x in Y iff x in A() & P[x] from XBOOLE_0:sch 1; A4: ex x be set st x in Y proof consider x be set such that A5: x in A() & P[x] by A2; take x; thus thesis by A3,A5; end; for x be set holds x in Y implies x in A() by A3; then Y c= A() by TARSKI:def 3; then consider X be set such that A6: X in Y and A7: for Z be set st Z in Y holds [X,Z] in R() by A1,A4,WELLORD1:5; A8: for M be set st M in A() & P[M] holds [X,M] in R() proof let M be set; assume M in A() & P[M]; then M in Y by A3; hence thesis by A7; end; X in A() & P[X] by A3,A6; hence thesis by A8; end; definition let FX be set, R be Relation, B be Element of FX; func PartUnion(B,R) equals union (R-Seg(B)); coherence; end; definition let FX be set, R be Relation; func DisjointFam(FX,R) means A in it iff ex B be Element of FX st B in FX & A = B\PartUnion(B,R); existence proof defpred P[set] means ex B be Element of FX st B in FX & $1 = B\PartUnion(B ,R); consider X being set such that A1: for x being set holds x in X iff x in bool union FX & P[x] from XBOOLE_0:sch 1; reconsider X as set; take X; let A; thus A in X implies ex B be Element of FX st B in FX & A = B\PartUnion(B,R ) by A1; assume A2: ex B be Element of FX st B in FX & A = B\PartUnion(B,R); then A c= union FX by XBOOLE_1:109,ZFMISC_1:74; hence thesis by A1,A2; end; uniqueness proof defpred P[set] means ex B be Element of FX st B in FX & $1 = B\PartUnion(B ,R); thus for X1,X2 being set st (for x be set holds x in X1 iff P[x]) & (for x be set holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3; end; end; definition let X be set, n be Element of NAT, f be Function of NAT,bool X; func PartUnionNat(n,f) equals union (f.:(Seg(n)\{n})); coherence; end; begin :: 3. Paracompactness of metrizable spaces reserve PT for non empty TopSpace; reserve PM for MetrSpace; reserve FX,GX,HX for Subset-Family of PT; reserve Y,V,W for Subset of PT; theorem Th2: PT is regular implies for FX st FX is Cover of PT & FX is open ex HX st HX is open & HX is Cover of PT & for V st V in HX ex W st W in FX & Cl V c= W proof assume A1: PT is regular; let FX; assume that A2: FX is Cover of PT and A3: FX is open; defpred P[set] means ex V1 being Subset of PT st V1 = $1 & V1 is open & ex W st W in FX & Cl V1 c= W; consider HX such that A4: for V being Subset of PT holds V in HX iff P[V] from SUBSET_1:sch 3; take HX; for V being Subset of PT st V in HX holds V is open proof let V be Subset of PT; assume V in HX; then ex V1 being Subset of PT st V1 = V & V1 is open & ex W st W in FX & Cl V1 c= W by A4; hence thesis; end; hence HX is open by TOPS_2:def 1; the carrier of PT c= union HX proof let x be set; assume x in the carrier of PT; then reconsider x as Point of PT; consider V being Subset of PT such that A5: x in V and A6: V in FX by A2,PCOMPS_1:3; reconsider V as Subset of PT; now per cases; suppose A7: V`<> {}; V is open by A3,A6,TOPS_2:def 1; then A8: V` is closed; x in V`` by A5; then consider X,Y being Subset of PT such that A9: X is open and A10: Y is open and A11: x in X and A12: V` c= Y and A13: X misses Y by A1,A7,A8,COMPTS_1:def 2; X c= Y` & Y` is closed by A10,A13,SUBSET_1:23; then A14: Cl X c= Y` by TOPS_1:5; Y` c= V by A12,SUBSET_1:17; then Cl X c= V by A14,XBOOLE_1:1; then X in HX by A4,A6,A9; hence x in union HX by A11,TARSKI:def 4; end; suppose A15: V` = {}; consider X being Subset of PT such that A16: X=[#](PT); A17: X is open by A16; V = ({}(PT))` by A15 .= [#](PT) by PRE_TOPC:6; then Cl X = V by A16,TOPS_1:2; then X in HX by A4,A6,A17; hence x in union HX by A16,TARSKI:def 4; end; end; hence thesis; end; hence HX is Cover of PT by SETFAM_1:def 11; let V be Subset of PT; assume V in HX; then ex V1 being Subset of PT st V1 = V & V1 is open & ex W st W in FX & Cl V1 c= W by A4; hence thesis; end; theorem for PT,FX st PT is T_2 & PT is paracompact & FX is Cover of PT & FX is open ex GX st GX is open & GX is Cover of PT & clf GX is_finer_than FX & GX is locally_finite proof let PT,FX; assume that A1: PT is T_2 and A2: PT is paracompact and A3: FX is Cover of PT & FX is open; consider HX such that A4: HX is open & HX is Cover of PT and A5: for V st V in HX ex W st W in FX & Cl V c= W by A1,A2,A3,Th2,PCOMPS_1:24; consider GX such that A6: GX is open & GX is Cover of PT and A7: GX is_finer_than HX and A8: GX is locally_finite by A2,A4,PCOMPS_1:def 3; A9: for V st V in GX ex W st W in FX & (Cl V) c= W proof let V; assume V in GX; then consider X being set such that A10: X in HX and A11: V c= X by A7,SETFAM_1:def 2; reconsider X as Subset of PT by A10; consider W such that A12: W in FX & Cl X c= W by A5,A10; take W; Cl V c= Cl X by A11,PRE_TOPC:19; hence thesis by A12,XBOOLE_1:1; end; clf GX is_finer_than FX proof let X be set; assume A13: X in clf GX; then reconsider X as Subset of PT; consider V such that A14: X = Cl V and A15: V in GX by A13,PCOMPS_1:def 2; consider W such that A16: W in FX & (Cl V) c= W by A9,A15; take W; thus thesis by A14,A16; end; hence thesis by A6,A8; end; theorem Th4: for f being Function of [:the carrier of PT,the carrier of PT:], REAL st f is_metric_of ( the carrier of PT) holds PM = SpaceMetr(the carrier of PT,f) implies the carrier of PM = the carrier of PT proof let f be Function of [:the carrier of PT,the carrier of PT:],REAL; assume A1: f is_metric_of the carrier of PT; assume PM = SpaceMetr(the carrier of PT,f); then PM = MetrStruct(#the carrier of PT,f#) by A1,PCOMPS_1:def 7; hence thesis; end; theorem for f being Function of [:the carrier of PT,the carrier of PT:],REAL st f is_metric_of ( the carrier of PT) holds PM = SpaceMetr(the carrier of PT,f ) implies (FX is Subset-Family of PT iff FX is Subset-Family of PM) by Th4; reserve Mn for Relation; reserve n,k,l,q,p,q1 for Element of NAT; definition let PM be non empty set; let g be Function of NAT,(bool bool PM)*; let n; redefine func g.n -> FinSequence of bool bool PM; coherence proof g.n is Element of (bool bool PM)*; hence g.n is FinSequence of bool bool PM; end; end; scheme XXX1 { PM() -> non empty set, UB() -> Subset-Family of PM(), F(set,set) -> Subset of PM(), P[set], Q[set,set,set,set]} : ex f being Function of NAT, bool bool PM() st f.0 = UB() & for n holds f.(n+1) = {union { F(c,n) where c is Element of PM(): for fq be Subset-Family of PM(),q st q <= n & fq = f.q holds Q [c,V,n,fq] } where V is Subset of PM() : P[V]} proof reconsider A = <*UB()*> as Element of (bool bool PM())* by FINSEQ_1:def 11; defpred T[Element of NAT,FinSequence of bool bool PM(),set] means $3 = $2^<* {union { F(c,$1) where c is Element of PM(): for fq be Subset-Family of PM(),q st q <= $1 & fq = $2/.(q+1) holds Q[c,V,$1,fq] } where V is Subset of PM() : P[ V]}*>; A1: for n being Element of NAT for x being Element of (bool bool PM())* ex y being Element of (bool bool PM())* st T[n,x,y] proof let n; let x be Element of (bool bool PM())*; set T = { union { F(c,n) where c is Element of PM(): for fq be Subset-Family of PM(),q st q <= n & fq = x/.(q+1) holds Q[c,V,n,fq]} where V is Subset of PM() : P[V]}; now let X be set; assume X in T; then consider V be Subset of PM() such that A2: X=union { F(c,n) where c is Element of PM(): for fq be Subset-Family of PM(),q st q <= n & fq = x/.(q+1) holds Q[c,V,n,fq] } and P[V]; now let a be set; assume a in X; then consider P be set such that A3: a in P and A4: P in { F(c,n) where c is Element of PM(): for fq be Subset-Family of PM(),q st q <= n & fq = x/.(q+1) holds Q[c,V,n,fq]} by A2, TARSKI:def 4; ex c be Element of PM() st P = F(c,n) & for fq be Subset-Family of PM(),q st q <= n & fq = x/.(q+1) holds Q[c,V,n,fq] by A4; hence a in PM() by A3; end; then X c= PM() by TARSKI:def 3; hence X in bool PM(); end; then reconsider T as Subset-Family of PM() by TARSKI:def 3; reconsider T1 = <*T*> as FinSequence of bool bool PM(); consider y be FinSequence of bool bool PM() such that A5: y = x^T1; reconsider y as Element of (bool bool PM())* by FINSEQ_1:def 11; take y; thus thesis by A5; end; consider g be Function of NAT,(bool bool PM())* such that A6: g.0=A and A7: for n be Element of NAT holds T[n,g.n,g.(n+1)] from RECDEF_1:sch 2 (A1 ); defpred R[Element of NAT] means len(g.$1) = $1 + 1; A8: for k st R[k] holds R[k+1] proof let k such that A9: len(g.k) = k+1; len(g.(k+1))=len((g.k)^<*{ union { F(c,k) where c is Element of PM(): for fq be Subset-Family of PM(),q st q <= k & fq = (g.k)/.(q+1) holds Q[c,V,k, fq] } where V is Subset of PM() : P[V]}*>) by A7 .= len(g.k)+1 by FINSEQ_2:16; hence thesis by A9; end; deffunc G(Element of NAT) = (g.$1)/.len(g.$1); consider f be Function of NAT,bool bool PM() such that A10: for n holds f.n=G(n) from FUNCT_2:sch 4; take f; len <*UB()*> = 1 by FINSEQ_1:39; hence f.0 = <*UB()*>/.1 by A6,A10 .= UB() by FINSEQ_4:16; let n; defpred T[Element of NAT] means for q st q <= $1 holds f.q = (g.$1)/.(q+1); A11: R[0] by A6,FINSEQ_1:39; A12: for n holds R[n] from NAT_1:sch 1(A11,A8); then A13: len(g.n)+1=n+1+1; A14: for k st T[k] holds T[k+1] proof let k; assume A15: for q st q <= k holds f.q = (g.k)/.(q+1); let q; assume A16: q <= k+1; now per cases by A16,XXREAL_0:1; suppose A17: q = k+1; thus f.q=(g.q)/.len(g.q) by A10 .= (g.(k+1))/.(q+1) by A12,A17; end; suppose A18: q < k+1; A19: q+1>=1 by NAT_1:11; q+1 <= k+1 by A18,NAT_1:13; then A20: q+1 in Seg(k+1) by A19,FINSEQ_1:1; then q+1 in Seg len(g.k) by A12; then A21: q+1 in dom (g.k) by FINSEQ_1:def 3; A22: q <= k by A18,NAT_1:13; k+1+1>=k+1 by NAT_1:11; then Seg(k+1) c= Seg(k+1+1) by FINSEQ_1:5; then q+1 in Seg(k+1+1) by A20; then q+1 in Seg(len(g.(k+1))) by A12; then q+1 in dom(g.(k+1)) by FINSEQ_1:def 3; hence (g.(k+1))/.(q+1) = (g.(k+1)).(q+1) by PARTFUN1:def 6 .= ((g.k)^<*{ union { F(c,k) where c is Element of PM(): for fq be Subset-Family of PM(),q st q <= k & fq = (g.k)/.(q+1) holds Q[c,V,k,fq]} where V is Subset of PM() : P[V]}*>).(q+1) by A7 .= (g.k).(q+1) by A21,FINSEQ_1:def 7 .= (g.k)/.(q+1) by A21,PARTFUN1:def 6 .= f.q by A15,A22; end; end; hence thesis; end; deffunc G2(set) = union { F(c,n) where c is Element of PM(): for fq be Subset-Family of PM(),q st q <= n & fq = (g.n)/.(q+1) holds Q[c,$1,n,fq]}; deffunc F2(set) = union { F(c,n) where c is Element of PM(): for fq be Subset-Family of PM(),q st q <= n & fq = f.q holds Q[c,$1,n,fq]}; set NF = { F2(V) where V is Subset of PM(): P[V] }; len(g.(n+1))= n+1+1 by A12; then A23: dom(g.(n+1)) = Seg(n+1+1) by FINSEQ_1:def 3; A24: T[0] proof let q; assume q <= 0; then A25: q = 0; thus f.q = (g.q)/.len(g.q) by A10 .= (g.0)/.(q+1) by A6,A25,FINSEQ_1:39; end; A26: for n holds T[n] from NAT_1:sch 1(A24,A14); A27: for V be Subset of PM() st P[V] holds F2(V) = G2(V) proof deffunc F1(set) = F($1,n); let V be Subset of PM() such that P[V]; defpred P1[set] means for fq be Subset-Family of PM(),q st q <= n & fq = f .q holds Q[$1,V,n,fq]; defpred P[set] means for fq be Subset-Family of PM(),q st q <= n & fq = (g .n)/.(q+1) holds Q[$1,V,n,fq]; A28: for c be Element of PM() holds P1[c] iff P[c] proof let c be Element of PM(); thus (for fq be Subset-Family of PM(),q st q <= n & fq = f.q holds Q[c,V ,n,fq]) implies for fq be Subset-Family of PM(),q st q <= n & fq = (g.n)/.(q+1) holds Q[c,V,n,fq] proof assume A29: for fq be Subset-Family of PM(),q st q <= n & fq = f.q holds Q[c,V,n,fq]; let fq be Subset-Family of PM(),q; assume that A30: q <= n and A31: fq = (g.n)/.(q+1); fq = f.q by A26,A30,A31; hence thesis by A29,A30; end; assume A32: for fq be Subset-Family of PM(),q st q <= n & fq = (g.n)/.(q+1) holds Q[c,V,n,fq]; let fq be Subset-Family of PM(),q; assume that A33: q <= n and A34: fq = f.q; f.q = (g.n)/.(q+1) by A26,A33; hence thesis by A32,A33,A34; end; { F1(c) where c is Element of PM(): P1[c] } = { F1(c) where c is Element of PM(): P[c] } from FRAENKEL:sch 3 (A28); hence thesis; end; A35: NF = { G2(V) where V is Subset of PM() : P[V] } from FRAENKEL:sch 6(A27 ); then len(g.(n+1))=len((g.n)^<*NF*>) by A7 .= len(g.n)+1 by FINSEQ_2:16; hence f.(n+1) = (g.(n+1))/.(len(g.n)+1) by A10 .= g.(n+1).(len(g.n)+1) by A23,A13,FINSEQ_1:4,PARTFUN1:def 6 .= ((g.n)^<*NF*>).(len(g.n)+1) by A7,A35 .= NF by FINSEQ_1:42; end; scheme XXX { PM() -> non empty set, UB() -> Subset-Family of PM(), F(set,set) -> Subset of PM(), P[set], Q[set,set,set]} : ex f being Function of NAT, bool bool PM() st f.0 = UB() & for n holds f.(n+1) = { union { F(c,n) where c is Element of PM(): Q[c,V,n] & not c in union{union(f.q): q <= n } } where V is Subset of PM() : P[V]} proof defpred Q1[set,set,set,set] means Q[$1,$2,$3] & not $1 in union $4; consider f being Function of NAT, bool bool PM() such that A1: f.0 = UB() and A2: for n holds f.(n+1) = { union { F(c,n) where c is Element of PM(): for fq be Subset-Family of PM(),q st q <= n & fq = f.q holds Q1[c,V,n,fq] } where V is Subset of PM() : P[V]} from XXX1; take f; thus f.0 = UB() by A1; let n; deffunc F2(set) = union { F(c,n) where c is Element of PM(): for fq be Subset-Family of PM(),q st q <= n & fq = f.q holds Q[c,$1,n] & not c in union( fq) }; deffunc G2(set) = union { F(c,n) where c is Element of PM(): Q[c,$1,n] & not c in union{union(f.q): q <= n } }; set fxxx1 = { F2(V) where V is Subset of PM() : P[V] }; set fxxx = { G2(V) where V is Subset of PM() : P[V] }; A3: now deffunc F(set) = F($1,n); let V be Subset of PM(); assume P[V]; defpred P[set] means for fq be Subset-Family of PM(),q st q <= n & fq = f. q holds Q[$1,V,n] & not $1 in union(fq); defpred Q1[set] means Q[$1,V,n] & not $1 in union{union(f.q1): q1 <= n }; A4: now let c be Element of PM(); A5: ( for fq be Subset-Family of PM(),q st q <= n & fq = f.q holds not c in union(fq)) iff not c in union{union(f.q): q <= n } proof thus (for fq be Subset-Family of PM(),q st q <= n & fq = f.q holds not c in union(fq)) implies not c in union{union(f.q): q <= n } proof assume A6: for fq be Subset-Family of PM(),q st q <= n & fq = f.q holds not c in union(fq); assume c in union{union(f.q): q <= n}; then consider C be set such that A7: c in C and A8: C in {union(f.q): q <= n}by TARSKI:def 4; ex q be Element of NAT st C = union(f.q) & q <= n by A8; hence contradiction by A6,A7; end; assume A9: not c in union{union(f.q): q <= n }; let fq be Subset-Family of PM(),q; assume q <= n & fq = f.q; then A10: union(fq) in {union(f.p): p <= n}; assume c in union(fq); hence contradiction by A9,A10,TARSKI:def 4; end; thus P[c] iff Q1[c] proof hereby consider q such that A11: q <= n; assume A12: for fq be Subset-Family of PM(),q st q <= n & fq = f.q holds Q[c,V,n] & not c in union(fq); ex fq be Subset-Family of PM() st fq = f.q; hence Q[c,V,n] by A12,A11; thus not c in union{union(f.p): p <= n } by A5,A12; end; assume Q[c,V,n] & not c in union{union(f.q): q <= n }; hence thesis by A5; end; end; { F(c) where c is Element of PM(): P[c] } = { F(c) where c is Element of PM(): Q1[c] } from FRAENKEL:sch 3(A4); hence F2(V) = G2(V); end; fxxx1 = fxxx from FRAENKEL:sch 6(A3); hence thesis by A2; end; theorem Th6: PT is metrizable implies for FX being Subset-Family of PT st FX is Cover of PT & FX is open ex GX being Subset-Family of PT st GX is open & GX is Cover of PT & GX is_finer_than FX & GX is locally_finite proof assume PT is metrizable; then consider metr being Function of [:the carrier of PT,the carrier of PT:],REAL such that A1: metr is_metric_of (the carrier of PT) and A2: Family_open_set( SpaceMetr (the carrier of PT,metr) ) = the topology of PT by PCOMPS_1:def 8; let FX; consider R such that A3: R well_orders FX by WELLORD2:17; defpred P1[set] means $1 in FX; consider Mn such that A4: Mn = R |_2 FX; assume that A5: FX is Cover of PT and A6: FX is open; consider PM being MetrSpace such that A7: PM = SpaceMetr(the carrier of PT,metr); reconsider PM as non empty MetrSpace by A1,A7,PCOMPS_1:36; deffunc F1(Element of PM,Element of NAT) = Ball($1,1/(2 |^($2+1))); set UB = {union {Ball(c,1/2) where c is Element of PM: c in V\PartUnion(V,Mn ) & Ball(c,3/2) c= V} where V is Subset of PM: V in FX}; UB is Subset-Family of PM proof reconsider UB as set; UB c= bool the carrier of PM proof let x be set; assume x in UB; then consider V be Subset of PM such that A8: x = union {Ball(c,1/2) where c is Element of PM: c in V\ PartUnion(V,Mn) & Ball(c,3/2) c= V} and V in FX; x c= the carrier of PM proof let y be set; assume y in x; then consider W be set such that A9: y in W and A10: W in {Ball(c,1/2) where c is Element of PM: c in V\PartUnion( V,Mn) & Ball(c,3/2) c= V} by A8,TARSKI:def 4; ex c be Element of PM st W = Ball(c,1/2) & c in V\ PartUnion(V,Mn) & Ball(c,3/2) c= V by A10; hence thesis by A9; end; hence thesis; end; hence thesis; end; then reconsider UB as Subset-Family of PM; defpred Q1[Element of PM, Subset of PM,Element of NAT] means $1 in $2\ PartUnion($2,Mn) & Ball($1,3/(2 |^ ($3+1))) c= $2; consider f being Function of NAT, bool bool the carrier of PM such that A11: f.0 = UB and A12: for n holds f.(n+1) = {union { F1(c,n) where c is Element of PM: Q1 [c,V,n] & not c in union{union (f.q): q <= n } } where V is Subset of PM: P1[V] } from XXX; defpred P2[set] means ex n st $1 in f.n; consider GX being Subset-Family of PM such that A13: for X being Subset of PM holds X in GX iff P2[X] from SUBSET_1:sch 3; reconsider GX as Subset-Family of PT by A1,A7,Th4; take GX; A14: for X being Subset of PT st X in GX holds X is open proof let X be Subset of PT; assume A15: X in GX; then reconsider X as Subset of PM; consider n such that A16: X in f.n by A13,A15; now per cases; suppose A17: n=0; thus X in the topology of PT proof consider V be Subset of PM such that A18: X = union {Ball(c,1/2) where c is Element of PM: c in V\ PartUnion(V,Mn) & Ball(c,3/2) c= V} and V in FX by A11,A16,A17; set NF = {Ball(c,1/2) where c is Element of PM: c in V\PartUnion(V, Mn) & Ball(c,3/2) c= V}; NF c= bool the carrier of PM proof let a be set; assume a in NF; then ex c be Element of PM st a = Ball(c,1/2) & c in V\ PartUnion(V ,Mn) & Ball(c,3/2) c= V; hence thesis; end; then reconsider NF as Subset-Family of PM; NF c= Family_open_set(PM) proof let a be set; assume a in NF; then ex c be Element of PM st a = Ball(c,1/2) & c in V\ PartUnion(V ,Mn) & Ball(c,3/2) c= V; hence thesis by PCOMPS_1:29; end; hence thesis by A2,A7,A18,PCOMPS_1:32; end; end; suppose n>0; then consider k being Nat such that A19: n = k + 1 by NAT_1:6; reconsider k as Element of NAT by ORDINAL1:def 12; thus X in the topology of PT proof X in {union { Ball(c,1/(2 |^ (k+1))) where c is Element of PM: c in V\PartUnion(V,Mn) & Ball(c,3/(2 |^ (k+1))) c= V & not c in union{union(f.q ) where q is Element of NAT: q <= k } } where V is Subset of PM: V in FX} by A12,A16,A19; then consider V be Subset of PM such that A20: X = union { Ball(c,1/(2 |^ (k+1))) where c is Element of PM : c in V\PartUnion(V,Mn) & Ball(c,3/(2 |^ (k+1))) c= V & not c in union{union(f .q) where q is Element of NAT: q <= k } } and V in FX; reconsider NF = { Ball(c,1/(2 |^ (k+1))) where c is Element of PM: c in V\PartUnion(V,Mn) & Ball(c,3/(2 |^ (k+1))) c= V & not c in union { union(f.q ) where q is Element of NAT: q <= k } } as set; NF c= bool the carrier of PM proof let a be set; assume a in NF; then ex c be Element of PM st a = Ball(c,1/(2 |^ (k+1))) & c in V\ PartUnion(V,Mn) & Ball(c,3/(2 |^ (k+1))) c= V & not c in union { union(f.l ): l <= k}; hence thesis; end; then reconsider NF as Subset-Family of PM; NF c= Family_open_set(PM) proof let a be set; assume a in NF; then ex c be Element of PM st a = Ball(c,1/(2 |^ (k+1))) & c in V\ PartUnion(V,Mn) & Ball(c,3/(2 |^ (k+1))) c= V & not c in union{union(f.l): l <= k}; hence thesis by PCOMPS_1:29; end; hence thesis by A2,A7,A20,PCOMPS_1:32; end; end; end; hence thesis by PRE_TOPC:def 2; end; hence GX is open by TOPS_2:def 1; A21: Mn well_orders FX by A3,A4,Th1; the carrier of PT c= union GX proof let x be set; defpred P1[set] means x in $1; assume A22: x in the carrier of PT; then reconsider x9=x as Element of PM by A1,A7,Th4; ex G be Subset of PT st x in G & G in FX by A5,A22,PCOMPS_1:3; then A23: ex G be set st G in FX & P1[G]; consider X be set such that A24: X in FX and A25: P1[X] and A26: for Y be set st Y in FX & P1[Y] holds [X,Y] in Mn from MinSet(A21 , A23 ); reconsider X as Subset of PT by A24; X is open by A6,A24,TOPS_2:def 1; then A27: X in Family_open_set(PM) by A2,A7,PRE_TOPC:def 2; reconsider X as Subset of PM by A1,A7,Th4; consider r be Real such that A28: r>0 and A29: Ball(x9,r) c= X by A25,A27,PCOMPS_1:def 4; defpred P2[Nat] means 3/(2 |^ $1) <= r; ex k be Element of NAT st P2[k] by A28,PREPOWER:92; then A30: ex k be Nat st P2[k]; consider k be Nat such that A31: P2[k] and for l be Nat st P2[l] holds k <= l from NAT_1:sch 5(A30 ); 2 |^ (k+1) = 2 |^ k * 2 by NEWTON:6; then 2 |^ k > 0 & 2 |^ (k+1) >= 2 |^ k by PREPOWER:6,XREAL_1:151; then A32: 3/2 |^ (k+1) <= 3/2 |^ k by XREAL_1:118; assume A33: not x in union GX; A34: for V be set,n st V in f.n holds not x in V proof let V be set; let n; assume V in f.n; then V in GX by A13; hence thesis by A33,TARSKI:def 4; end; A35: for n holds not x in union (f.n) proof let n; assume x in union (f.n); then ex V be set st x in V & V in f.n by TARSKI:def 4; hence contradiction by A34; end; A36: k in NAT by ORDINAL1:def 12; now set W = union{ Ball(y,1/(2 |^ (k+1))) where y is Element of PM: y in X\ PartUnion(X,Mn) & Ball(y,3/(2 |^ (k+1))) c= X & not y in union{ union(f.q) where q is Element of NAT: q <= k} }; A37: x in W proof A38: not x9 in union { union(f.q) where q is Element of NAT: q <= k} proof assume x9 in union { union(f.q) where q is Element of NAT: q <= k}; then consider D be set such that A39: x9 in D and A40: D in { union(f.q) where q is Element of NAT: q <= k} by TARSKI:def 4; ex q be Element of NAT st D = union (f.q) & q <= k by A40; hence contradiction by A35,A39; end; not x9 in PartUnion(X,Mn) proof reconsider FX as set; assume x9 in PartUnion(X,Mn); then consider M be set such that A41: x9 in M and A42: M in Mn-Seg(X) by TARSKI:def 4; A43: M <> X by A42,WELLORD1:1; A44: Mn is_antisymmetric_in FX by A21,WELLORD1:def 5; A45: [M,X] in Mn by A42,WELLORD1:1; then M in field Mn by RELAT_1:15; then A46: M in FX by A3,A4,Th1; then [X,M] in Mn by A26,A41; hence contradiction by A24,A43,A45,A46,A44,RELAT_2:def 4; end; then A47: x9 in X\PartUnion(X,Mn) by A25,XBOOLE_0:def 5; consider A be Subset of PM such that A48: A = Ball(x9,1/(2 |^ (k+1))); 0 < 2 |^ (k+1) by PREPOWER:6; then A49: x in A by A48,TBSP_1:11,XREAL_1:139; Ball(x9,3/(2 |^ (k+1))) c= Ball(x9,r) by A31,A32,PCOMPS_1:1,XXREAL_0:2; then Ball(x9,3/(2 |^ (k+1))) c= X by A29,XBOOLE_1:1; then A in { Ball(y,1/(2 |^ (k+1))) where y is Element of PM: y in X\ PartUnion(X,Mn) & Ball(y,3/(2 |^ (k+1))) c= X & not y in union { union(f.q) where q is Element of NAT: q <= k}} by A48,A47,A38; hence thesis by A49,TARSKI:def 4; end; reconsider W as set; W in {union{ Ball(y,1/(2 |^ (k+1))) where y is Element of PM: y in V\PartUnion(V,Mn) & Ball(y,3/(2 |^ (k+1))) c= V & not y in union { union(f.q) where q is Element of NAT: q <= k}} where V is Subset of PM: V in FX} by A24; then W in f.(k+1) by A12,A36; hence ex W be set,l be Element of NAT st W in f.l & x in W by A37; end; hence contradiction by A34; end; hence A50: GX is Cover of PT by SETFAM_1:def 11; for X be set st X in GX ex Y be set st Y in FX & X c= Y proof let X be set; assume A51: X in GX; then reconsider X as Subset of PM; consider n such that A52: X in f.n by A13,A51; now per cases; suppose A53: n=0; thus ex Y be set st Y in FX & X c= Y proof consider V be Subset of PM such that A54: X = union {Ball(c,1/2) where c is Element of PM: c in V\ PartUnion(V,Mn) & Ball(c,3/2) c= V} and A55: V in FX by A11,A52,A53; set NF = {Ball(c,1/2) where c is Element of PM: c in V\PartUnion(V, Mn) & Ball(c,3/2) c= V}; NF c= bool the carrier of PM proof let a be set; assume a in NF; then ex c be Element of PM st a = Ball(c,1/2) & c in V\ PartUnion( V,Mn) & Ball(c,3/2) c= V; hence thesis; end; then reconsider NF as Subset-Family of PM; A56: for W be set st W in NF holds W c= V proof let W be set; assume W in NF; then consider c be Element of PM such that A57: W = Ball(c,1/2) and c in V\PartUnion(V,Mn) and A58: Ball(c,3/2) c= V; Ball(c,1/2) c= Ball(c,3/2) by PCOMPS_1:1; hence thesis by A57,A58,XBOOLE_1:1; end; reconsider V as set; take Y = V; thus Y in FX by A55; thus thesis by A54,A56,ZFMISC_1:76; end; end; suppose n>0; then consider k being Nat such that A59: n = k + 1 by NAT_1:6; reconsider k as Element of NAT by ORDINAL1:def 12; thus ex Y be set st Y in FX & X c= Y proof X in {union { Ball(c,1/(2 |^ (k+1))) where c is Element of PM: c in V\PartUnion(V,Mn) & Ball(c,3/(2 |^ (k+1))) c= V & not c in union { union(f .q) where q is Element of NAT: q <= k}} where V is Subset of PM: V in FX} by A12,A52,A59; then consider V be Subset of PM such that A60: X = union { Ball(c,1/(2 |^ (k+1))) where c is Element of PM: c in V\PartUnion(V,Mn) & Ball(c,3/(2 |^ (k+1))) c= V & not c in union{union (f.q) where q is Element of NAT: q <= k}} and A61: V in FX; reconsider NF = { Ball(c,1/(2 |^ (k+1))) where c is Element of PM: c in V\PartUnion(V,Mn) & Ball(c,3/(2 |^ (k+1))) c= V & not c in union{union(f.q) where q is Element of NAT: q <= k}} as set; NF c= bool the carrier of PM proof let a be set; assume a in NF; then ex c be Element of PM st a = Ball(c,1/(2 |^ (k+1))) & c in V\ PartUnion(V,Mn) & Ball(c,3/(2 |^ (k+1))) c= V & not c in union { union(f .q) where q is Element of NAT: q <= k}; hence thesis; end; then reconsider NF as Subset-Family of PM; A62: for W be set st W in NF holds W c= V proof let W be set; assume W in NF; then consider c be Element of PM such that A63: W = Ball(c,1/(2 |^ (k+1))) and c in V\PartUnion(V,Mn) and A64: Ball(c,3/(2 |^ (k+1))) c= V and not c in union { union(f.q) where q is Element of NAT: q <= k}; Ball(c,1/(2 |^ (k+1))) c= Ball(c,3/(2 |^ (k+1))) by PCOMPS_1:1 ,XREAL_1:72; hence thesis by A63,A64,XBOOLE_1:1; end; reconsider V as set; take Y = V; thus Y in FX by A61; thus thesis by A60,A62,ZFMISC_1:76; end; end; end; hence thesis; end; hence GX is_finer_than FX by SETFAM_1:def 2; for x be Point of PT ex W be Subset of PT st x in W & W is open & { V : V in GX & V meets W } is finite proof let x be Point of PT; reconsider x9=x as Element of PM by A1,A7,Th4; consider X be Subset of PT such that A65: x in X and A66: X in GX by A50,PCOMPS_1:3; reconsider X as Subset of PT; X is open by A14,A66; then X in Family_open_set(PM) by A2,A7,PRE_TOPC:def 2; then consider r be Real such that A67: r>0 and A68: Ball(x9,r) c= X by A65,PCOMPS_1:def 4; consider m be Element of NAT such that A69: 1/(2 |^ m) <= r by A67,PREPOWER:92; defpred P3[set] means X in f.$1; ex n be Element of NAT st P3[n] by A13,A66; then A70: ex n be Nat st P3[n]; consider k be Nat such that A71: P3[k] and for l be Nat st P3[l] holds k <= l from NAT_1:sch 5(A70 ); consider W be Subset of PM such that A72: W = Ball(x9,1/(2 |^ (m+1+k+1))); reconsider W as Subset of PT by A1,A7,Th4; A73: { V : V in GX & V meets W } is finite proof defpred P4[set,set] means $1 in f.$2; set NZ={ V : V in GX & V meets W }; A74: for p be set st p in NZ ex n st P4[p,n] proof let p be set; assume p in NZ; then ex V be Subset of PT st p = V & V in GX & V meets W; hence thesis by A13; end; consider g be Function such that A75: dom g = NZ and A76: for y be set st y in NZ ex n st g.y=n & P4[y,n] & for t be Element of NAT st P4[y,t] holds n <=t from TREES_2:sch 4(A74); A77: rng g c= {i: i < (m+1+k+1)} proof let t be set; assume t in rng g; then consider a be set such that A78: a in dom g and A79: t = g.a by FUNCT_1:def 3; assume A80: not t in {i: i < (m+1+k+1)}; A81: ex n be Element of NAT st g.a = n & a in f.n & for p be Element of NAT st a in f.p holds n <= p by A75,A76,A78; then reconsider t as Element of NAT by A79; consider V such that A82: a=V and V in GX and A83: V meets W by A75,A78; consider y being set such that A84: y in V and A85: y in W by A83,XBOOLE_0:3; A86: t >= (m+1+k+1) by A80; now per cases; suppose t=0; hence contradiction by A80; end; suppose t>0; then consider l be Nat such that A87: t=l+1 by NAT_1:6; reconsider l as Element of NAT by ORDINAL1:def 12; A88: V in {union { Ball(c,1/(2 |^ (l+1))) where c is Element of PM: c in Y\PartUnion(Y,Mn) & Ball(c,3/(2 |^ (l+1))) c= Y & not c in union{union (f.q) where q is Element of NAT: q <= l}} where Y is Subset of PM: Y in FX} by A12,A79,A81,A82,A87; 2 |^ t >= 2 |^ (m+1+k+1) & 2 |^ (m+1+k+1) > 0 by A86,PREPOWER:6,93; then A89: 1/(2 |^ (m+1+k+1)) >= 1/(2 |^ t) by XREAL_1:118; consider Y be Subset of PM such that A90: V = union { Ball(c,1/(2 |^ (l+1))) where c is Element of PM: c in Y\PartUnion(Y,Mn) & Ball(c,3/(2 |^ (l+1))) c= Y & not c in union{union (f.q) where q is Element of NAT: q <= l}} and Y in FX by A88; reconsider NF = { Ball(c,1/(2 |^ (l+1) ) ) where c is Element of PM: c in Y\PartUnion(Y,Mn) & Ball(c,3/(2 |^ (l+1))) c= Y & not c in union{union (f.q) where q is Element of NAT: q <= l}} as set; consider T be set such that A91: y in T and A92: T in NF by A84,A90,TARSKI:def 4; reconsider y as Element of PM by A85; consider c be Element of PM such that A93: T = Ball(c,1/(2 |^ (l+1))) and c in Y\PartUnion(Y,Mn) and Ball(c,3/(2 |^ (l+1))) c= Y and A94: not c in union{union (f.q) where q is Element of NAT: q <= l} by A92; dist(c,y) < 1/(2 |^ t) by A87,A91,A93,METRIC_1:11; then dist(c,y) < 1/(2 |^ (m+1+k+1)) by A89,XXREAL_0:2; then A95: dist(c,y) + dist(y,x9) < 1/(2 |^ (m+1+k+1)) + dist(y,x9) by XREAL_1:6; A96: for t be Element of NAT st t < l holds not c in union(f.t) proof let t be Element of NAT; assume t < l; then A97: union(f.t) in {union(f.q) where q is Element of NAT: q <= l}; assume c in union(f.t); hence contradiction by A94,A97,TARSKI:def 4; end; A98: dist(c,x9) >= 1/(2 |^ m) proof assume not dist(c,x9) >= 1/(2 |^ m); then dist(x9,c) < r by A69,XXREAL_0:2; then c in Ball(x9,r) by METRIC_1:11; then A99: c in union (f.k) by A71,A68,TARSKI:def 4; A100: k <> l proof assume k=l; then union (f.k) in {union(f.q) where q is Element of NAT: q <= l}; hence contradiction by A94,A99,TARSKI:def 4; end; l >= k+(m+1) & k+(m+1)>=k by A86,A87,NAT_1:11,XREAL_1:6; then k <= l by XXREAL_0:2; then k in NAT & k < l by A100,ORDINAL1:def 12,XXREAL_0:1; hence contradiction by A96,A99; end; dist(c,y) + dist(y,x9) >= dist(c,x9) by METRIC_1:4; then dist(c,y) + dist(y,x9) >= 1/(2 |^ m) by A98,XXREAL_0:2; then 1/(2 |^ (m+1+k+1)) + dist(y,x9) > 1/(2 |^ m) by A95,XXREAL_0:2 ; then A101: dist(y,x9) >= 1/(2 |^ m) - 1/(2 |^ (m+1+k+1)) by XREAL_1:19; (2 |^ (1+k))*2>=2 by PREPOWER:11,XREAL_1:151; then A102: ((2 |^ (1+k))*2)-1>=2-1 by XREAL_1:9; 2 |^ (1+k+1) <> 0 by PREPOWER:5; then 1/(2 |^ m) - 1/(2 |^ (m+1+k+1)) = (1*(2 |^ (1+k+1)))/((2 |^ m)*(2 |^ (1+k+1))) - 1/(2 |^ (m+1+k+1)) by XCMPLX_1:91 .= (1*(2 |^ (1+k+1)))/(2 |^ (m+((1+k)+1))) - 1/(2 |^ (m+1+k+1) ) by NEWTON:8 .= ((2 |^ (1+k))*2)/(2 |^ (m+1+k+1)) - 1/(2 |^ (m+1+k+1)) by NEWTON:6 .= (((2 |^ (1+k))*2)-1)/(2 |^ (m+1+k+1)) by XCMPLX_1:120; then 1 /(2 |^ m) - 1/(2 |^ (m+1+k+1)) >= 1/(2 |^ (m+1+k+1)) by A102 ,XREAL_1:72; then dist(y,x9) >= 1/(2 |^ (m+1+k+1)) by A101,XXREAL_0:2; hence contradiction by A72,A85,METRIC_1:11; end; end; hence contradiction; end; for x1,x2 be set st x1 in dom g & x2 in dom g & g.x1 = g.x2 holds x1 = x2 proof let x1,x2 be set; assume that A103: x1 in dom g and A104: x2 in dom g and A105: g.x1 = g.x2; ex V2 be Subset of PT st x2=V2 & V2 in GX & V2 meets W by A75,A104; then consider w2 being set such that A106: w2 in W and A107: w2 in x2 by XBOOLE_0:3; consider n1 be Element of NAT such that A108: g.x1 = n1 and A109: x1 in f.n1 and for t be Element of NAT st x1 in f.t holds n1 <= t by A75,A76,A103; ex V1 be Subset of PT st x1=V1 & V1 in GX & V1 meets W by A75,A103; then consider w1 being set such that A110: w1 in W and A111: w1 in x1 by XBOOLE_0:3; assume A112: x1<>x2; reconsider w1, w2 as Element of PM by A110,A106; A113: ex n2 be Element of NAT st g.x2 = n2 & x2 in f.n2 & for t be Element of NAT st x2 in f.t holds n2 <= t by A75,A76,A104; now per cases; suppose A114: n1=0; m+k+1 >= 1 by NAT_1:11; then 2 |^ (m+1+k) >= 2 |^ 1 by PREPOWER:93; then 2 |^ (m+1+k) >= 2 by NEWTON:5; then A115: 1/(2 |^ (m+1+k)) <= 1/2 by XREAL_1:118; A116: 2/(2 |^ (m+1+k+1)) =(1*2)/(2 |^ (m+1+k)*2) by NEWTON:6 .= 1/(2 |^ (m+1+k)) by XCMPLX_1:91; (1/2 + 1/(2 |^ (m+1+k+1))) + (1/(2 |^ (m+1+k+1)) + 1/2) = (1 +1)/2 + (1/(2 |^ (m+1+k+1)) + 1/(2 |^ (m+1+k+1))) .= 2/2 + 2/(2 |^ (m+1+k+1)) by XCMPLX_1:62; then (1/2 + 1/(2 |^ (m+1+k+1))) + (1/(2 |^ (m+1+k+1)) + 1/2) - 2/ 2 = 1/(2 |^ (m+1+k)) by A116; then A117: (1/2 + 1/(2 |^ (m+1+k+1))) + (1/(2 |^ (m+1+k+1)) + 1/2) <= 2 /2 + 1/2 by A115,XREAL_1:20; A118: Mn is_connected_in FX by A21,WELLORD1:def 5; A119: dist(x9,w2) < 1/(2 |^ (m+1+k+1)) by A72,A106,METRIC_1:11; consider M1 be Subset of PM such that A120: x1 = union {Ball(c,1/2) where c is Element of PM: c in M1\PartUnion(M1,Mn) & Ball(c,3/2) c= M1} and A121: M1 in FX by A11,A109,A114; consider k1 be set such that A122: w1 in k1 and A123: k1 in {Ball(c,1/2) where c is Element of PM: c in M1\ PartUnion(M1,Mn) & Ball(c,3/2) c= M1} by A111,A120,TARSKI:def 4; consider c1 be Element of PM such that A124: k1 = Ball(c1,1/2) and A125: c1 in M1\PartUnion(M1,Mn) and A126: Ball(c1,3/2) c= M1 by A123; A127: dist(c1,w1) < 1/2 by A122,A124,METRIC_1:11; consider M2 be Subset of PM such that A128: x2 = union {Ball(c,1/2) where c is Element of PM: c in M2\PartUnion(M2,Mn) & Ball(c,3/2) c= M2} and A129: M2 in FX by A11,A105,A108,A113,A114; consider k2 be set such that A130: w2 in k2 and A131: k2 in {Ball(c,1/2) where c is Element of PM: c in M2\ PartUnion(M2,Mn) & Ball(c,3/2) c= M2} by A107,A128,TARSKI:def 4; consider c2 be Element of PM such that A132: k2 = Ball(c2,1/2) and A133: c2 in M2\PartUnion(M2,Mn) and A134: Ball(c2,3/2) c= M2 by A131; dist(x9,c2) <= dist(x9,w2) + dist(w2,c2) & dist(c1,x9) <= dist(c1,w1) + dist (w1,x9) by METRIC_1:4; then A135: dist(c1,x9) + dist(x9,c2) <= (dist(c1,w1) + dist(w1,x9)) + ( dist(x9,w2) + dist(w2,c2)) by XREAL_1:7; dist(c1,c2) <= dist(c1,x9) + dist(x9,c2) by METRIC_1:4; then dist(c1,c2) <= dist(c1,w1) + (dist(w1,x9) + (dist(x9,w2) + dist(w2,c2))) by A135,XXREAL_0:2; then dist(c1,c2) - (dist(w1,x9) + (dist(x9,w2) + dist(w2,c2))) <= dist(c1,w1) by XREAL_1:20; then dist(c1,c2) - (dist(w1,x9) + (dist(x9,w2) + dist(w2,c2))) < 1/2 by A127,XXREAL_0:2; then dist(c1,c2) < 1/2 + (dist(w1,x9) + (dist(x9,w2) + dist(w2,c2 ))) by XREAL_1:19; then dist(c1,c2) < dist(w1,x9) + (1/2 + (dist(x9,w2) + dist(w2,c2 ))); then A136: dist(c1,c2) - (1/2 + (dist(x9,w2) + dist(w2,c2))) < dist(w1, x9) by XREAL_1:19; dist(x9,w1) < 1/(2 |^ (m+1+k+1)) by A72,A110,METRIC_1:11; then dist(c1,c2) - (1/2 + (dist(x9,w2) + dist(w2,c2))) < 1/(2 |^ (m+1+k+1)) by A136,XXREAL_0:2; then dist(c1,c2) < 1/(2 |^ (m+1+k+1)) + (1/2 + (dist(x9,w2) + dist(w2,c2))) by XREAL_1:19; then dist(c1,c2) < dist(x9,w2) + (dist(w2,c2) + (1/(2 |^ (m+1+k+1 )) + 1/2)); then dist(c1,c2) - (dist(w2,c2) + (1/(2 |^ (m+1+k+1)) + 1/2)) < dist(x9,w2) by XREAL_1:19; then dist(c1,c2) - (dist(w2,c2) + (1/(2 |^ (m+1+k+1)) + 1/2)) < 1 /(2 |^ (m+1+k+1)) by A119,XXREAL_0:2; then dist(c1,c2) < 1/(2 |^ (m+1+k+1)) + (dist(w2,c2) + (1/(2 |^ ( m+1+k+1)) + 1/2)) by XREAL_1:19; then dist(c1,c2) < dist(w2,c2) + (1/(2 |^ (m+1+k+1)) + (1/(2 |^ ( m+1+k+1)) + 1/2)); then A137: dist(c1,c2) - (1/(2 |^ (m+1+k+1)) + (1/(2 |^ (m+1+k+1)) + 1/ 2)) < dist(w2,c2) by XREAL_1:19; dist(c2,w2) < 1/2 by A130,A132,METRIC_1:11; then dist(c1,c2) - (1/(2 |^ (m+1+k+1)) + (1/(2 |^ (m+1+k+1)) + 1/ 2)) < 1/2 by A137,XXREAL_0:2; then dist(c1,c2) < 1/2 + (1/(2 |^ (m+1+k+1)) + (1/(2 |^ (m+1+k+1) ) + 1/2)) by XREAL_1:19; then A138: dist(c1,c2) < 3/2 by A117,XXREAL_0:2; then A139: c1 in Ball(c2,3/2) by METRIC_1:11; A140: M1 <> M2 by A112,A120,A128; A141: c2 in Ball(c1,3/2) by A138,METRIC_1:11; now per cases by A121,A129,A118,A140,RELAT_2:def 6; suppose [M1,M2] in Mn; then M1 in Mn-Seg(M2) by A140,WELLORD1:1; then c2 in PartUnion(M2,Mn) by A126,A141,TARSKI:def 4; hence contradiction by A133,XBOOLE_0:def 5; end; suppose [M2,M1] in Mn; then M2 in Mn-Seg(M1) by A140,WELLORD1:1; then c1 in PartUnion(M1,Mn) by A134,A139,TARSKI:def 4; hence contradiction by A125,XBOOLE_0:def 5; end; end; hence contradiction; end; suppose n1>0; then consider l be Nat such that A142: n1 = l+1 by NAT_1:6; reconsider l as Element of NAT by ORDINAL1:def 12; A143: x1 in {union {Ball(c,1/(2 |^ (l+1))) where c is Element of PM: c in M1\PartUnion(M1,Mn) & Ball(c,3/(2 |^ (l+1))) c= M1 & not c in union { union(f.q) where q is Element of NAT: q <= l}} where M1 is Subset of PM: M1 in FX} by A12,A109,A142; A144: dist(x9,w2) < 1/(2 |^ (m+1+k+1)) by A72,A106,METRIC_1:11; A145: x2 in {union {Ball(c,1/(2 |^ (l+1))) where c is Element of PM: c in M2\PartUnion(M2,Mn) & Ball(c,3/(2 |^ (l+1))) c= M2 & not c in union { union(f.q) where q is Element of NAT: q <= l}} where M2 is Subset of PM: M2 in FX} by A12,A105,A108,A113,A142; A146: (1/(2 |^ (l+1)) + 1/(2 |^ (m+1+k+1))) + (1/(2 |^ (m+1+k+1)) + 1/(2 |^ (l+1))) = (1/(2 |^ (l+1)) + 1/(2 |^ (l+1))) + (1/(2 |^ (m+1+k+1)) + 1 /(2 |^ (m+1+k+1))) .= (1+1)/(2 |^ (l+1)) + (1/(2 |^ (m+1+k+1)) + 1/(2 |^ (m+1+k+1 ))) by XCMPLX_1:62 .= 2/(2 |^ (l+1)) + 2/(2 |^ (m+1+k+1)) by XCMPLX_1:62; n1 in rng g by A103,A108,FUNCT_1:def 3; then n1 in {i: i 0 by A142,A147,A148; then consider i be Nat such that A149: h = i + 1 by NAT_1:6; (l+1)+i >= l+1 by NAT_1:11; then 2 |^ (l+1) > 0 & 2 |^ ((l+1)+i) >= 2 |^ (l+1) by PREPOWER:6,93 ; then A150: 1/(2 |^ ((l+1)+i)) <= 1/(2 |^ (l+1)) by XREAL_1:118; 2/(2 |^ (m+1+k+1)) = (1*2)/(2 |^ ((l+1)+i)*2) by A148,A149,NEWTON:6 .= 1/(2 |^ ((l+1)+i)) by XCMPLX_1:91; then (1/(2 |^ (l+1)) + 1/(2 |^ (m+1+k+1))) + (1/(2 |^ (m+1+k+1)) + 1/(2 |^ (l+1))) - 2/(2 |^ (l+1)) = 1/(2 |^ ((l+1)+i)) by A146; then (1/(2 |^ (l+1)) + 1/(2 |^ (m+1+k+1))) + (1/(2 |^ (m+1+k+1)) + 1/(2 |^ (l+1))) <= 2/(2 |^ (l+1)) + 1/(2 |^ (l+1)) by A150,XREAL_1:20; then A151: (1/(2 |^ (l+1)) + 1/(2 |^ (m+1+k+1))) + (1/(2 |^ (m+1+k+1)) + 1/(2 |^ (l+1))) <= (2+1)/(2 |^ (l+1)) by XCMPLX_1:62; A152: Mn is_connected_in FX by A21,WELLORD1:def 5; consider M1 be Subset of PM such that A153: x1 = union {Ball(c,1/(2 |^ (l+1))) where c is Element of PM: c in M1\PartUnion(M1,Mn) & Ball(c,3/(2 |^ (l+1))) c= M1 & not c in union { union(f.q) where q is Element of NAT: q <= l}} and A154: M1 in FX by A143; reconsider NF = {Ball(c,1/(2 |^ (l+1))) where c is Element of PM: c in M1\PartUnion(M1,Mn) & Ball(c,3/(2 |^ (l+1))) c= M1 & not c in union { union(f.q) where q is Element of NAT: q <= l}} as set; consider k1 be set such that A155: w1 in k1 and A156: k1 in NF by A111,A153,TARSKI:def 4; consider c1 be Element of PM such that A157: k1 = Ball(c1,1/(2 |^ (l+1))) and A158: c1 in M1\PartUnion(M1,Mn) and A159: Ball(c1,3/(2 |^ (l+1))) c= M1 and not c1 in union { union(f.q) where q is Element of NAT: q <= l } by A156; A160: dist(c1,w1) < 1/(2 |^ (l+1)) by A155,A157,METRIC_1:11; consider M2 be Subset of PM such that A161: x2 = union {Ball(c,1/(2 |^ (l+1))) where c is Element of PM: c in M2\PartUnion(M2,Mn) & Ball(c,3/(2 |^ (l+1))) c= M2 & not c in union { union(f.q) where q is Element of NAT: q <= l}} and A162: M2 in FX by A145; A163: M1 <> M2 by A112,A153,A161; reconsider NF = {Ball(c,1/(2 |^ (l+1))) where c is Element of PM: c in M2\PartUnion(M2,Mn) & Ball(c,3/(2 |^ (l+1))) c= M2 & not c in union { union(f.q) where q is Element of NAT: q <= l}} as set; consider k2 be set such that A164: w2 in k2 and A165: k2 in NF by A107,A161,TARSKI:def 4; consider c2 be Element of PM such that A166: k2 = Ball(c2,1/(2 |^ (l+1))) and A167: c2 in M2\PartUnion(M2,Mn) and A168: Ball(c2,3/(2 |^ (l+1))) c= M2 and not c2 in union { union(f.q) where q is Element of NAT: q <= l } by A165; dist(x9,c2) <= dist(x9,w2) + dist(w2,c2) & dist(c1,x9) <= dist(c1,w1) + dist (w1,x9) by METRIC_1:4; then A169: dist(c1,x9) + dist(x9,c2) <= (dist(c1,w1) + dist(w1,x9)) + ( dist(x9,w2) + dist(w2,c2)) by XREAL_1:7; dist(c1,c2) <= dist(c1,x9) + dist(x9,c2) by METRIC_1:4; then dist(c1,c2) <= dist(c1,w1) + (dist(w1,x9) + (dist(x9,w2) + dist(w2,c2))) by A169,XXREAL_0:2; then dist(c1,c2) - (dist(w1,x9) + (dist(x9,w2) + dist(w2,c2))) <= dist(c1,w1) by XREAL_1:20; then dist(c1,c2) - (dist(w1,x9) + (dist(x9,w2) + dist(w2,c2))) < 1/(2 |^ (l+1)) by A160,XXREAL_0:2; then dist(c1,c2) < 1/(2 |^ (l+1)) + (dist(w1,x9) + (dist(x9,w2) + dist(w2,c2))) by XREAL_1:19; then dist(c1,c2) < dist(w1,x9) + (1/(2 |^ (l+1)) + (dist(x9,w2) + dist(w2,c2))); then A170: dist(c1,c2) - (1/(2 |^ (l+1)) + (dist(x9,w2) + dist(w2,c2))) < dist(w1,x9) by XREAL_1:19; dist(x9,w1) < 1/(2 |^ (m+1+k+1)) by A72,A110,METRIC_1:11; then dist(c1,c2) - (1/(2 |^ (l+1)) + (dist(x9,w2) + dist(w2,c2))) < 1/(2 |^ (m+1+k+1)) by A170,XXREAL_0:2; then dist(c1,c2) < 1/(2 |^ (m+1+k+1)) + (1/(2 |^ (l+1)) + (dist( x9,w2) + dist(w2,c2))) by XREAL_1:19; then dist(c1,c2) < dist(x9,w2) + (dist(w2,c2) + (1/(2 |^ (m+1+k+1 )) + 1/(2 |^ (l+1)))); then dist(c1,c2) - (dist(w2,c2) + (1/(2 |^ (m+1+k+1)) + 1/(2 |^ ( l+1)))) < dist(x9,w2) by XREAL_1:19; then dist(c1,c2) - (dist(w2,c2) + (1/(2 |^ (m+1+k+1)) + 1/(2 |^ ( l+1)))) < 1/(2 |^ (m+1+k+1)) by A144,XXREAL_0:2; then dist(c1,c2) < 1/(2 |^ (m+1+k+1)) + (dist(w2,c2) + (1/(2 |^ ( m+1+k+1)) + 1/(2 |^ (l+1)))) by XREAL_1:19; then dist(c1,c2) < dist(w2,c2) + (1/(2 |^ (m+1+k+1)) + (1/(2 |^ ( m+1+k+1)) + 1/(2 |^ (l+1)))); then A171: dist(c1,c2) - (1/(2 |^ (m+1+k+1)) + (1/(2 |^ (m+1+k+1)) + 1/ (2 |^ (l+1)))) < dist(w2,c2) by XREAL_1:19; dist(c2,w2) < 1/(2 |^ (l+1)) by A164,A166,METRIC_1:11; then dist(c1,c2) - (1/(2 |^ (m+1+k+1)) + (1/(2 |^ (m+1+k+1)) + 1/ (2 |^ (l+1)))) < 1/(2 |^ (l+1)) by A171,XXREAL_0:2; then dist(c1,c2) < 1/(2 |^ (l+1)) + (1/(2 |^ (m+1+k+1)) + (1/(2 |^ (m+1+k+1)) + 1/(2 |^ (l+1)))) by XREAL_1:19; then A172: dist(c1,c2) < 3/(2 |^ (l+1)) by A151,XXREAL_0:2; then A173: c1 in Ball(c2,3/(2 |^ (l+1))) by METRIC_1:11; A174: c2 in Ball(c1,3/(2 |^ (l+1))) by A172,METRIC_1:11; now per cases by A154,A162,A152,A163,RELAT_2:def 6; suppose [M1,M2] in Mn; then M1 in Mn-Seg(M2) by A163,WELLORD1:1; then c2 in PartUnion(M2,Mn) by A159,A174,TARSKI:def 4; hence contradiction by A167,XBOOLE_0:def 5; end; suppose [M2,M1] in Mn; then M2 in Mn-Seg(M1) by A163,WELLORD1:1; then c1 in PartUnion(M1,Mn) by A168,A173,TARSKI:def 4; hence contradiction by A158,XBOOLE_0:def 5; end; end; hence contradiction; end; end; hence contradiction; end; then g is one-to-one by FUNCT_1:def 4; then A175: NZ,rng g are_equipotent by A75,WELLORD2:def 4; {i: i < m+1+k+1 } is finite proof {i: i < m+1+k+1 } c= {0} \/ Seg(m+1+k+1) proof let x be set; assume x in {i: i < m+1+k+1}; then A176: ex i be Element of NAT st x = i & i < (m+1+k+1); then reconsider x1=x as Element of NAT; now per cases; suppose x1 = 0; hence x1 in {0} or x1 in Seg(m+1+k+1) by TARSKI:def 1; end; suppose x1 > 0; then ex l be Nat st x1 = l +1 by NAT_1:6; then x1 >= 1 by NAT_1:11; hence x1 in {0} or x1 in Seg(m+1+k+1) by A176,FINSEQ_1:1; end; end; hence thesis by XBOOLE_0:def 3; end; hence thesis; end; hence thesis by A77,A175,CARD_1:38; end; 2 |^ (m+1+k+1) > 0 by PREPOWER:6; then A177: 1/(2 |^ (m+1+k+1)) > 0 by XREAL_1:139; W in the topology of PT by A2,A7,A72,PCOMPS_1:29; then W is open by PRE_TOPC:def 2; hence thesis by A177,A72,A73,TBSP_1:11; end; hence GX is locally_finite by PCOMPS_1:def 1; end; theorem :: Stone Theorem PT is metrizable implies PT is paracompact proof assume PT is metrizable; then for FX being Subset-Family of PT st FX is Cover of PT & FX is open ex GX being Subset-Family of PT st GX is open & GX is Cover of PT & GX is_finer_than FX & GX is locally_finite by Th6; hence thesis by PCOMPS_1:def 3; end;