:: CANTOR_1 semantic presentation

registration

let c₁ be set ;
let c₂ be non empty set ;
cluster a₁ --> a₂ -> non-empty ;
coherence ;

end;

definition

let c₁ be set ;
let c₂ be Subset-Family of c₁;
func UniCl c₂ -> Subset-Family of a₁ means :E1: :: CANTOR_1:def 1
for b₁ being Subset of a₁ holds
( b₁ in a₃ iff ex b₂ being Subset-Family of a₁ st
( b₂ c= a₂ & b₁ = union b₂ ) );
existence

proof

defpred S₁[ set ] means ex b₁ being Subset-Family of c₁ st
( b₁ c= c₂ & a₁ = union b₁ );
ex b₁ being Subset-Family of c₁ st
for b₂ being Subset of c₁ holds
( b₂ in b₁ iff S₁[b₂] ) from SUBSET_1:sch 3();
hence ex b₁ being Subset-Family of c₁ st
for b₂ being Subset of c₁ holds
( b₂ in b₁ iff ex b₃ being Subset-Family of c₁ st
( b₃ c= c₂ & b₂ = union b₃ ) ) ;

end;

uniqueness

proof

let c₃, c₄ be Subset-Family of c₁;
assume that
E1: for b₁ being Subset of c₁ holds
( b₁ in c₃ iff ex b₂ being Subset-Family of c₁ st
( b₂ c= c₂ & b₁ = union b₂ ) ) and
E2: for b₁ being Subset of c₁ holds
( b₁ in c₄ iff ex b₂ being Subset-Family of c₁ st
( b₂ c= c₂ & b₁ = union b₂ ) ) ;

now

let c₅ be Subset of c₁;
( c₅ in c₃ iff ex b₁ being Subset-Family of c₁ st
( b₁ c= c₂ & c₅ = union b₁ ) ) by E1;
hence ( c₅ in c₃ iff c₅ in c₄ ) by E2;

end;

hence c₃ = c₄ by SUBSET_1:8;

end;

:: deftheorem E1 defines UniCl CANTOR_1:def 1 :

definition

let c₁ be TopStruct ;
mode Basis of c₁ -> Subset-Family of a₁ means :E2: :: CANTOR_1:def 2
( a₂ c= the topology of a₁ & the topology of a₁ c= UniCl a₂ );
existence

proof

reconsider c₂ = the topology of c₁ as Subset-Family of c₁ ;
take c₂ ;
thus c₂ c= the topology of c₁ ;

now

let c₃ be Subset of c₁;
{c₃} is Subset-Family of c₁ by SUBSET_1:63;
then reconsider c₄ = {c₃} as Subset-Family of c₁ ;
assume c₃ in the topology of c₁ ;
then E2: c₄ c= c₂ by ZFMISC_1:37;
c₃ = union c₄ by ZFMISC_1:31;
hence c₃ in UniCl c₂ by E2, E1;

end;

hence the topology of c₁ c= UniCl c₂ by SUBSET_1:7;

end;

:: deftheorem E2 defines Basis CANTOR_1:def 2 :

theorem E3: :: CANTOR_1:1

for b₁ being set
for b₂ being Subset-Family of b₁ holds b₂ c= UniCl b₂

proof

let c₁ be set ;
let c₂ be Subset-Family of c₁;
let c₃ be set ; :: according to TARSKI:def 3
assume E4: c₃ in c₂ ;
then reconsider c₄ = c₃ as Subset of c₁ ;
reconsider c₅ = {c₄} as Subset-Family of c₁ by SUBSET_1:63;
reconsider c₆ = c₅ as Subset-Family of c₁ ;
( c₆ c= c₂ & c₃ = union c₆ ) by E4, ZFMISC_1:31, ZFMISC_1:37;
hence c₃ in UniCl c₂ by E1;

end;

theorem E4: :: CANTOR_1:2

for b₁ being TopStruct holds
the topology of b₁ is Basis of b₁

proof

let c₁ be TopStruct ;
the topology of c₁ c= UniCl the topology of c₁ by E3;
hence the topology of c₁ is Basis of c₁ by E2;

end;

theorem :: CANTOR_1:3

for b₁ being TopStruct holds the topology of b₁ is open

proof

let c₁ be TopStruct ;
let c₂ be Subset of c₁; :: according to TOPS_2:def 1
assume c₂ in the topology of c₁ ;
hence c₂ is open by PRE_TOPC:def 5;

end;

definition

