:: REALSET1 semantic presentation

begin

theorem Th1: :: REALSET1:1
for X, x being set
for F being Function of [:X,X:],X st x in [:X,X:] holds
F . x in X
proof
let X, x be set ; ::_thesis: for F being Function of [:X,X:],X st x in [:X,X:] holds
F . x in X
let F be Function of [:X,X:],X; ::_thesis: ( x in [:X,X:] implies F . x in X )
 ( X = {} implies [:X,X:] = {} ) ;
then A1: dom F = [:X,X:] by FUNCT_2:def_1;
assume  x in [:X,X:] ; ::_thesis: F . x in X
then  ( rng F c= X & F . x in rng F ) by A1, FUNCT_1:def_3, RELAT_1:def_19;
hence  F . x in X ; ::_thesis: verum
end;

definition
let X be set ;
let F be BinOp of X;
mode Preserv of F ->  Subset of X means :Def1: :: REALSET1:def 1
 for x being set st x in [:it,it:] holds
F . x in it;
existence
 ex b1 being Subset of X st
for x being set st x in [:b1,b1:] holds
F . x in b1
proof
 X c= X ;
then reconsider Z = X as Subset of X ;
take  Z ; ::_thesis: for x being set st x in [:Z,Z:] holds
F . x in Z
thus  for x being set st x in [:Z,Z:] holds
F . x in Z by Th1; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Preserv REALSET1:def_1_:_
 for X being set
for F being BinOp of X
for b3 being Subset of X holds
( b3 is Preserv of F iff for x being set st x in [:b3,b3:] holds
F . x in b3 );

definition
let R be Relation;
let A be set ;
funcR || A ->  set  equals :: REALSET1:def 2
R | [:A,A:];
coherence
 R | [:A,A:] is set ;
end;

:: deftheorem  defines || REALSET1:def_2_:_
 for R being Relation
for A being set holds R || A = R | [:A,A:];

registration
let R be Relation;
let A be set ;
clusterR || A ->  Relation-like ;
coherence
 R || A is Relation-like ;
end;

registration
let R be Function;
let A be set ;
clusterR || A ->  Function-like ;
coherence
 R || A is Function-like ;
end;

theorem Th2: :: REALSET1:2
for X being set
for F being BinOp of X
for A being Preserv of F holds F || A is BinOp of A
proof
let X be set ; ::_thesis: for F being BinOp of X
for A being Preserv of F holds F || A is BinOp of A
let F be BinOp of X; ::_thesis: for A being Preserv of F holds F || A is BinOp of A
let A be Preserv of F; ::_thesis: F || A is BinOp of A
 ( X = {} implies [:X,X:] = {} ) ;
then  dom F = [:X,X:] by FUNCT_2:def_1;
then A1: dom (F || A) = [:A,A:] by RELAT_1:62, ZFMISC_1:96;
 for x being set st x in [:A,A:] holds
(F || A) . x in A
proof
let x be set ; ::_thesis: ( x in [:A,A:] implies (F || A) . x in A )
assume A2: x in [:A,A:] ; ::_thesis: (F || A) . x in A
then  (F || A) . x = F . x by A1, FUNCT_1:47;
hence  (F || A) . x in A by A2, Def1; ::_thesis: verum
end;
hence  F || A is BinOp of A by A1, FUNCT_2:3; ::_thesis: verum
end;

definition
let X be set ;
let F be BinOp of X;
let A be Preserv of F;
:: original: ||
redefine funcF || A ->  BinOp of A;
coherence
 F || A is BinOp of A by Th2;
end;

theorem Th3: :: REALSET1:3
for X being set holds
( not X is trivial iff for x being set holds X \ {x} is non empty set )
proof
let X be set ; ::_thesis: ( not X is trivial iff for x being set holds X \ {x} is non empty set )
hereby  ::_thesis: ( ( for x being set holds X \ {x} is non empty set ) implies not X is trivial )
assume A1: not X is trivial ; ::_thesis: for x being set holds X \ {x} is non empty set
let x be set ; ::_thesis: X \ {x} is non empty set
 X <> {x} by A1;
then consider y being set  such that
A2: y in X and
A3: x <> y by A1, ZFMISC_1:35;
 not y in {x} by A3, TARSKI:def_1;
hence  X \ {x} is non empty set by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A4: for x being set holds X \ {x} is non empty set ; ::_thesis: not X is trivial
 X \ {{}} c= X ;
then  not X is empty by A4;
then consider x being set  such that
A5: x in X by XBOOLE_0:def_1;
 not X \ {x} is empty by A4;
