set Y = One-Point_Compactification X;
set T = succ ([#] X);
set D = { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;
A1:
not [#] X in [#] X
;
A2:
the topology of (One-Point_Compactification X) = the topology of X \/ { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) }
by Def9;
A3:
[#] (One-Point_Compactification X) = succ ([#] X)
by Def9;
One-Point_Compactification X is TopSpace-like
proof
([#] X) ` =
(({} X) `) `
.=
{} X
;
then
succ ([#] X) in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) }
;
hence
the
carrier of
(One-Point_Compactification X) in the
topology of
(One-Point_Compactification X)
by A3, A2, XBOOLE_0:def 3;
PRE_TOPC:def 1 ( ( for b1 being Element of K19(K19( the carrier of (One-Point_Compactification X))) holds
( not b1 c= the topology of (One-Point_Compactification X) or union b1 in the topology of (One-Point_Compactification X) ) ) & ( for b1, b2 being Element of K19( the carrier of (One-Point_Compactification X)) holds
( not b1 in the topology of (One-Point_Compactification X) or not b2 in the topology of (One-Point_Compactification X) or b1 /\ b2 in the topology of (One-Point_Compactification X) ) ) )
hereby for b1, b2 being Element of K19( the carrier of (One-Point_Compactification X)) holds
( not b1 in the topology of (One-Point_Compactification X) or not b2 in the topology of (One-Point_Compactification X) or b1 /\ b2 in the topology of (One-Point_Compactification X) )
let a be
Subset-Family of
(One-Point_Compactification X);
( a c= the topology of (One-Point_Compactification X) implies union b1 in the topology of (One-Point_Compactification X) )A4:
not
[#] X in [#] X
;
set ua =
{ U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) ) } ;
A5:
{ U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) ) } c= the
topology of
X
then reconsider ua =
{ U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) ) } as
Subset-Family of
X by XBOOLE_1:1;
union ua in the
topology of
X
by A5, PRE_TOPC:def 1;
then A6:
union ua is
open
;
assume A7:
a c= the
topology of
(One-Point_Compactification X)
;
union b1 in the topology of (One-Point_Compactification X)A8:
union ua = (union a) \ {([#] X)}
per cases
( [#] X in union a or not [#] X in union a )
;
suppose A23:
[#] X in union a
;
union b1 in the topology of (One-Point_Compactification X)then consider A being
set such that A24:
[#] X in A
and A25:
A in a
by TARSKI:def 4;
(
A in the
topology of
X or
A in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } )
by A2, A7, A25, XBOOLE_0:def 3;
then consider U being
Subset of
X such that A26:
A = U \/ {([#] X)}
and
U is
open
and A27:
U ` is
compact
by A4, A24;
A28:
now not [#] X in Uassume
[#] X in U
;
contradictionthen
[#] X in [#] X
;
hence
contradiction
;
verum end; A \ {([#] X)} =
U \ {([#] X)}
by A26, XBOOLE_1:40
.=
U
by A28, ZFMISC_1:57
;
then
U c= union ua
by A8, A25, XBOOLE_1:33, ZFMISC_1:74;
then A29:
(union ua) ` is
compact
by A6, A27, COMPTS_1:9, XBOOLE_1:34;
(union ua) \/ {([#] X)} =
(union a) \/ {([#] X)}
by A8, XBOOLE_1:39
.=
union a
by A23, ZFMISC_1:40
;
then
union a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) }
by A6, A29;
hence
union a in the
topology of
(One-Point_Compactification X)
by A2, XBOOLE_0:def 3;
verum end; end;
end;
let a,
b be
Subset of
(One-Point_Compactification X);
( not a in the topology of (One-Point_Compactification X) or not b in the topology of (One-Point_Compactification X) or a /\ b in the topology of (One-Point_Compactification X) )
assume A34:
a in the
topology of
(One-Point_Compactification X)
;
( not b in the topology of (One-Point_Compactification X) or a /\ b in the topology of (One-Point_Compactification X) )
assume A35:
b in the
topology of
(One-Point_Compactification X)
;
a /\ b in the topology of (One-Point_Compactification X)
end;
hence
One-Point_Compactification X is TopSpace-like
; verum