let c₁ be set ;
let c₂ be Subset-Family of c₁;
canceled;
func FinMeetCl c₂ -> Subset-Family of a₁ means :E5: :: CANTOR_1:def 4
for b₁ being Subset of a₁ holds
( b₁ in a₃ iff ex b₂ being Subset-Family of a₁ st
( b₂ c= a₂ & b₂ is finite & b₁ = Intersect b₂ ) );
existence

proof

defpred S₁[ set ] means ex b₁ being Subset-Family of c₁ st
( b₁ c= c₂ & b₁ is finite & a₁ = Intersect b₁ );
ex b₁ being Subset-Family of c₁ st
for b₂ being Subset of c₁ holds
( b₂ in b₁ iff S₁[b₂] ) from SUBSET_1:sch 3();
hence ex b₁ being Subset-Family of c₁ st
for b₂ being Subset of c₁ holds
( b₂ in b₁ iff ex b₃ being Subset-Family of c₁ st
( b₃ c= c₂ & b₃ is finite & b₂ = Intersect b₃ ) ) ;

end;

uniqueness

proof

let c₃, c₄ be Subset-Family of c₁;
assume that
E5: for b₁ being Subset of c₁ holds
( b₁ in c₃ iff ex b₂ being Subset-Family of c₁ st
( b₂ c= c₂ & b₂ is finite & b₁ = Intersect b₂ ) ) and
E6: for b₁ being Subset of c₁ holds
( b₁ in c₄ iff ex b₂ being Subset-Family of c₁ st
( b₂ c= c₂ & b₂ is finite & b₁ = Intersect b₂ ) ) ;

now

let c₅ be Subset of c₁;
( c₅ in c₄ iff ex b₁ being Subset-Family of c₁ st
( b₁ c= c₂ & b₁ is finite & c₅ = Intersect b₁ ) ) by E6;
hence ( c₅ in c₄ iff c₅ in c₃ ) by E5;

end;

hence c₃ = c₄ by SUBSET_1:8;

end;

:: deftheorem CANTOR_1:def 3 :

:: deftheorem E5 defines FinMeetCl CANTOR_1:def 4 :

theorem E6: :: CANTOR_1:4

for b₁ being set
for b₂ being Subset-Family of b₁ holds b₂ c= FinMeetCl b₂

proof

let c₁ be set ;
let c₂ be Subset-Family of c₁;
let c₃ be set ; :: according to TARSKI:def 3
assume E7: c₃ in c₂ ;
then reconsider c₄ = c₃ as Subset of c₁ ;
reconsider c₅ = {c₄} as Subset-Family of c₁ by SUBSET_1:63;
reconsider c₆ = c₅ as Subset-Family of c₁ ;
E8: ( c₆ is finite & c₆ c= c₂ & c₃ = meet c₆ ) by E7, SETFAM_1:11, ZFMISC_1:37;
then c₃ = Intersect c₆ by SETFAM_1:def 10;
hence c₃ in FinMeetCl c₂ by E8, E5;

end;

registration

let c₁ be non empty TopSpace;
cluster the topology of a₁ -> non empty ;
coherence ;

end;

theorem E7: :: CANTOR_1:5

for b₁ being non empty TopSpace holds the topology of b₁ = FinMeetCl the topology of b₁

proof

let c₁ be non empty TopSpace;
thus the topology of c₁ c= FinMeetCl the topology of c₁ by E6; :: according to XBOOLE_0:def 10
set c₂ = the topology of c₁;
defpred S₁[ set ] means meet a₁ in the topology of c₁;
E8: S₁[ {}. the topology of c₁] by PRE_TOPC:5, SETFAM_1:2;
E9: for b₁ being Element of Fin the topology of c₁
for b₂ being Element of the topology of c₁ holds
( S₁[b₁] implies S₁[b₁ \/ {b₂}] )

proof

let c₃ be Element of Fin the topology of c₁;
let c₄ be Element of the topology of c₁;
E10: meet {c₄} = c₄ by SETFAM_1:11;
assume E11: meet c₃ in the topology of c₁ ;

per cases not ( not c₃ <> {} & not c₃ = {} ) ;

suppose c₃ <> {} ;

then meet (c₃ \/ {c₄}) = (meet c₃) /\ (meet {c₄}) by SETFAM_1:10;
hence meet (c₃ \/ {c₄}) in the topology of c₁ by E10, E11, PRE_TOPC:def 1;

end;

suppose c₃ = {} ;

hence meet (c₃ \/ {c₄}) in the topology of c₁ by E10;

end;

E10: for b₁ being Element of Fin the topology of c₁ holds
S₁[b₁] from SETWISEO:sch 4(E8, E9);

now