then consider y being set  such that
A6: y in X \ {x} by XBOOLE_0:def_1;
take  x ; :: according to ZFMISC_1:def_10 ::_thesis: ex b1 being set st
( x in X & b1 in X & not x = b1 )
take  y ; ::_thesis: ( x in X & y in X & not x = y )
thus  x in X by A5; ::_thesis: ( y in X & not x = y )
thus  y in X by A6; ::_thesis: not x = y
 x in {x} by TARSKI:def_1;
then  not x in X \ {x} by XBOOLE_0:def_5;
hence  x <> y by A6; ::_thesis: verum
end;

theorem :: REALSET1:4
ex A being non empty set st
for z being Element of A holds A \ {z} is non empty set
proof
set B = {0,1};
take  {0,1} ; ::_thesis: for z being Element of {0,1} holds {0,1} \ {z} is non empty set
 for z being Element of {0,1} holds {0,1} \ {z} is non empty set
proof
let z be Element of {0,1}; ::_thesis: {0,1} \ {z} is non empty set
 ( 0 in {0,1} & not 0 in {1} ) by TARSKI:def_1, TARSKI:def_2;
then A1: {0,1} \ {1} is non empty set by XBOOLE_0:def_5;
 ( 1 in {0,1} & not 1 in {0} ) by TARSKI:def_1, TARSKI:def_2;
then  {0,1} \ {0} is non empty set by XBOOLE_0:def_5;
hence  {0,1} \ {z} is non empty set by A1, TARSKI:def_2; ::_thesis: verum
end;
hence  for z being Element of {0,1} holds {0,1} \ {z} is non empty set ; ::_thesis: verum
end;

definition
let X be non trivial set ;
let F be BinOp of X;
let x be Element of X;
predF is_Bin_Op_Preserv x means :: REALSET1:def 3
( X \ {x} is Preserv of F & (F || X) \ {x} is BinOp of (X \ {x}) );
correctness
;
end;

:: deftheorem  defines is_Bin_Op_Preserv REALSET1:def_3_:_
 for X being non trivial set
for F being BinOp of X
for x being Element of X holds
( F is_Bin_Op_Preserv x iff ( X \ {x} is Preserv of F & (F || X) \ {x} is BinOp of (X \ {x}) ) );

theorem Th5: :: REALSET1:5
for X being set
for A being Subset of X ex F being BinOp of X st
for x being set st x in [:A,A:] holds
F . x in A
proof
let X be set ; ::_thesis: for A being Subset of X ex F being BinOp of X st
for x being set st x in [:A,A:] holds
F . x in A
let A be Subset of X; ::_thesis: ex F being BinOp of X st
for x being set st x in [:A,A:] holds
F . x in A
set S = pr1 (X,X);
take  pr1 (X,X) ; ::_thesis: for x being set st x in [:A,A:] holds
(pr1 (X,X)) . x in A
 for x being set st x in [:A,A:] holds
(pr1 (X,X)) . x in A
proof
let x be set ; ::_thesis: ( x in [:A,A:] implies (pr1 (X,X)) . x in A )
assume  x in [:A,A:] ; ::_thesis: (pr1 (X,X)) . x in A
then consider p, q being set  such that
A1: ( p in A & q in A ) and
A2: x = [p,q] by ZFMISC_1:def_2;
 (pr1 (X,X)) . x = (pr1 (X,X)) . (p,q) by A2;
hence  (pr1 (X,X)) . x in A by A1, FUNCT_3:def_4; ::_thesis: verum
end;
hence  for x being set st x in [:A,A:] holds
(pr1 (X,X)) . x in A ; ::_thesis: verum
end;

definition
let X be set ;
let A be Subset of X;
mode Presv of X,A ->  BinOp of X means :Def4: :: REALSET1:def 4
 for x being set st x in [:A,A:] holds
it . x in A;
existence
 ex b1 being BinOp of X st
for x being set st x in [:A,A:] holds
b1 . x in A by Th5;
end;

:: deftheorem Def4 defines Presv REALSET1:def_4_:_
 for X being set
for A being Subset of X
for b3 being BinOp of X holds
( b3 is Presv of X,A iff for x being set st x in [:A,A:] holds
b3 . x in A );

theorem Th6: :: REALSET1:6
for X being set
for A being Subset of X
for F being Presv of X,A holds F || A is BinOp of A
proof
let X be set ; ::_thesis: for A being Subset of X
for F being Presv of X,A holds F || A is BinOp of A
let A be Subset of X; ::_thesis: for F being Presv of X,A holds F || A is BinOp of A
let F be Presv of X,A; ::_thesis: F || A is BinOp of A
 ( X = {} implies [:X,X:] = {} ) ;
