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; :: according to PRE_TOPC:def 1 :: thesis: ( ( 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 :: thesis: 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); :: thesis: ( 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
proof
let x be object ; :: 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 ; :: 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 A5, PRE_TOPC:def 1;
then A6: union ua is open ;
assume A7: a c= the topology of (One-Point_Compactification X) ; :: thesis: union b1 in the topology of (One-Point_Compactification X)
A8: 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 object ; :: 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
A9: x in A and
A10: A in ua by TARSKI:def 4;
consider U being Subset of X such that
A11: A = U and
U is open and
A12: ( U in a or U \/ {([#] X)} in a ) by A10;
now :: thesis: not x in {([#] X)}
assume x in {([#] X)} ; :: thesis: contradiction
then A15: x = [#] X by TARSKI:def 1;
A: x in [#] X by A9, A11;
reconsider xx = x as set by TARSKI:1;
not xx in xx ;
hence contradiction by A, A15; :: thesis: verum
end;
hence x in (union a) \ {([#] X)} by A13, XBOOLE_0:def 5; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (union a) \ {([#] X)} or x in union ua )
assume A16: 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
A17: x in A and
A18: 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 A2, A7, A18, XBOOLE_0:def 3;
suppose A19: A in the topology of X ; :: thesis: x in union ua
then reconsider U = A as Subset of X ;
U is open by A19;
then U in ua by A18;
hence x in union ua by A17, 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
A20: A = U \/ {([#] X)} and
A21: U is open and
U ` is compact ;
A22: U in ua by A18, A20, A21;
not x in {([#] X)} by A16, XBOOLE_0:def 5;
then x in U by A17, A20, XBOOLE_0:def 3;
hence x in union ua by A22, TARSKI:def 4; :: thesis: verum
end;
end;
end;
per cases ( [#] X in union a or not [#] X in union a ) ;
suppose A23: [#] X in union a ; :: thesis: 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 :: thesis: not [#] X in U
assume [#] X in U ; :: thesis: contradiction
then [#] X in [#] X ;
hence contradiction ; :: thesis: 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; :: thesis: verum
end;
suppose A30: not [#] X in union a ; :: thesis: union b1 in the topology of (One-Point_Compactification X)
A31: a c= the topology of X
proof
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in a or A in the topology of X )
reconsider AA = A as set by TARSKI:1;
assume A32: 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 A2, A7, A32, XBOOLE_0:def 3;
then A33: ex U being Subset of X st
( A = U \/ {([#] X)} & U is open & U ` is compact ) ;
[#] X in {([#] X)} by TARSKI:def 1;
then [#] X in AA by A33, XBOOLE_0:def 3;
hence contradiction by A30, A32, 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 A31, PRE_TOPC:def 1;
hence union a in the topology of (One-Point_Compactification X) by A2, 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 A34: 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 A35: 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 A2, A34, A35, XBOOLE_0:def 3;
suppose that A36: a in the topology of X and
A37: 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)
reconsider a9 = a as Subset of X by A36;
not [#] X in a9 by A1;
then {([#] X)} misses a9 by ZFMISC_1:50;
then a9 /\ {([#] X)} = {} X ;
then reconsider aX = a9 /\ {([#] X)} as open Subset of X ;
consider U being Subset of X such that
A38: b = U \/ {([#] X)} and
A39: U is open and
U ` is compact by A37;
a9 is open by A36;
then reconsider aXU = a9 /\ U as open Subset of X by A39;
a /\ b = aXU \/ aX by A38, XBOOLE_1:23;
then a /\ b in the topology of X by PRE_TOPC:def 2;
hence a /\ b in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def 3; :: thesis: verum
end;
suppose that A40: b in the topology of X and
A41: 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)
reconsider b9 = b as Subset of X by A40;
not [#] X in b9 by A1;
then {([#] X)} misses b9 by ZFMISC_1:50;
then b9 /\ {([#] X)} = {} X ;
then reconsider bX = b9 /\ {([#] X)} as open Subset of X ;
consider U being Subset of X such that
A42: a = U \/ {([#] X)} and
A43: U is open and
U ` is compact by A41;
b9 is open by A40;
then reconsider bXUa = b9 /\ U as open Subset of X by A43;
a /\ b = bXUa \/ bX by A42, XBOOLE_1:23;
then a /\ b in the topology of X by PRE_TOPC:def 2;
hence a /\ b in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def 3; :: thesis: verum
end;
suppose that A44: a in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } and
A45: 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
A46: a = Ua \/ {([#] X)} and
A47: Ua is open and
A48: Ua ` is compact by A44;
consider Ub being Subset of X such that
A49: b = Ub \/ {([#] X)} and
A50: Ub is open and
A51: Ub ` is compact by A45;
(Ua `) \/ (Ub `) is compact by A48, A51, COMPTS_1:10;
then A52: (Ua /\ Ub) ` is compact by XBOOLE_1:54;
a /\ b = (Ua /\ Ub) \/ {([#] X)} by A46, A49, XBOOLE_1:24;
then a /\ b in { (U \/ {([#] X)}) where U is Subset of X : ( U is open & U ` is compact ) } by A47, A50, A52;
hence a /\ b in the topology of (One-Point_Compactification X) by A2, XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
hence One-Point_Compactification X is TopSpace-like ; :: thesis: verum