let c₃ be Subset of c₁;
assume c₃ in FinMeetCl the topology of c₁ ;
then consider c₄ being Subset-Family of c₁ such that
E11: ( c₄ c= the topology of c₁ & c₄ is finite & c₃ = Intersect c₄ ) by E5;
reconsider c₅ = c₄ as Subset-Family of c₁ ;

per cases not ( not c₅ <> {} & not c₅ = {} ) ;

suppose c₅ <> {} ;

then E12: c₃ = meet c₅ by E11, SETFAM_1:def 10;
c₅ in Fin the topology of c₁ by E11, FINSUB_1:def 5;
hence c₃ in the topology of c₁ by E10, E12;

end;

suppose E12: c₅ = {} ;

reconsider c₆ = {} (bool the carrier of c₁) as Subset-Family of the carrier of c₁ ;
Intersect c₆ = the carrier of c₁ by SETFAM_1:def 10;
hence c₃ in the topology of c₁ by E11, E12, PRE_TOPC:def 1;

end;

hence FinMeetCl the topology of c₁ c= the topology of c₁ by SUBSET_1:7;

end;

theorem E8: :: CANTOR_1:6

for b₁ being TopSpace holds the topology of b₁ = UniCl the topology of b₁

proof

let c₁ be TopSpace;
thus the topology of c₁ c= UniCl the topology of c₁ by E3; :: according to XBOOLE_0:def 10
let c₂ be set ; :: according to TARSKI:def 3
assume E9: c₂ in UniCl the topology of c₁ ;
then reconsider c₃ = c₂ as Subset of c₁ ;
ex b₁ being Subset-Family of c₁ st
( b₁ c= the topology of c₁ & c₃ = union b₁ ) by E9, E1;
hence c₂ in the topology of c₁ by PRE_TOPC:def 1;

end;

theorem E9: :: CANTOR_1:7

for b₁ being non empty TopSpace holds the topology of b₁ = UniCl (FinMeetCl the topology of b₁)

proof

let c₁ be non empty TopSpace;
the topology of c₁ = FinMeetCl the topology of c₁ by E7;
hence the topology of c₁ = UniCl (FinMeetCl the topology of c₁) by E8;

end;

theorem E10: :: CANTOR_1:8

for b₁ being set
for b₂ being Subset-Family of b₁ holds b₁ in FinMeetCl b₂

proof

let c₁ be set ;
let c₂ be Subset-Family of c₁;
{} is Subset-Family of c₁ by XBOOLE_1:2;
then {} is Subset-Family of c₁ ;
then consider c₃ being Subset-Family of c₁ such that
E11: c₃ = {} ;
( c₃ c= c₂ & c₃ is finite & Intersect c₃ = c₁ ) by E11, SETFAM_1:def 10, XBOOLE_1:2;
hence c₁ in FinMeetCl c₂ by E5;

end;

theorem E11: :: CANTOR_1:9

for b₁ being set
for b₂, b₃ being Subset-Family of b₁ holds
( b₂ c= b₃ implies UniCl b₂ c= UniCl b₃ )

proof

let c₁ be set ;
let c₂, c₃ be Subset-Family of c₁;
assume E12: c₂ c= c₃ ;
let c₄ be set ; :: according to TARSKI:def 3
assume E13: c₄ in UniCl c₂ ;
then reconsider c₅ = c₄ as Subset of c₁ ;
consider c₆ being Subset-Family of c₁ such that
E14: ( c₆ c= c₂ & c₅ = union c₆ ) by E13, E1;
c₆ c= c₃ by E12, E14, XBOOLE_1:1;
hence c₄ in UniCl c₃ by E14, E1;

end;

theorem :: CANTOR_1:10

canceled;

theorem :: CANTOR_1:11

canceled;

theorem E12: :: CANTOR_1:12

for b₁ being set
for b₂ being non empty Subset-Family of (bool b₁)
for b₃ being Subset-Family of b₁ holds
( b₃ = { (Intersect b₄) where B is Element of b₂ : verum } implies Intersect b₃ = Intersect (union b₂) )

proof

let c₁ be set ;
let c₂ be non empty Subset-Family of (bool c₁);
let c₃ be Subset-Family of c₁;
assume E13: c₃ = { (Intersect b₁) where B is Element of c₂ : verum } ;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10

let c₄ be set ;
assume E14: c₄ in Intersect c₃ ;
for b₁ being set holds
( b₁ in union c₂ implies c₄ in b₁ )

proof

let c₅ be set ;
assume c₅ in union c₂ ;
then consider c₆ being set such that
E15: c₅ in c₆ and
E16: c₆ in c₂ by TARSKI:def 4;
reconsider c₇ = c₆ as Subset-Family of c₁ by E16;
reconsider c₈ = c₇ as Subset-Family of c₁ ;
Intersect c₈ in c₃ by E13, E16;
then c₄ in Intersect c₈ by E14, SETFAM_1:58;
hence c₄ in c₅ by E15, SETFAM_1:58;

