A1: not [#] X in [#] X ;
set T = succ ([#] X);
set D = { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ;
A2: [#] (One-Point_Compactification X) = succ ([#] X) by Def9;
A3: 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;
set Y = One-Point_Compactification X;
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 A2, A3, XBOOLE_0:def 3; :: according to PRE_TOPC:def 1 :: thesis: ( ( for b1 being Element of bool (bool 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 bool 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 :: thesis: for b1, b2 being Element of bool 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); :: thesis: ( a c= the topology of (One-Point_Compactification X) implies union b1 in the topology of (One-Point_Compactification X) )
assume A4: a c= the topology of (One-Point_Compactification X) ; :: thesis: union b1 in the topology of (One-Point_Compactification X)
A5: not [#] X in [#] X ;
set ua = { U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) ) } ;
A6: { U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) ) } c= the topology of X
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) ) } or x in the topology of X )
assume x in { U where U is Subset of X : ( U is open & ( U in a or U \/ {([#] X)} in a ) ) } ; :: thesis: x in the topology of X
then ex U being Subset of X st
( x = U & U is open & ( U in a or U \/ {([#] X)} in a ) ) ;
hence x in the topology of X by PRE_TOPC:def 5; :: thesis: verum
end;
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 A6, PRE_TOPC:def 1;
then A7: union ua is open by PRE_TOPC:def 5;
A9: union ua = (union a) \ {([#] X)}
proof
thus union ua c= (union a) \ {([#] X)} :: according to XBOOLE_0:def 10 :: thesis: (union a) \ {([#] X)} c= union ua
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union ua or x in (union a) \ {([#] X)} )
assume x in union ua ; :: thesis: x in (union a) \ {([#] X)}
then consider A being set such that
A10: x in A and
A11: A in ua by TARSKI:def 4;
consider U being Subset of X such that
A12: A = U and
U is open and
A13: ( U in a or U \/ {([#] X)} in a ) by A11;
A14: now
assume x in {([#] X)} ; :: thesis: contradiction
then A15: x = [#] X by TARSKI:def 1;
x in [#] X by A10, A12;
hence contradiction by A15; :: thesis: verum
end;
hence x in (union a) \ {([#] X)} by A14, XBOOLE_0:def 5; :: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (union a) \ {([#] X)} or x in union ua )
assume A17: x in (union a) \ {([#] X)} ; :: thesis: x in union ua
then x in union a by XBOOLE_0:def 5;
then consider A being set such that
A18: x in A and
A19: A in a by TARSKI:def 4;
per cases ( A in the topology of X or A in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) by A3, A4, A19, XBOOLE_0:def 3;
suppose A20: A in the topology of X ; :: thesis: x in union ua
then reconsider U = A as Subset of X ;
U is open by A20, PRE_TOPC:def 5;
then U in ua by A19;
hence x in union ua by A18, TARSKI:def 4; :: thesis: verum
end;
suppose A in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; :: thesis: x in union ua
then consider U being Subset of X such that
A21: A = U \/ {([#] X)} and
A22: U is open and
U ` is compact ;
not x in {([#] X)} by A17, XBOOLE_0:def 5;
then A23: x in U by A18, A21, XBOOLE_0:def 3;
U in ua by A19, A21, A22;
hence x in union ua by A23, TARSKI:def 4; :: thesis: verum
end;
end;
end;
per cases ( [#] X in union a or not [#] X in union a ) ;
suppose A24: [#] X in union a ; :: thesis: union b1 in the topology of (One-Point_Compactification X)
then consider A being set such that
A25: [#] X in A and
A26: 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 A3, A4, A26, XBOOLE_0:def 3;
then consider U being Subset of X such that
A27: A = U \/ {([#] X)} and
U is open and
A28: U ` is compact by A5, A25;
A29: now
assume [#] X in U ; :: thesis: contradiction
then [#] X in [#] X ;
hence contradiction ; :: thesis: verum
end;
A \ {([#] X)} = U \ {([#] X)} by A27, XBOOLE_1:40
.= U by A29, ZFMISC_1:65 ;
then U c= union ua by A9, A26, XBOOLE_1:33, ZFMISC_1:92;
then A30: (union ua) ` is compact by A7, A28, COMPTS_1:18, XBOOLE_1:34;
(union ua) \/ {([#] X)} = (union a) \/ {([#] X)} by A9, XBOOLE_1:39
.= union a by A24, ZFMISC_1:46 ;
then union a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A7, A30;
hence union a in the topology of (One-Point_Compactification X) by A3, XBOOLE_0:def 3; :: thesis: verum
end;
suppose A31: not [#] X in union a ; :: thesis: union b1 in the topology of (One-Point_Compactification X)
A32: a c= the topology of X
proof
let A be set ; :: according to TARSKI:def 3 :: thesis: ( not A in a or A in the topology of X )
assume A33: A in a ; :: thesis: A in the topology of X
assume not A in the topology of X ; :: thesis: contradiction
then A in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A3, A4, A33, XBOOLE_0:def 3;
then consider U being Subset of X such that
A34: A = U \/ {([#] X)} and
U is open and
U ` is compact ;
[#] X in {([#] X)} by TARSKI:def 1;
then [#] X in A by A34, XBOOLE_0:def 3;
hence contradiction by A31, A33, TARSKI:def 4; :: thesis: verum
end;
then a is Subset-Family of ([#] X) by XBOOLE_1:1;
then union a in the topology of X by A32, PRE_TOPC:def 1;
hence union a in the topology of (One-Point_Compactification X) by A3, XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
let a, b be Subset of (One-Point_Compactification X); :: thesis: ( 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 A35: a in the topology of (One-Point_Compactification X) ; :: thesis: ( not b in the topology of (One-Point_Compactification X) or a /\ b in the topology of (One-Point_Compactification X) )
assume A36: b in the topology of (One-Point_Compactification X) ; :: thesis: a /\ b in the topology of (One-Point_Compactification X)
per cases ( ( a in the topology of X & b in the topology of X ) or ( a in the topology of X & b in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) or ( b in the topology of X & a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) or ( a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } & b in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ) ) by A3, A35, A36, XBOOLE_0:def 3;
suppose that A37: a in the topology of X and
A38: b in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; :: thesis: a /\ b in the topology of (One-Point_Compactification X)
consider U being Subset of X such that
A39: b = U \/ {([#] X)} and
A40: U is open and
U ` is compact by A38;
reconsider a' = a as Subset of X by A37;
a' is open by A37, PRE_TOPC:def 5;
then reconsider aXU = a' /\ U as open Subset of X by A40, TOPS_1:38;
not [#] X in a' by A1;
then {([#] X)} misses a' by ZFMISC_1:56;
then a' /\ {([#] X)} = {} X by XBOOLE_0:def 7;
then reconsider aX = a' /\ {([#] X)} as open Subset of X ;
A41: aXU \/ aX is open by TOPS_1:37;
a /\ b = aXU \/ aX by A39, XBOOLE_1:23;
then a /\ b in the topology of X by A41, PRE_TOPC:def 5;
hence a /\ b in the topology of (One-Point_Compactification X) by A3, XBOOLE_0:def 3; :: thesis: verum
end;
suppose that A42: b in the topology of X and
A43: a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; :: thesis: a /\ b in the topology of (One-Point_Compactification X)
consider U being Subset of X such that
A44: a = U \/ {([#] X)} and
A45: U is open and
U ` is compact by A43;
reconsider b' = b as Subset of X by A42;
b' is open by A42, PRE_TOPC:def 5;
then reconsider bXUa = b' /\ U as open Subset of X by A45, TOPS_1:38;
not [#] X in b' by A1;
then {([#] X)} misses b' by ZFMISC_1:56;
then b' /\ {([#] X)} = {} X by XBOOLE_0:def 7;
then reconsider bX = b' /\ {([#] X)} as open Subset of X ;
A46: bXUa \/ bX is open by TOPS_1:37;
a /\ b = bXUa \/ bX by A44, XBOOLE_1:23;
then a /\ b in the topology of X by A46, PRE_TOPC:def 5;
hence a /\ b in the topology of (One-Point_Compactification X) by A3, XBOOLE_0:def 3; :: thesis: verum
end;
suppose that A47: a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } and
A48: b in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } ; :: thesis: a /\ b in the topology of (One-Point_Compactification X)
consider Ua being Subset of X such that
A49: a = Ua \/ {([#] X)} and
A50: Ua is open and
A51: Ua ` is compact by A47;
consider Ub being Subset of X such that
A52: b = Ub \/ {([#] X)} and
A53: Ub is open and
A54: Ub ` is compact by A48;
A55: a /\ b = (Ua /\ Ub) \/ {([#] X)} by A49, A52, XBOOLE_1:24;
A56: Ua /\ Ub is open by A50, A53, TOPS_1:38;
(Ua ` ) \/ (Ub ` ) is compact by A51, A54, COMPTS_1:19;
then (Ua /\ Ub) ` is compact by XBOOLE_1:54;
then a /\ b in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A55, A56;
hence a /\ b in the topology of (One-Point_Compactification X) by A3, XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
hence One-Point_Compactification X is TopSpace-like ; :: thesis: verum