:: CANTOR_1 semantic presentation begin definition let X be set ; let A be Subset-Family of X; func UniCl A -> Subset-Family of X means :Def1: :: CANTOR_1:def 1 for x being Subset of X holds ( x in it iff ex Y being Subset-Family of X st ( Y c= A & x = union Y ) ); existence ex b1 being Subset-Family of X st for x being Subset of X holds ( x in b1 iff ex Y being Subset-Family of X st ( Y c= A & x = union Y ) ) proof defpred S1[ set ] means ex Y being Subset-Family of X st ( Y c= A & \$1 = union Y ); ex Z being Subset-Family of X st for x being Subset of X holds ( x in Z iff S1[x] ) from SUBSET_1:sch_3(); hence ex b1 being Subset-Family of X st for x being Subset of X holds ( x in b1 iff ex Y being Subset-Family of X st ( Y c= A & x = union Y ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Subset-Family of X st ( for x being Subset of X holds ( x in b1 iff ex Y being Subset-Family of X st ( Y c= A & x = union Y ) ) ) & ( for x being Subset of X holds ( x in b2 iff ex Y being Subset-Family of X st ( Y c= A & x = union Y ) ) ) holds b1 = b2 proof let F1, F2 be Subset-Family of X; ::_thesis: ( ( for x being Subset of X holds ( x in F1 iff ex Y being Subset-Family of X st ( Y c= A & x = union Y ) ) ) & ( for x being Subset of X holds ( x in F2 iff ex Y being Subset-Family of X st ( Y c= A & x = union Y ) ) ) implies F1 = F2 ) assume that A1: for x being Subset of X holds ( x in F1 iff ex Y being Subset-Family of X st ( Y c= A & x = union Y ) ) and A2: for x being Subset of X holds ( x in F2 iff ex Y being Subset-Family of X st ( Y c= A & x = union Y ) ) ; ::_thesis: F1 = F2 now__::_thesis:_for_x_being_Subset_of_X_holds_ (_x_in_F1_iff_x_in_F2_) let x be Subset of X; ::_thesis: ( x in F1 iff x in F2 ) ( x in F1 iff ex Y being Subset-Family of X st ( Y c= A & x = union Y ) ) by A1; hence ( x in F1 iff x in F2 ) by A2; ::_thesis: verum end; hence F1 = F2 by SUBSET_1:3; ::_thesis: verum end; end; :: deftheorem Def1 defines UniCl CANTOR_1:def_1_:_ for X being set for A, b3 being Subset-Family of X holds ( b3 = UniCl A iff for x being Subset of X holds ( x in b3 iff ex Y being Subset-Family of X st ( Y c= A & x = union Y ) ) ); definition let X be TopStruct ; let F be Subset-Family of X; attrF is quasi_basis means :Def2: :: CANTOR_1:def 2 the topology of X c= UniCl F; end; :: deftheorem Def2 defines quasi_basis CANTOR_1:def_2_:_ for X being TopStruct for F being Subset-Family of X holds ( F is quasi_basis iff the topology of X c= UniCl F ); registration let X be TopStruct ; cluster the topology of X -> quasi_basis ; coherence the topology of X is quasi_basis proof set F = the topology of X; let A be set ; :: according to TARSKI:def_3,CANTOR_1:def_2 ::_thesis: ( not A in the topology of X or A in UniCl the topology of X ) assume A1: A in the topology of X ; ::_thesis: A in UniCl the topology of X then reconsider B = {A} as Subset-Family of X by SUBSET_1:41; A2: B c= the topology of X by A1, ZFMISC_1:31; A = union B by ZFMISC_1:25; hence A in UniCl the topology of X by A2, Def1; ::_thesis: verum end; end; registration let X be TopStruct ; cluster open quasi_basis for Element of bool (bool the carrier of X); existence ex b1 being Subset-Family of X st ( b1 is open & b1 is quasi_basis ) proof take the topology of X ; ::_thesis: ( the topology of X is open & the topology of X is quasi_basis ) thus ( the topology of X is open & the topology of X is quasi_basis ) ; ::_thesis: verum end; end; definition let X be TopStruct ; mode Basis of X is open quasi_basis Subset-Family of X; end; theorem Th1: :: CANTOR_1:1 for X being set for A being Subset-Family of X holds A c= UniCl A proof let X be set ; ::_thesis: for A being Subset-Family of X holds A c= UniCl A let A be Subset-Family of X; ::_thesis: A c= UniCl A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in UniCl A ) assume A1: x in A ; ::_thesis: x in UniCl A then reconsider x9 = x as Subset of X ; reconsider s = {x9} as Subset-Family of X by SUBSET_1:41; A2: x = union s by ZFMISC_1:25; s c= A by A1, ZFMISC_1:31; hence x in UniCl A by A2, Def1; ::_thesis: verum end; theorem :: CANTOR_1:2 for S being TopStruct holds the topology of S is Basis of S ; theorem :: CANTOR_1:3 for S being TopStruct holds the topology of S is open ; definition let X be set ; let A be Subset-Family of X; func FinMeetCl A -> Subset-Family of X means :Def3: :: CANTOR_1:def 3 for x being Subset of X holds ( x in it iff ex Y being Subset-Family of X st ( Y c= A & Y is finite & x = Intersect Y ) ); existence ex b1 being Subset-Family of X st for x being Subset of X holds ( x in b1 iff ex Y being Subset-Family of X st ( Y c= A & Y is finite & x = Intersect Y ) ) proof defpred S1[ set ] means ex Y being Subset-Family of X st ( Y c= A & Y is finite & \$1 = Intersect Y ); ex Z being Subset-Family of X st for x being Subset of X holds ( x in Z iff S1[x] ) from SUBSET_1:sch_3(); hence ex b1 being Subset-Family of X st for x being Subset of X holds ( x in b1 iff ex Y being Subset-Family of X st ( Y c= A & Y is finite & x = Intersect Y ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Subset-Family of X st ( for x being Subset of X holds ( x in b1 iff ex Y being Subset-Family of X st ( Y c= A & Y is finite & x = Intersect Y ) ) ) & ( for x being Subset of X holds ( x in b2 iff ex Y being Subset-Family of X st ( Y c= A & Y is finite & x = Intersect Y ) ) ) holds b1 = b2 proof let B1, B2 be Subset-Family of X; ::_thesis: ( ( for x being Subset of X holds ( x in B1 iff ex Y being Subset-Family of X st ( Y c= A & Y is finite & x = Intersect Y ) ) ) & ( for x being Subset of X holds ( x in B2 iff ex Y being Subset-Family of X st ( Y c= A & Y is finite & x = Intersect Y ) ) ) implies B1 = B2 ) assume that A1: for x being Subset of X holds ( x in B1 iff ex Y being Subset-Family of X st ( Y c= A & Y is finite & x = Intersect Y ) ) and A2: for x being Subset of X holds ( x in B2 iff ex Y being Subset-Family of X st ( Y c= A & Y is finite & x = Intersect Y ) ) ; ::_thesis: B1 = B2 now__::_thesis:_for_x_being_Subset_of_X_holds_ (_x_in_B2_iff_x_in_B1_) let x be Subset of X; ::_thesis: ( x in B2 iff x in B1 ) ( x in B2 iff ex Y being Subset-Family of X st ( Y c= A & Y is finite & x = Intersect Y ) ) by A2; hence ( x in B2 iff x in B1 ) by A1; ::_thesis: verum end; hence B1 = B2 by SUBSET_1:3; ::_thesis: verum end; end; :: deftheorem Def3 defines FinMeetCl CANTOR_1:def_3_:_ for X being set for A, b3 being Subset-Family of X holds ( b3 = FinMeetCl A iff for x being Subset of X holds ( x in b3 iff ex Y being Subset-Family of X st ( Y c= A & Y is finite & x = Intersect Y ) ) ); theorem Th4: :: CANTOR_1:4 for X being set for A being Subset-Family of X holds A c= FinMeetCl A proof let X be set ; ::_thesis: for A being Subset-Family of X holds A c= FinMeetCl A let A be Subset-Family of X; ::_thesis: A c= FinMeetCl A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in FinMeetCl A ) assume A1: x in A ; ::_thesis: x in FinMeetCl A then reconsider x9 = x as Subset of X ; reconsider s = {x9} as Subset-Family of X by SUBSET_1:41; x = meet s by SETFAM_1:10; then A2: x = Intersect s by SETFAM_1:def_9; s c= A by A1, ZFMISC_1:31; hence x in FinMeetCl A by A2, Def3; ::_thesis: verum end; theorem Th5: :: CANTOR_1:5 for T being non empty TopSpace holds the topology of T = FinMeetCl the topology of T proof let T be non empty TopSpace; ::_thesis: the topology of T = FinMeetCl the topology of T set X = the topology of T; defpred S1[ set ] means meet \$1 in the topology of T; A1: for B9 being Element of Fin the topology of T for b being Element of the topology of T st S1[B9] holds S1[B9 \/ {b}] proof let B9 be Element of Fin the topology of T; ::_thesis: for b being Element of the topology of T st S1[B9] holds S1[B9 \/ {b}] let b be Element of the topology of T; ::_thesis: ( S1[B9] implies S1[B9 \/ {b}] ) A2: meet {b} = b by SETFAM_1:10; assume A3: meet B9 in the topology of T ; ::_thesis: S1[B9 \/ {b}] percases ( B9 <> {} or B9 = {} ) ; suppose B9 <> {} ; ::_thesis: S1[B9 \/ {b}] then meet (B9 \/ {b}) = (meet B9) /\ (meet {b}) by SETFAM_1:9; hence S1[B9 \/ {b}] by A2, A3, PRE_TOPC:def_1; ::_thesis: verum end; suppose B9 = {} ; ::_thesis: S1[B9 \/ {b}] hence S1[B9 \/ {b}] by A2; ::_thesis: verum end; end; end; thus the topology of T c= FinMeetCl the topology of T by Th4; :: according to XBOOLE_0:def_10 ::_thesis: FinMeetCl the topology of T c= the topology of T A4: S1[ {}. the topology of T] by PRE_TOPC:1, SETFAM_1:1; A5: for B being Element of Fin the topology of T holds S1[B] from SETWISEO:sch_4(A4, A1); now__::_thesis:_for_x_being_Subset_of_T_st_x_in_FinMeetCl_the_topology_of_T_holds_ x_in_the_topology_of_T let x be Subset of T; ::_thesis: ( x in FinMeetCl the topology of T implies b1 in the topology of T ) assume x in FinMeetCl the topology of T ; ::_thesis: b1 in the topology of T then consider y being Subset-Family of T such that A6: ( y c= the topology of T & y is finite ) and A7: x = Intersect y by Def3; reconsider y = y as Subset-Family of T ; percases ( y <> {} or y = {} ) ; supposeA8: y <> {} ; ::_thesis: b1 in the topology of T A9: y in Fin the topology of T by A6, FINSUB_1:def_5; x = meet y by A7, A8, SETFAM_1:def_9; hence x in the topology of T by A5, A9; ::_thesis: verum end; supposeA10: y = {} ; ::_thesis: b1 in the topology of T reconsider aa = {} (bool the carrier of T) as Subset-Family of the carrier of T ; Intersect aa = the carrier of T by SETFAM_1:def_9; hence x in the topology of T by A7, A10, PRE_TOPC:def_1; ::_thesis: verum end; end; end; hence FinMeetCl the topology of T c= the topology of T by SUBSET_1:2; ::_thesis: verum end; theorem Th6: :: CANTOR_1:6 for T being TopSpace holds the topology of T = UniCl the topology of T proof let T be TopSpace; ::_thesis: the topology of T = UniCl the topology of T thus the topology of T c= UniCl the topology of T by Th1; :: according to XBOOLE_0:def_10 ::_thesis: UniCl the topology of T c= the topology of T let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in UniCl the topology of T or a in the topology of T ) assume A1: a in UniCl the topology of T ; ::_thesis: a in the topology of T then reconsider a9 = a as Subset of T ; ex b being Subset-Family of T st ( b c= the topology of T & a9 = union b ) by A1, Def1; hence a in the topology of T by PRE_TOPC:def_1; ::_thesis: verum end; theorem Th7: :: CANTOR_1:7 for T being non empty TopSpace holds the topology of T = UniCl (FinMeetCl the topology of T) proof let T be non empty TopSpace; ::_thesis: the topology of T = UniCl (FinMeetCl the topology of T) the topology of T = FinMeetCl the topology of T by Th5; hence the topology of T = UniCl (FinMeetCl the topology of T) by Th6; ::_thesis: verum end; theorem Th8: :: CANTOR_1:8 for X being set for A being Subset-Family of X holds X in FinMeetCl A proof let X be set ; ::_thesis: for A being Subset-Family of X holds X in FinMeetCl A let A be Subset-Family of X; ::_thesis: X in FinMeetCl A {} is Subset-Family of X by XBOOLE_1:2; then consider y being Subset-Family of X such that A1: y = {} ; ( y c= A & Intersect y = X ) by A1, SETFAM_1:def_9, XBOOLE_1:2; hence X in FinMeetCl A by A1, Def3; ::_thesis: verum end; theorem Th9: :: CANTOR_1:9 for X being set for A, B being Subset-Family of X st A c= B holds UniCl A c= UniCl B proof let X be set ; ::_thesis: for A, B being Subset-Family of X st A c= B holds UniCl A c= UniCl B let A, B be Subset-Family of X; ::_thesis: ( A c= B implies UniCl A c= UniCl B ) assume A1: A c= B ; ::_thesis: UniCl A c= UniCl B let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UniCl A or x in UniCl B ) assume A2: x in UniCl A ; ::_thesis: x in UniCl B then reconsider x9 = x as Subset of X ; consider T being Subset-Family of X such that A3: T c= A and A4: x9 = union T by A2, Def1; T c= B by A1, A3, XBOOLE_1:1; hence x in UniCl B by A4, Def1; ::_thesis: verum end; theorem Th10: :: CANTOR_1:10 for X being set for R being non empty Subset-Family of (bool X) for F being Subset-Family of X st F = { (Intersect x) where x is Element of R : verum } holds Intersect F = Intersect (union R) proof let X be set ; ::_thesis: for R being non empty Subset-Family of (bool X) for F being Subset-Family of X st F = { (Intersect x) where x is Element of R : verum } holds Intersect F = Intersect (union R) let R be non empty Subset-Family of (bool X); ::_thesis: for F being Subset-Family of X st F = { (Intersect x) where x is Element of R : verum } holds Intersect F = Intersect (union R) let F be Subset-Family of X; ::_thesis: ( F = { (Intersect x) where x is Element of R : verum } implies Intersect F = Intersect (union R) ) assume A1: F = { (Intersect x) where x is Element of R : verum } ; ::_thesis: Intersect F = Intersect (union R) hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: Intersect (union R) c= Intersect F let c be set ; ::_thesis: ( c in Intersect F implies c in Intersect (union R) ) assume A2: c in Intersect F ; ::_thesis: c in Intersect (union R) for Y being set st Y in union R holds c in Y proof let Y be set ; ::_thesis: ( Y in union R implies c in Y ) assume Y in union R ; ::_thesis: c in Y then consider d being set such that A3: Y in d and A4: d in R by TARSKI:def_4; reconsider d = d as Subset-Family of X by A4; reconsider d = d as Subset-Family of X ; Intersect d in F by A1, A4; then c in Intersect d by A2, SETFAM_1:43; hence c in Y by A3, SETFAM_1:43; ::_thesis: verum end; hence c in Intersect (union R) by A2, SETFAM_1:43; ::_thesis: verum end; let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in Intersect (union R) or c in Intersect F ) assume A5: c in Intersect (union R) ; ::_thesis: c in Intersect F for Y being set st Y in F holds c in Y proof let Y be set ; ::_thesis: ( Y in F implies c in Y ) assume Y in F ; ::_thesis: c in Y then consider x being Element of R such that A6: Y = Intersect x by A1; Intersect (union R) c= Intersect x by SETFAM_1:44, ZFMISC_1:74; hence c in Y by A5, A6; ::_thesis: verum end; hence c in Intersect F by A5, SETFAM_1:43; ::_thesis: verum end; theorem Th11: :: CANTOR_1:11 for X being set for A being Subset-Family of X holds FinMeetCl A = FinMeetCl (FinMeetCl A) proof let X be set ; ::_thesis: for A being Subset-Family of X holds FinMeetCl A = FinMeetCl (FinMeetCl A) let A be Subset-Family of X; ::_thesis: FinMeetCl A = FinMeetCl (FinMeetCl A) defpred S1[ set , set ] means ex A being Subset-Family of X st ( \$1 = Intersect A & A = \$2 & \$2 is finite ); thus FinMeetCl A c= FinMeetCl (FinMeetCl A) by Th4; :: according to XBOOLE_0:def_10 ::_thesis: FinMeetCl (FinMeetCl A) c= FinMeetCl A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in FinMeetCl (FinMeetCl A) or x in FinMeetCl A ) assume A1: x in FinMeetCl (FinMeetCl A) ; ::_thesis: x in FinMeetCl A then reconsider x9 = x as Subset of X ; consider Y being Subset-Family of X such that A2: Y c= FinMeetCl A and A3: Y is finite and A4: x9 = Intersect Y by A1, Def3; A5: for e being set st e in Y holds ex u being set st ( u in bool A & S1[e,u] ) proof let e be set ; ::_thesis: ( e in Y implies ex u being set st ( u in bool A & S1[e,u] ) ) assume A6: e in Y ; ::_thesis: ex u being set st ( u in bool A & S1[e,u] ) then reconsider e9 = e as Subset of X ; consider Y being Subset-Family of X such that A7: ( Y c= A & Y is finite & e9 = Intersect Y ) by A2, A6, Def3; take Y ; ::_thesis: ( Y in bool A & S1[e,Y] ) thus ( Y in bool A & S1[e,Y] ) by A7; ::_thesis: verum end; consider f being Function of Y,(bool A) such that A8: for e being set st e in Y holds S1[e,f . e] from FUNCT_2:sch_1(A5); set fz = { (Intersect s) where s is Subset-Family of X : s in rng f } ; A9: { (Intersect s) where s is Subset-Family of X : s in rng f } c= Y proof let l be set ; :: according to TARSKI:def_3 ::_thesis: ( not l in { (Intersect s) where s is Subset-Family of X : s in rng f } or l in Y ) assume l in { (Intersect s) where s is Subset-Family of X : s in rng f } ; ::_thesis: l in Y then consider s being Subset-Family of X such that A10: l = Intersect s and A11: s in rng f ; consider v being set such that A12: v in dom f and A13: s = f . v by A11, FUNCT_1:def_3; v in Y by A12, FUNCT_2:def_1; then S1[v,f . v] by A8; hence l in Y by A10, A12, A13, FUNCT_2:def_1; ::_thesis: verum end; rng f c= bool A by RELAT_1:def_19; then union (rng f) c= union (bool A) by ZFMISC_1:77; then A14: union (rng f) c= A by ZFMISC_1:81; then reconsider y = union (rng f) as Subset-Family of X by XBOOLE_1:1; reconsider y = y as Subset-Family of X ; Y c= { (Intersect s) where s is Subset-Family of X : s in rng f } proof let l be set ; :: according to TARSKI:def_3 ::_thesis: ( not l in Y or l in { (Intersect s) where s is Subset-Family of X : s in rng f } ) assume A15: l in Y ; ::_thesis: l in { (Intersect s) where s is Subset-Family of X : s in rng f } then consider C being Subset-Family of X such that A16: l = Intersect C and A17: C = f . l and f . l is finite by A8; l in dom f by A15, FUNCT_2:def_1; then C in rng f by A17, FUNCT_1:def_3; hence l in { (Intersect s) where s is Subset-Family of X : s in rng f } by A16; ::_thesis: verum end; then A18: Y = { (Intersect s) where s is Subset-Family of X : s in rng f } by A9, XBOOLE_0:def_10; A19: x = Intersect y proof percases ( rng f <> {} or rng f = {} ) ; supposeA20: rng f <> {} ; ::_thesis: x = Intersect y ( rng f c= bool A & bool A c= bool (bool X) ) by RELAT_1:def_19, ZFMISC_1:67; then reconsider GGG = rng f as non empty Subset-Family of (bool X) by A20, XBOOLE_1:1; reconsider GGG = GGG as non empty Subset-Family of (bool X) ; { (Intersect s) where s is Subset-Family of X : s in rng f } = { (Intersect b) where b is Element of GGG : verum } proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { (Intersect b) where b is Element of GGG : verum } c= { (Intersect s) where s is Subset-Family of X : s in rng f } let x be set ; ::_thesis: ( x in { (Intersect s) where s is Subset-Family of X : s in rng f } implies x in { (Intersect b) where b is Element of GGG : verum } ) assume x in { (Intersect s) where s is Subset-Family of X : s in rng f } ; ::_thesis: x in { (Intersect b) where b is Element of GGG : verum } then ex s being Subset-Family of X st ( x = Intersect s & s in rng f ) ; hence x in { (Intersect b) where b is Element of GGG : verum } ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (Intersect b) where b is Element of GGG : verum } or x in { (Intersect s) where s is Subset-Family of X : s in rng f } ) assume x in { (Intersect b) where b is Element of GGG : verum } ; ::_thesis: x in { (Intersect s) where s is Subset-Family of X : s in rng f } then ex s being Element of GGG st x = Intersect s ; hence x in { (Intersect s) where s is Subset-Family of X : s in rng f } ; ::_thesis: verum end; hence x = Intersect y by A4, A18, Th10; ::_thesis: verum end; supposeA21: rng f = {} ; ::_thesis: x = Intersect y Y = dom f by FUNCT_2:def_1; hence x = Intersect y by A4, A21, RELAT_1:38, RELAT_1:41, ZFMISC_1:2; ::_thesis: verum end; end; end; for V being set st V in rng f holds V is finite proof let V be set ; ::_thesis: ( V in rng f implies V is finite ) assume V in rng f ; ::_thesis: V is finite then consider x being set such that A22: x in dom f and A23: V = f . x by FUNCT_1:def_3; x in Y by A22, FUNCT_2:def_1; then reconsider x = x as Subset of X ; reconsider G = f . x as Subset-Family of X ; x in Y by A22, FUNCT_2:def_1; then S1[x,G] by A8; hence V is finite by A23; ::_thesis: verum end; then union (rng f) is finite by A3, FINSET_1:7; hence x in FinMeetCl A by A14, A19, Def3; ::_thesis: verum end; theorem :: CANTOR_1:12 for X being set for A being Subset-Family of X for a, b being set st a in FinMeetCl A & b in FinMeetCl A holds a /\ b in FinMeetCl A proof let X be set ; ::_thesis: for A being Subset-Family of X for a, b being set st a in FinMeetCl A & b in FinMeetCl A holds a /\ b in FinMeetCl A let A be Subset-Family of X; ::_thesis: for a, b being set st a in FinMeetCl A & b in FinMeetCl A holds a /\ b in FinMeetCl A let a, b be set ; ::_thesis: ( a in FinMeetCl A & b in FinMeetCl A implies a /\ b in FinMeetCl A ) assume A1: ( a in FinMeetCl A & b in FinMeetCl A ) ; ::_thesis: a /\ b in FinMeetCl A then reconsider M = {a,b} as Subset-Family of X by ZFMISC_1:32; reconsider M = M as Subset-Family of X ; a /\ b = meet M by SETFAM_1:11; then A2: a /\ b = Intersect M by SETFAM_1:def_9; M c= FinMeetCl A by A1, ZFMISC_1:32; then Intersect M in FinMeetCl (FinMeetCl A) by Def3; hence a /\ b in FinMeetCl A by A2, Th11; ::_thesis: verum end; theorem Th13: :: CANTOR_1:13 for X being set for A being Subset-Family of X for a, b being set st a c= FinMeetCl A & b c= FinMeetCl A holds INTERSECTION (a,b) c= FinMeetCl A proof let X be set ; ::_thesis: for A being Subset-Family of X for a, b being set st a c= FinMeetCl A & b c= FinMeetCl A holds INTERSECTION (a,b) c= FinMeetCl A let A be Subset-Family of X; ::_thesis: for a, b being set st a c= FinMeetCl A & b c= FinMeetCl A holds INTERSECTION (a,b) c= FinMeetCl A let a, b be set ; ::_thesis: ( a c= FinMeetCl A & b c= FinMeetCl A implies INTERSECTION (a,b) c= FinMeetCl A ) assume A1: ( a c= FinMeetCl A & b c= FinMeetCl A ) ; ::_thesis: INTERSECTION (a,b) c= FinMeetCl A let Z be set ; :: according to TARSKI:def_3 ::_thesis: ( not Z in INTERSECTION (a,b) or Z in FinMeetCl A ) assume Z in INTERSECTION (a,b) ; ::_thesis: Z in FinMeetCl A then consider V, B being set such that A2: ( V in a & B in b ) and A3: Z = V /\ B by SETFAM_1:def_5; ( V in FinMeetCl A & B in FinMeetCl A ) by A1, A2; then reconsider M = {V,B} as Subset-Family of X by ZFMISC_1:32; reconsider M = M as Subset-Family of X ; V /\ B = meet M by SETFAM_1:11; then A4: V /\ B = Intersect M by SETFAM_1:def_9; M c= FinMeetCl A by A1, A2, ZFMISC_1:32; then Intersect M in FinMeetCl (FinMeetCl A) by Def3; hence Z in FinMeetCl A by A3, A4, Th11; ::_thesis: verum end; theorem Th14: :: CANTOR_1:14 for X being set for A, B being Subset-Family of X st A c= B holds FinMeetCl A c= FinMeetCl B proof let X be set ; ::_thesis: for A, B being Subset-Family of X st A c= B holds FinMeetCl A c= FinMeetCl B let A, B be Subset-Family of X; ::_thesis: ( A c= B implies FinMeetCl A c= FinMeetCl B ) assume A1: A c= B ; ::_thesis: FinMeetCl A c= FinMeetCl B let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in FinMeetCl A or x in FinMeetCl B ) assume A2: x in FinMeetCl A ; ::_thesis: x in FinMeetCl B then reconsider x = x as Subset of X ; consider y being Subset-Family of X such that A3: y c= A and A4: ( y is finite & x = Intersect y ) by A2, Def3; y c= B by A1, A3, XBOOLE_1:1; hence x in FinMeetCl B by A4, Def3; ::_thesis: verum end; registration let X be set ; let A be Subset-Family of X; cluster FinMeetCl A -> non empty ; coherence not FinMeetCl A is empty by Th8; end; theorem Th15: :: CANTOR_1:15 for X being non empty set for A being Subset-Family of X holds TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like proof let X be non empty set ; ::_thesis: for A being Subset-Family of X holds TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like let A be Subset-Family of X; ::_thesis: TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like set T = TopStruct(# X,(UniCl (FinMeetCl A)) #); A1: [#] TopStruct(# X,(UniCl (FinMeetCl A)) #) in FinMeetCl A by Th8; now__::_thesis:_ex_Y_being_Subset-Family_of_X_st_ (_Y_c=_FinMeetCl_A_&_[#]_TopStruct(#_X,(UniCl_(FinMeetCl_A))_#)_=_union_Y_) reconsider Y = {([#] TopStruct(# X,(UniCl (FinMeetCl A)) #))} as Subset-Family of X by ZFMISC_1:68; reconsider Y = Y as Subset-Family of X ; take Y = Y; ::_thesis: ( Y c= FinMeetCl A & [#] TopStruct(# X,(UniCl (FinMeetCl A)) #) = union Y ) thus Y c= FinMeetCl A by A1, ZFMISC_1:31; ::_thesis: [#] TopStruct(# X,(UniCl (FinMeetCl A)) #) = union Y thus [#] TopStruct(# X,(UniCl (FinMeetCl A)) #) = union Y by ZFMISC_1:25; ::_thesis: verum end; hence the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #) in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) by Def1; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #)) holds ( not b1 c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or union b1 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) ) & ( for b1, b2 being Element of bool the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #) holds ( not b1 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or not b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or b1 /\ b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) ) ) thus for a being Subset-Family of TopStruct(# X,(UniCl (FinMeetCl A)) #) st a c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) holds union a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ::_thesis: for b1, b2 being Element of bool the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #) holds ( not b1 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or not b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or b1 /\ b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) proof let a be Subset-Family of TopStruct(# X,(UniCl (FinMeetCl A)) #); ::_thesis: ( a c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) implies union a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) assume A2: a c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ; ::_thesis: union a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) defpred S1[ set ] means ex c being Subset of TopStruct(# X,(UniCl (FinMeetCl A)) #) st ( c in a & c = union \$1 ); consider b being Subset-Family of (FinMeetCl A) such that A3: for B being Subset of (FinMeetCl A) holds ( B in b iff S1[B] ) from SUBSET_1:sch_3(); A4: a = { (union B) where B is Subset of (FinMeetCl A) : B in b } proof set gh = { (union B) where B is Subset of (FinMeetCl A) : B in b } ; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { (union B) where B is Subset of (FinMeetCl A) : B in b } c= a let x be set ; ::_thesis: ( x in a implies x in { (union B) where B is Subset of (FinMeetCl A) : B in b } ) assume A5: x in a ; ::_thesis: x in { (union B) where B is Subset of (FinMeetCl A) : B in b } then reconsider x9 = x as Subset of X ; consider V being Subset-Family of X such that A6: V c= FinMeetCl A and A7: x9 = union V by A2, A5, Def1; V in b by A3, A5, A6, A7; hence x in { (union B) where B is Subset of (FinMeetCl A) : B in b } by A7; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (union B) where B is Subset of (FinMeetCl A) : B in b } or x in a ) assume x in { (union B) where B is Subset of (FinMeetCl A) : B in b } ; ::_thesis: x in a then consider B being Subset of (FinMeetCl A) such that A8: x = union B and A9: B in b ; ex c being Subset of TopStruct(# X,(UniCl (FinMeetCl A)) #) st ( c in a & c = union B ) by A3, A9; hence x in a by A8; ::_thesis: verum end; ( union (union b) = union { (union B) where B is Subset of (FinMeetCl A) : B in b } & union b c= bool X ) by EQREL_1:54, XBOOLE_1:1; hence union a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) by A4, Def1; ::_thesis: verum end; let a, b be Subset of TopStruct(# X,(UniCl (FinMeetCl A)) #); ::_thesis: ( not a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or not b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or a /\ b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) assume a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ; ::_thesis: ( not b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or a /\ b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) then consider F being Subset-Family of X such that A10: F c= FinMeetCl A and A11: a = union F by Def1; assume b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ; ::_thesis: a /\ b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) then consider G being Subset-Family of X such that A12: G c= FinMeetCl A and A13: b = union G by Def1; A14: union (INTERSECTION (F,G)) = a /\ b by A11, A13, SETFAM_1:28; A15: INTERSECTION (F,G) c= FinMeetCl A by A10, A12, Th13; then INTERSECTION (F,G) is Subset-Family of X by XBOOLE_1:1; hence a /\ b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) by A15, A14, Def1; ::_thesis: verum end; definition let X be TopStruct ; let F be Subset-Family of X; attrF is quasi_prebasis means :Def4: :: CANTOR_1:def 4 ex G being Basis of X st G c= FinMeetCl F; end; :: deftheorem Def4 defines quasi_prebasis CANTOR_1:def_4_:_ for X being TopStruct for F being Subset-Family of X holds ( F is quasi_prebasis iff ex G being Basis of X st G c= FinMeetCl F ); registration let X be TopStruct ; cluster the topology of X -> quasi_prebasis ; coherence the topology of X is quasi_prebasis proof take the topology of X ; :: according to CANTOR_1:def_4 ::_thesis: the topology of X c= FinMeetCl the topology of X thus the topology of X c= FinMeetCl the topology of X by Th4; ::_thesis: verum end; cluster open quasi_basis -> quasi_prebasis for Element of bool (bool the carrier of X); coherence for b1 being Basis of X holds b1 is quasi_prebasis proof let F be Basis of X; ::_thesis: F is quasi_prebasis take F ; :: according to CANTOR_1:def_4 ::_thesis: F c= FinMeetCl F thus F c= FinMeetCl F by Th4; ::_thesis: verum end; cluster open quasi_prebasis for Element of bool (bool the carrier of X); existence ex b1 being Subset-Family of X st ( b1 is open & b1 is quasi_prebasis ) proof take the topology of X ; ::_thesis: ( the topology of X is open & the topology of X is quasi_prebasis ) thus ( the topology of X is open & the topology of X is quasi_prebasis ) ; ::_thesis: verum end; end; definition let X be TopStruct ; mode prebasis of X is open quasi_prebasis Subset-Family of X; end; theorem Th16: :: CANTOR_1:16 for X being non empty set for Y being Subset-Family of X holds Y is Basis of TopStruct(# X,(UniCl Y) #) proof let X be non empty set ; ::_thesis: for Y being Subset-Family of X holds Y is Basis of TopStruct(# X,(UniCl Y) #) let Y be Subset-Family of X; ::_thesis: Y is Basis of TopStruct(# X,(UniCl Y) #) Y c= UniCl Y by Th1; hence Y is Basis of TopStruct(# X,(UniCl Y) #) by Def2, TOPS_2:64; ::_thesis: verum end; theorem Th17: :: CANTOR_1:17 for T1, T2 being non empty strict TopSpace for P being prebasis of T1 st the carrier of T1 = the carrier of T2 & P is prebasis of T2 holds T1 = T2 proof let T1, T2 be non empty strict TopSpace; ::_thesis: for P being prebasis of T1 st the carrier of T1 = the carrier of T2 & P is prebasis of T2 holds T1 = T2 let P be prebasis of T1; ::_thesis: ( the carrier of T1 = the carrier of T2 & P is prebasis of T2 implies T1 = T2 ) assume that A1: the carrier of T1 = the carrier of T2 and A2: P is prebasis of T2 ; ::_thesis: T1 = T2 reconsider P9 = P as prebasis of T2 by A2; consider B1 being Basis of T1 such that A3: B1 c= FinMeetCl P by Def4; P c= the topology of T1 by TOPS_2:64; then FinMeetCl P c= FinMeetCl the topology of T1 by Th14; then A4: UniCl (FinMeetCl P) c= UniCl (FinMeetCl the topology of T1) by Th9; P9 c= the topology of T2 by TOPS_2:64; then FinMeetCl P9 c= FinMeetCl the topology of T2 by Th14; then A5: UniCl (FinMeetCl P9) c= UniCl (FinMeetCl the topology of T2) by Th9; A6: the topology of T1 c= UniCl B1 by Def2; UniCl B1 c= UniCl (FinMeetCl P) by A3, Th9; then A7: the topology of T1 c= UniCl (FinMeetCl P) by A6, XBOOLE_1:1; consider B2 being Basis of T2 such that A8: B2 c= FinMeetCl P9 by Def4; A9: the topology of T2 c= UniCl B2 by Def2; UniCl B2 c= UniCl (FinMeetCl P9) by A8, Th9; then A10: the topology of T2 c= UniCl (FinMeetCl P9) by A9, XBOOLE_1:1; the topology of T2 = UniCl (FinMeetCl the topology of T2) by Th7; then A11: UniCl (FinMeetCl P9) = the topology of T2 by A10, A5, XBOOLE_0:def_10; the topology of T1 = UniCl (FinMeetCl the topology of T1) by Th7; hence T1 = T2 by A1, A7, A11, A4, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th18: :: CANTOR_1:18 for X being non empty set for Y being Subset-Family of X holds Y is prebasis of TopStruct(# X,(UniCl (FinMeetCl Y)) #) proof let X be non empty set ; ::_thesis: for Y being Subset-Family of X holds Y is prebasis of TopStruct(# X,(UniCl (FinMeetCl Y)) #) let A be Subset-Family of X; ::_thesis: A is prebasis of TopStruct(# X,(UniCl (FinMeetCl A)) #) set T = TopStruct(# X,(UniCl (FinMeetCl A)) #); reconsider A9 = A as Subset-Family of TopStruct(# X,(UniCl (FinMeetCl A)) #) ; now__::_thesis:_(_A9_is_open_&_A9_is_quasi_prebasis_) ( A9 c= FinMeetCl A & FinMeetCl A c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) by Th1, Th4; then A9 c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) by XBOOLE_1:1; hence A9 is open by TOPS_2:64; ::_thesis: A9 is quasi_prebasis thus A9 is quasi_prebasis ::_thesis: verum proof reconsider B = FinMeetCl A9 as Basis of TopStruct(# X,(UniCl (FinMeetCl A)) #) by Th16; take B ; :: according to CANTOR_1:def_4 ::_thesis: B c= FinMeetCl A9 thus B c= FinMeetCl A9 ; ::_thesis: verum end; end; hence A is prebasis of TopStruct(# X,(UniCl (FinMeetCl A)) #) ; ::_thesis: verum end; definition func the_Cantor_set -> non empty strict TopSpace means :: CANTOR_1:def 5 ( the carrier of it = product (NAT --> {0,1}) & ex P being prebasis of it st for X being Subset of (product (NAT --> {0,1})) holds ( X in P iff ex N, n being Nat st for F being Element of product (NAT --> {0,1}) holds ( F in X iff F . N = n ) ) ); existence ex b1 being non empty strict TopSpace st ( the carrier of b1 = product (NAT --> {0,1}) & ex P being prebasis of b1 st for X being Subset of (product (NAT --> {0,1})) holds ( X in P iff ex N, n being Nat st for F being Element of product (NAT --> {0,1}) holds ( F in X iff F . N = n ) ) ) proof defpred S1[ set ] means ex N, n being Nat st for F being Element of product (NAT --> {0,1}) holds ( F in \$1 iff F . N = n ); consider Y being Subset-Family of (product (NAT --> {0,1})) such that A1: for y being Subset of (product (NAT --> {0,1})) holds ( y in Y iff S1[y] ) from SUBSET_1:sch_3(); reconsider T = TopStruct(# (product (NAT --> {0,1})),(UniCl (FinMeetCl Y)) #) as non empty strict TopSpace by Th15; take T ; ::_thesis: ( the carrier of T = product (NAT --> {0,1}) & ex P being prebasis of T st for X being Subset of (product (NAT --> {0,1})) holds ( X in P iff ex N, n being Nat st for F being Element of product (NAT --> {0,1}) holds ( F in X iff F . N = n ) ) ) thus the carrier of T = product (NAT --> {0,1}) ; ::_thesis: ex P being prebasis of T st for X being Subset of (product (NAT --> {0,1})) holds ( X in P iff ex N, n being Nat st for F being Element of product (NAT --> {0,1}) holds ( F in X iff F . N = n ) ) reconsider Y = Y as prebasis of T by Th18; take Y ; ::_thesis: for X being Subset of (product (NAT --> {0,1})) holds ( X in Y iff ex N, n being Nat st for F being Element of product (NAT --> {0,1}) holds ( F in X iff F . N = n ) ) thus for X being Subset of (product (NAT --> {0,1})) holds ( X in Y iff ex N, n being Nat st for F being Element of product (NAT --> {0,1}) holds ( F in X iff F . N = n ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being non empty strict TopSpace st the carrier of b1 = product (NAT --> {0,1}) & ex P being prebasis of b1 st for X being Subset of (product (NAT --> {0,1})) holds ( X in P iff ex N, n being Nat st for F being Element of product (NAT --> {0,1}) holds ( F in X iff F . N = n ) ) & the carrier of b2 = product (NAT --> {0,1}) & ex P being prebasis of b2 st for X being Subset of (product (NAT --> {0,1})) holds ( X in P iff ex N, n being Nat st for F being Element of product (NAT --> {0,1}) holds ( F in X iff F . N = n ) ) holds b1 = b2 proof let T1, T2 be non empty strict TopSpace; ::_thesis: ( the carrier of T1 = product (NAT --> {0,1}) & ex P being prebasis of T1 st for X being Subset of (product (NAT --> {0,1})) holds ( X in P iff ex N, n being Nat st for F being Element of product (NAT --> {0,1}) holds ( F in X iff F . N = n ) ) & the carrier of T2 = product (NAT --> {0,1}) & ex P being prebasis of T2 st for X being Subset of (product (NAT --> {0,1})) holds ( X in P iff ex N, n being Nat st for F being Element of product (NAT --> {0,1}) holds ( F in X iff F . N = n ) ) implies T1 = T2 ) assume that A2: the carrier of T1 = product (NAT --> {0,1}) and A3: ex P being prebasis of T1 st for X being Subset of (product (NAT --> {0,1})) holds ( X in P iff ex N, n being Nat st for F being Element of product (NAT --> {0,1}) holds ( F in X iff F . N = n ) ) and A4: the carrier of T2 = product (NAT --> {0,1}) and A5: ex P being prebasis of T2 st for X being Subset of (product (NAT --> {0,1})) holds ( X in P iff ex N, n being Nat st for F being Element of product (NAT --> {0,1}) holds ( F in X iff F . N = n ) ) ; ::_thesis: T1 = T2 consider P1 being prebasis of T1 such that A6: for X being Subset of (product (NAT --> {0,1})) holds ( X in P1 iff ex N, n being Nat st for F being Element of product (NAT --> {0,1}) holds ( F in X iff F . N = n ) ) by A3; consider P2 being prebasis of T2 such that A7: for X being Subset of (product (NAT --> {0,1})) holds ( X in P2 iff ex N, n being Nat st for F being Element of product (NAT --> {0,1}) holds ( F in X iff F . N = n ) ) by A5; now__::_thesis:_for_x_being_Subset_of_(product_(NAT_-->_{0,1}))_holds_ (_x_in_P1_iff_x_in_P2_) let x be Subset of (product (NAT --> {0,1})); ::_thesis: ( x in P1 iff x in P2 ) ( x in P1 iff ex N, n being Nat st for F being Element of product (NAT --> {0,1}) holds ( F in x iff F . N = n ) ) by A6; hence ( x in P1 iff x in P2 ) by A7; ::_thesis: verum end; then P1 = P2 by A2, A4, SUBSET_1:3; hence T1 = T2 by A2, A4, Th17; ::_thesis: verum end; end; :: deftheorem defines the_Cantor_set CANTOR_1:def_5_:_ for b1 being non empty strict TopSpace holds ( b1 = the_Cantor_set iff ( the carrier of b1 = product (NAT --> {0,1}) & ex P being prebasis of b1 st for X being Subset of (product (NAT --> {0,1})) holds ( X in P iff ex N, n being Nat st for F being Element of product (NAT --> {0,1}) holds ( F in X iff F . N = n ) ) ) );