end;

hence c₄ in Intersect (union c₂) by E14, SETFAM_1:58;

end;

let c₄ be set ; :: according to TARSKI:def 3
assume E14: c₄ in Intersect (union c₂) ;
for b₁ being set holds
( b₁ in c₃ implies c₄ in b₁ )

proof

let c₅ be set ;
assume c₅ in c₃ ;
then consider c₆ being Element of c₂ such that
E15: c₅ = Intersect c₆ by E13;
c₆ c= union c₂ by ZFMISC_1:92;
then Intersect (union c₂) c= Intersect c₆ by SETFAM_1:59;
hence c₄ in c₅ by E14, E15;

end;

hence c₄ in Intersect c₃ by E14, SETFAM_1:58;

end;

definition

let c₁, c₂ be set ;
let c₃ be Subset-Family of c₁;
let c₄ be Function of c₂, bool c₃;
let c₅ be set ;
redefine func . as c₄ . c₅ -> Subset-Family of a₁;
coherence

proof

per cases not ( not c₅ in dom c₄ & c₅ in dom c₄ ) ;

suppose c₅ in dom c₄ ;

then ( c₄ . c₅ in rng c₄ & rng c₄ c= bool c₃ ) by FUNCT_1:def 5, RELSET_1:12;
then E13: c₄ . c₅ in bool c₃ ;
bool c₃ c= bool (bool c₁) by ZFMISC_1:79;
hence c₄ . c₅ is Subset-Family of c₁ by E13;

end;

suppose not c₅ in dom c₄ ;

then c₄ . c₅ = {} by FUNCT_1:def 4;
then c₄ . c₅ is Subset-Family of c₁ by XBOOLE_1:2;
hence c₄ . c₅ is Subset-Family of c₁ ;

end;

theorem E13: :: CANTOR_1:13

for b₁ being set
for b₂ being Subset-Family of b₁ holds FinMeetCl b₂ = FinMeetCl (FinMeetCl b₂)

proof

let c₁ be set ;
let c₂ be Subset-Family of c₁;
thus FinMeetCl c₂ c= FinMeetCl (FinMeetCl c₂) by E6; :: according to XBOOLE_0:def 10
let c₃ be set ; :: according to TARSKI:def 3
assume E14: c₃ in FinMeetCl (FinMeetCl c₂) ;
then reconsider c₄ = c₃ as Subset of c₁ ;
consider c₅ being Subset-Family of c₁ such that
E15: ( c₅ c= FinMeetCl c₂ & c₅ is finite & c₄ = Intersect c₅ ) by E14, E5;
defpred S₁[ set , set ] means ex b₁ being Subset-Family of c₁ st
( a₁ = Intersect b₁ & b₁ = a₂ & a₂ is finite );
E16: for b₁ being set holds
not ( b₁ in c₅ & ( for b₂ being set holds
not ( b₂ in bool c₂ & S₁[b₁,b₂] ) ) )

proof

let c₆ be set ;
assume E17: c₆ in c₅ ;
then reconsider c₇ = c₆ as Subset of c₁ ;
consider c₈ being Subset-Family of c₁ such that
E18: ( c₈ c= c₂ & c₈ is finite & c₇ = Intersect c₈ ) by E15, E17, E5;
take c₈ ;
thus ( c₈ in bool c₂ & S₁[c₆,c₈] ) by E18;

end;

consider c₆ being Function of c₅, bool c₂ such that
E17: for b₁ being set holds
( b₁ in c₅ implies S₁[b₁,c₆ . b₁] ) from FUNCT_2:sch 1(E16);
dom c₆ is finite by E15, FUNCT_2:def 1;
then E18: rng c₆ is finite by FINSET_1:26;
for b₁ being set holds
( b₁ in rng c₆ implies b₁ is finite )

proof

let c₇ be set ;
assume c₇ in rng c₆ ;
then consider c₈ being set such that
E19: ( c₈ in dom c₆ & c₇ = c₆ . c₈ ) by FUNCT_1:def 5;
c₈ in c₅ by E19, FUNCT_2:def 1;
then reconsider c₉ = c₈ as Subset of c₁ ;
reconsider c₁₀ = c₆ . c₉ as Subset-Family of c₁ ;
c₉ in c₅ by E19, FUNCT_2:def 1;
then S₁[c₉,c₁₀] by E17;
hence c₇ is finite by E19;

end;