then  dom F = [:X,X:] by FUNCT_2:def_1;
then A1: dom (F || A) = [:A,A:] by RELAT_1:62, ZFMISC_1:96;
 for x being set st x in [:A,A:] holds
(F || A) . x in A
proof
let x be set ; ::_thesis: ( x in [:A,A:] implies (F || A) . x in A )
assume A2: x in [:A,A:] ; ::_thesis: (F || A) . x in A
then  (F || A) . x = F . x by A1, FUNCT_1:47;
hence  (F || A) . x in A by A2, Def4; ::_thesis: verum
end;
hence  F || A is BinOp of A by A1, FUNCT_2:3; ::_thesis: verum
end;

definition
let X be set ;
let A be Subset of X;
let F be Presv of X,A;
funcF ||| A ->  BinOp of A equals :: REALSET1:def 5
F || A;
coherence
 F || A is BinOp of A by Th6;
end;

:: deftheorem  defines ||| REALSET1:def_5_:_
 for X being set
for A being Subset of X
for F being Presv of X,A holds F ||| A = F || A;

definition
let A be set ;
let x be Element of A;
mode DnT of x,A ->  BinOp of A means :Def6: :: REALSET1:def 6
 for y being set st y in [:(A \ {x}),(A \ {x}):] holds
it . y in A \ {x};
existence
 ex b1 being BinOp of A st
for y being set st y in [:(A \ {x}),(A \ {x}):] holds
b1 . y in A \ {x} by Th5;
end;

:: deftheorem Def6 defines DnT REALSET1:def_6_:_
 for A being set
for x being Element of A
for b3 being BinOp of A holds
( b3 is DnT of x,A iff for y being set st y in [:(A \ {x}),(A \ {x}):] holds
b3 . y in A \ {x} );

theorem Th7: :: REALSET1:7
for A being non trivial set
for x being Element of A
for F being DnT of x,A holds F || (A \ {x}) is BinOp of (A \ {x})
proof
let A be non trivial set ; ::_thesis: for x being Element of A
for F being DnT of x,A holds F || (A \ {x}) is BinOp of (A \ {x})
let x be Element of A; ::_thesis: for F being DnT of x,A holds F || (A \ {x}) is BinOp of (A \ {x})
let F be DnT of x,A; ::_thesis: F || (A \ {x}) is BinOp of (A \ {x})
 dom F = [:A,A:] by FUNCT_2:def_1;
then A1: dom (F || (A \ {x})) = [:(A \ {x}),(A \ {x}):] by RELAT_1:62, ZFMISC_1:96;
 for y being set st y in [:(A \ {x}),(A \ {x}):] holds
(F || (A \ {x})) . y in A \ {x}
proof
let y be set ; ::_thesis: ( y in [:(A \ {x}),(A \ {x}):] implies (F || (A \ {x})) . y in A \ {x} )
assume A2: y in [:(A \ {x}),(A \ {x}):] ; ::_thesis: (F || (A \ {x})) . y in A \ {x}
then  (F || (A \ {x})) . y = F . y by A1, FUNCT_1:47;
hence  (F || (A \ {x})) . y in A \ {x} by A2, Def6; ::_thesis: verum
end;
hence  F || (A \ {x}) is BinOp of (A \ {x}) by A1, FUNCT_2:3; ::_thesis: verum
end;

definition
let A be non trivial set ;
let x be Element of A;
let F be DnT of x,A;
funcF ! (A,x) ->  BinOp of (A \ {x}) equals :: REALSET1:def 7
F || (A \ {x});
coherence
 F || (A \ {x}) is BinOp of (A \ {x}) by Th7;
end;

:: deftheorem  defines ! REALSET1:def_7_:_
 for A being non trivial set
for x being Element of A
for F being DnT of x,A holds F ! (A,x) = F || (A \ {x});

theorem Th8: :: REALSET1:8
for F being non trivial set
for A being Singleton of F holds F \ A is non empty set
proof
let F be non trivial set ; ::_thesis: for A being Singleton of F holds F \ A is non empty set
let A be Singleton of F; ::_thesis: F \ A is non empty set
 ex x being Element of F st A = {x} by CARD_1:65;
hence  F \ A is non empty set by Th3; ::_thesis: verum
end;

registration
let F be non trivial set ;
let A be Singleton of F;
clusterF \ A ->  non empty ;
coherence
 not F \ A is empty by Th8;
end;