then E19: union (rng c₆) is finite by E18, FINSET_1:25;
rng c₆ c= bool c₂ by RELSET_1:12;
then union (rng c₆) c= union (bool c₂) by ZFMISC_1:95;
then E20: union (rng c₆) c= c₂ by ZFMISC_1:99;
then reconsider c₇ = union (rng c₆) as Subset-Family of c₁ by XBOOLE_1:1;
reconsider c₈ = c₇ as Subset-Family of c₁ ;
set c₉ = { (Intersect b₁) where B is Subset-Family of c₁ : b₁ in rng c₆ } ;
E21: c₅ = { (Intersect b₁) where B is Subset-Family of c₁ : b₁ in rng c₆ }

proof

E22: c₅ c= { (Intersect b₁) where B is Subset-Family of c₁ : b₁ in rng c₆ }

proof

let c₁₀ be set ; :: according to TARSKI:def 3
assume E23: c₁₀ in c₅ ;
then consider c₁₁ being Subset-Family of c₁ such that
E24: ( c₁₀ = Intersect c₁₁ & c₁₁ = c₆ . c₁₀ & c₆ . c₁₀ is finite ) by E17;
c₁₀ in dom c₆ by E23, FUNCT_2:def 1;
then c₁₁ in rng c₆ by E24, FUNCT_1:def 5;
hence c₁₀ in { (Intersect b₁) where B is Subset-Family of c₁ : b₁ in rng c₆ } by E24;

end;

{ (Intersect b₁) where B is Subset-Family of c₁ : b₁ in rng c₆ } c= c₅

proof

let c₁₀ be set ; :: according to TARSKI:def 3
assume c₁₀ in { (Intersect b₁) where B is Subset-Family of c₁ : b₁ in rng c₆ } ;
then consider c₁₁ being Subset-Family of c₁ such that
E23: c₁₀ = Intersect c₁₁ and
E24: c₁₁ in rng c₆ ;
consider c₁₂ being set such that
E25: ( c₁₂ in dom c₆ & c₁₁ = c₆ . c₁₂ ) by E24, FUNCT_1:def 5;
c₁₂ in c₅ by E25, FUNCT_2:def 1;
then S₁[c₁₂,c₆ . c₁₂] by E17;
hence c₁₀ in c₅ by E23, E25, FUNCT_2:def 1;

end;

hence c₅ = { (Intersect b₁) where B is Subset-Family of c₁ : b₁ in rng c₆ } by E22, XBOOLE_0:def 10;

end;

c₃ = Intersect c₈

proof

per cases not ( not rng c₆ <> {} & not rng c₆ = {} ) ;

suppose E22: rng c₆ <> {} ;

E23: rng c₆ c= bool c₂ by RELSET_1:12;
bool c₂ c= bool (bool c₁) by ZFMISC_1:79;
then reconsider c₁₀ = rng c₆ as non empty Subset-Family of (bool c₁) by E22, E23, XBOOLE_1:1;
reconsider c₁₁ = c₁₀ as non empty Subset-Family of (bool c₁) ;
{ (Intersect b₁) where B is Subset-Family of c₁ : b₁ in rng c₆ } = { (Intersect b₁) where B is Element of c₁₁ : verum }

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10

let c₁₂ be set ;
assume c₁₂ in { (Intersect b₁) where B is Subset-Family of c₁ : b₁ in rng c₆ } ;
then ex b₁ being Subset-Family of c₁ st
( c₁₂ = Intersect b₁ & b₁ in rng c₆ ) ;
hence c₁₂ in { (Intersect b₁) where B is Element of c₁₁ : verum } ;

end;

let c₁₂ be set ; :: according to TARSKI:def 3
assume c₁₂ in { (Intersect b₁) where B is Element of c₁₁ : verum } ;
then ex b₁ being Element of c₁₁ st c₁₂ = Intersect b₁ ;
hence c₁₂ in { (Intersect b₁) where B is Subset-Family of c₁ : b₁ in rng c₆ } ;

end;

hence c₃ = Intersect c₈ by E15, E21, E12;

end;

suppose E22: rng c₆ = {} ;

c₅ = dom c₆ by FUNCT_2:def 1;
hence c₃ = Intersect c₈ by E15, E22, RELAT_1:60, RELAT_1:64, ZFMISC_1:2;

end;

hence c₃ in FinMeetCl c₂ by E19, E20, E5;

end;

theorem :: CANTOR_1:14

for b₁ being set
for b₂ being Subset-Family of b₁
for b₃, b₄ being set holds
( ( b₃ in FinMeetCl b₂ & b₄ in FinMeetCl b₂ ) implies ( b₃ /\ b₄ in FinMeetCl b₂ ) )

proof

let c₁ be set ;
let c₂ be Subset-Family of c₁;
let c₃, c₄ be set ;
assume E14: ( c₃ in FinMeetCl c₂ & c₄ in FinMeetCl c₂ ) ;
then reconsider c₅ = {c₃,c₄} as Subset-Family of c₁ by ZFMISC_1:38;
reconsider c₆ = c₅ as Subset-Family of c₁ ;
c₃ /\ c₄ = meet c₆ by SETFAM_1:12;
then E15: c₃ /\ c₄ = Intersect c₆ by SETFAM_1:def 10;
( c₆ is non empty Subset-Family of c₁ & c₆ c= FinMeetCl c₂ ) by E14, ZFMISC_1:38;
then Intersect c₆ in FinMeetCl (FinMeetCl c₂) by E5;
hence c₃ /\ c₄ in FinMeetCl c₂ by E15, E13;

end;

theorem E14: :: CANTOR_1:15

for b₁ being set
for b₂ being Subset-Family of b₁
for b₃, b₄ being set holds
( ( b₃ c= FinMeetCl b₂ & b₄ c= FinMeetCl b₂ ) implies ( INTERSECTION b₃,b₄ c= FinMeetCl b₂ ) )

proof

let c₁ be set ;
let c₂ be Subset-Family of c₁;
let c₃, c₄ be set ;
assume E15: ( c₃ c= FinMeetCl c₂ & c₄ c= FinMeetCl c₂ ) ;
let c₅ be set ; :: according to TARSKI:def 3
assume c₅ in INTERSECTION c₃,c₄ ;
then consider c₆, c₇ being set such that
E16: c₆ in c₃ and
E17: c₇ in c₄ and
E18: c₅ = c₆ /\ c₇ by SETFAM_1:def 5;
( c₆ in FinMeetCl c₂ & c₇ in FinMeetCl c₂ ) by E15, E16, E17;
then reconsider c₈ = {c₆,c₇} as Subset-Family of c₁ by ZFMISC_1:38;
reconsider c₉ = c₈ as Subset-Family of c₁ ;
c₆ /\ c₇ = meet c₉ by SETFAM_1:12;
then E19: c₆ /\ c₇ = Intersect c₉ by SETFAM_1:def 10;
( c₉ is non empty Subset-Family of c₁ & c₉ c= FinMeetCl c₂ ) by E15, E16, E17, ZFMISC_1:38;
then Intersect c₉ in FinMeetCl (FinMeetCl c₂) by E5;
hence c₅ in FinMeetCl c₂ by E18, E19, E13;

end;

theorem E15: :: CANTOR_1:16

for b₁ being set
for b₂, b₃ being Subset-Family of b₁ holds
( b₂ c= b₃ implies FinMeetCl b₂ c= FinMeetCl b₃ )

proof

let c₁ be set ;
let c₂, c₃ be Subset-Family of c₁;
assume E16: c₂ c= c₃ ;
let c₄ be set ; :: according to TARSKI:def 3
assume E17: c₄ in FinMeetCl c₂ ;
then reconsider c₅ = c₄ as Subset of c₁ ;
consider c₆ being Subset-Family of c₁ such that
E18: ( c₆ c= c₂ & c₆ is finite & c₅ = Intersect c₆ ) by E17, E5;
c₆ c= c₃ by E16, E18, XBOOLE_1:1;
hence c₄ in FinMeetCl c₃ by E18, E5;

end;

registration

let c₁ be set ;
let c₂ be Subset-Family of c₁;
cluster FinMeetCl a₂ -> non empty ;
coherence by E10;

end;

theorem E16: :: CANTOR_1:17

for b₁ being non empty set
for b₂ being Subset-Family of b₁ holds TopStruct(# b₁,(UniCl (FinMeetCl b₂)) #) is TopSpace-like

proof

let c₁ be non empty set ;
let c₂ be Subset-Family of c₁;
set c₃ = TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #);
E17: [#] TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #) in FinMeetCl c₂ by E10;

now

reconsider c₄ = {([#] TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #))} as Subset-Family of c₁ by ZFMISC_1:80;
reconsider c₅ = c₄ as Subset-Family of c₁ ;
take c₆ = c₅;
thus c₆ c= FinMeetCl c₂ by E17, ZFMISC_1:37;
thus [#] TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #) = union c₆ by ZFMISC_1:31;

end;

hence the carrier of TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #) in the topology of TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #) by E1; :: according to PRE_TOPC:def 1
thus for b₁ being Subset-Family of TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #) holds
( b₁ c= the topology of TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #) implies union b₁ in the topology of TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #) )

proof

let c₄ be Subset-Family of TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #);
assume E18: c₄ c= the topology of TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #) ;
defpred S₁[ set ] means ex b₁ being Subset of TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #) st
( b₁ in c₄ & b₁ = union a₁ );
consider c₅ being Subset-Family of (FinMeetCl c₂) such that
E19: for b₁ being Subset of (FinMeetCl c₂) holds
( b₁ in c₅ iff S₁[b₁] ) from SUBSET_1:sch 3();
E20: union (union c₅) = union { (union b₁) where B is Subset of (FinMeetCl c₂) : b₁ in c₅ } by BORSUK_1:17;
E21: c₄ = { (union b₁) where B is Subset of (FinMeetCl c₂) : b₁ in c₅ }

proof

set c₆ = { (union b₁) where B is Subset of (FinMeetCl c₂) : b₁ in c₅ } ;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10

let c₇ be set ;
assume E22: c₇ in c₄ ;
then reconsider c₈ = c₇ as Subset of c₁ ;
consider c₉ being Subset-Family of c₁ such that
E23: c₉ c= FinMeetCl c₂ and
E24: c₈ = union c₉ by E18, E22, E1;
c₉ in c₅ by E19, E22, E23, E24;
hence c₇ in { (union b₁) where B is Subset of (FinMeetCl c₂) : b₁ in c₅ } by E24;

end;

let c₇ be set ; :: according to TARSKI:def 3
assume c₇ in { (union b₁) where B is Subset of (FinMeetCl c₂) : b₁ in c₅ } ;
then consider c₈ being Subset of (FinMeetCl c₂) such that
E22: c₇ = union c₈ and
E23: c₈ in c₅ ;
consider c₉ being Subset of TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #) such that
E24: c₉ in c₄ and
E25: c₉ = union c₈ by E19, E23;
thus c₇ in c₄ by E22, E24, E25;

end;

union c₅ c= bool c₁ by XBOOLE_1:1;
then union c₅ is Subset-Family of TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #) ;
hence union c₄ in the topology of TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #) by E20, E21, E1;

end;

let c₄, c₅ be Subset of TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #);
assume c₄ in the topology of TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #) ;
then consider c₆ being Subset-Family of c₁ such that
E18: c₆ c= FinMeetCl c₂ and
E19: c₄ = union c₆ by E1;
assume c₅ in the topology of TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #) ;
then consider c₇ being Subset-Family of c₁ such that
E20: c₇ c= FinMeetCl c₂ and
E21: c₅ = union c₇ by E1;
E22: INTERSECTION c₆,c₇ c= FinMeetCl c₂ by E18, E20, E14;
then INTERSECTION c₆,c₇ is Subset-Family of c₁ by XBOOLE_1:1;
then E23: INTERSECTION c₆,c₇ is Subset-Family of c₁ ;
union (INTERSECTION c₆,c₇) = c₄ /\ c₅ by E19, E21, SETFAM_1:39;
hence c₄ /\ c₅ in the topology of TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #) by E22, E23, E1;

end;

definition

let c₁ be TopStruct ;
mode prebasis of c₁ -> Subset-Family of a₁ means :E17: :: CANTOR_1:def 5
( a₂ c= the topology of a₁ & ex b₁ being Basis of a₁ st b₁ c= FinMeetCl a₂ );
existence

proof

reconsider c₂ = the topology of c₁ as Subset-Family of c₁ ;
take c₂ ;
thus c₂ c= the topology of c₁ ;
reconsider c₃ = the topology of c₁ as Basis of c₁ by E4;
take c₃ ;
thus c₃ c= FinMeetCl c₂ by E6;

end;

:: deftheorem E17 defines prebasis CANTOR_1:def 5 :

theorem E18: :: CANTOR_1:18

for b₁ being non empty set
for b₂ being Subset-Family of b₁ holds
b₂ is Basis of TopStruct(# b₁,(UniCl b₂) #)

proof

let c₁ be non empty set ;
let c₂ be Subset-Family of c₁;
c₂ c= UniCl c₂ by E3;
hence c₂ is Basis of TopStruct(# c₁,(UniCl c₂) #) by E2;

end;

theorem E19: :: CANTOR_1:19

for b₁, b₂ being non empty strict TopSpace
for b₃ being prebasis of b₁ holds
( ( the carrier of b₁ = the carrier of b₂ & b₃ is prebasis of b₂ ) implies ( b₁ = b₂ ) )

proof

let c₁, c₂ be non empty strict TopSpace;
let c₃ be prebasis of c₁;
assume that
E20: the carrier of c₁ = the carrier of c₂ and
E21: c₃ is prebasis of c₂ ;
consider c₄ being Basis of c₁ such that
E22: c₄ c= FinMeetCl c₃ by E17;
E23: the topology of c₁ c= UniCl c₄ by E2;
UniCl c₄ c= UniCl (FinMeetCl c₃) by E22, E11;
then E24: the topology of c₁ c= UniCl (FinMeetCl c₃) by E23, XBOOLE_1:1;
reconsider c₅ = c₃ as prebasis of c₂ by E21;
consider c₆ being Basis of c₂ such that
E25: c₆ c= FinMeetCl c₅ by E17;
E26: the topology of c₂ c= UniCl c₆ by E2;
E27: the topology of c₂ = UniCl (FinMeetCl the topology of c₂) by E9;
E28: the topology of c₁ = UniCl (FinMeetCl the topology of c₁) by E9;
UniCl c₆ c= UniCl (FinMeetCl c₅) by E25, E11;
then E29: the topology of c₂ c= UniCl (FinMeetCl c₅) by E26, XBOOLE_1:1;
c₅ c= the topology of c₂ by E17;
then FinMeetCl c₅ c= FinMeetCl the topology of c₂ by E15;
then UniCl (FinMeetCl c₅) c= UniCl (FinMeetCl the topology of c₂) by E11;
then E30: UniCl (FinMeetCl c₅) = the topology of c₂ by E27, E29, XBOOLE_0:def 10;
c₃ c= the topology of c₁ by E17;
then FinMeetCl c₃ c= FinMeetCl the topology of c₁ by E15;
then UniCl (FinMeetCl c₃) c= UniCl (FinMeetCl the topology of c₁) by E11;
hence c₁ = c₂ by E20, E24, E28, E30, XBOOLE_0:def 10;

end;

theorem E20: :: CANTOR_1:20

for b₁ being non empty set
for b₂ being Subset-Family of b₁ holds
b₂ is prebasis of TopStruct(# b₁,(UniCl (FinMeetCl b₂)) #)

proof

let c₁ be non empty set ;
let c₂ be Subset-Family of c₁;
set c₃ = TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #);
reconsider c₄ = c₂ as Subset-Family of TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #) ;
c₄ is prebasis of TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #)

proof

( c₄ c= FinMeetCl c₂ & FinMeetCl c₂ c= the topology of TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #) ) by E3, E6;
hence c₄ c= the topology of TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #) by XBOOLE_1:1; :: according to CANTOR_1:def 5
reconsider c₅ = FinMeetCl c₄ as Basis of TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #) by E18;
take c₅ ;
thus c₅ c= FinMeetCl c₄ ;

end;

hence c₂ is prebasis of TopStruct(# c₁,(UniCl (FinMeetCl c₂)) #) ;

end;

definition

func the_Cantor_set -> non empty strict TopSpace means :: CANTOR_1:def 6
( the carrier of a₁ = product (NAT --> {0,1}) & ex b₁ being prebasis of a₁ st
for b₂ being Subset of (product (NAT --> {0,1})) holds
( b₂ in b₁ iff ex b₃, b₄ being Nat st
for b₅ being Element of product (NAT --> {0,1}) holds
( b₅ in b₂ iff b₅ . b₃ = b₄ ) ) );
existence

proof

defpred S₁[ set ] means ex b₁, b₂ being Nat st
for b₃ being Element of product (NAT --> {0,1}) holds
( b₃ in a₁ iff b₃ . b₁ = b₂ );
consider c₁ being Subset-Family of (product (NAT --> {0,1})) such that
E21: for b₁ being Subset of (product (NAT --> {0,1})) holds
( b₁ in c₁ iff S₁[b₁] ) from SUBSET_1:sch 3();
reconsider c₂ = TopStruct(# (product (NAT --> {0,1})),(UniCl (FinMeetCl c₁)) #) as non empty strict TopSpace by E16;
take c₂ ;
thus the carrier of c₂ = product (NAT --> {0,1}) ;
reconsider c₃ = c₁ as prebasis of c₂ by E20;
take c₃ ;
thus for b₁ being Subset of (product (NAT --> {0,1})) holds
( b₁ in c₃ iff ex b₂, b₃ being Nat st
for b₄ being Element of product (NAT --> {0,1}) holds
( b₄ in b₁ iff b₄ . b₂ = b₃ ) ) by E21;

end;

uniqueness

proof

let c₁, c₂ be non empty strict TopSpace;
assume that
E21: ( the carrier of c₁ = product (NAT --> {0,1}) & ex b₁ being prebasis of c₁ st
for b₂ being Subset of (product (NAT --> {0,1}))