:: XBOOLE_0 semantic presentation
begin
scheme :: XBOOLE_0:sch 1
Separation{ F1() -> set , P1[ set ] } :
ex X being set st
for x being set holds
( x in X iff ( x in F1() & P1[x] ) )
proof
defpred S1[ set , set ] means ( $1 = $2 & P1[$2] );
A1: for x, y, z being set st S1[x,y] & S1[x,z] holds
y = z ;
consider X being set such that
A2: for x being set holds
( x in X iff ex y being set st
( y in F1() & S1[y,x] ) ) from TARSKI:sch_1(A1);
take X ; ::_thesis: for x being set holds
( x in X iff ( x in F1() & P1[x] ) )
let x be set ; ::_thesis: ( x in X iff ( x in F1() & P1[x] ) )
( x in X iff ex y being set st
( y in F1() & y = x & P1[x] ) ) by A2;
hence ( x in X iff ( x in F1() & P1[x] ) ) ; ::_thesis: verum
end;
definition
let X be set ;
attrX is empty means :Def1: :: XBOOLE_0:def 1
for x being set holds not x in X;
end;
:: deftheorem Def1 defines empty XBOOLE_0:def_1_:_
for X being set holds
( X is empty iff for x being set holds not x in X );
registration
cluster empty for set ;
existence
ex b1 being set st b1 is empty
proof
defpred S1[ set ] means contradiction;
consider Y being set such that
A1: for x being set holds
( x in Y iff ( x in the set & S1[x] ) ) from XBOOLE_0:sch_1();
take Y ; ::_thesis: Y is empty
thus for x being set holds not x in Y by A1; :: according to XBOOLE_0:def_1 ::_thesis: verum
end;
end;
definition
func {} -> set equals :: XBOOLE_0:def 2
the empty set ;
coherence
the empty set is set ;
let X, Y be set ;
funcX \/ Y -> set means :Def3: :: XBOOLE_0:def 3
for x being set holds
( x in it iff ( x in X or x in Y ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x in X or x in Y ) )
proof
take union {X,Y} ; ::_thesis: for x being set holds
( x in union {X,Y} iff ( x in X or x in Y ) )
let x be set ; ::_thesis: ( x in union {X,Y} iff ( x in X or x in Y ) )
thus ( not x in union {X,Y} or x in X or x in Y ) ::_thesis: ( ( x in X or x in Y ) implies x in union {X,Y} )
proof
assume x in union {X,Y} ; ::_thesis: ( x in X or x in Y )
then ex Z being set st
( x in Z & Z in {X,Y} ) by TARSKI:def_4;
hence ( x in X or x in Y ) by TARSKI:def_2; ::_thesis: verum
end;
( X in {X,Y} & Y in {X,Y} ) by TARSKI:def_2;
hence ( ( x in X or x in Y ) implies x in union {X,Y} ) by TARSKI:def_4; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in X or x in Y ) ) ) & ( for x being set holds
( x in b2 iff ( x in X or x in Y ) ) ) holds
b1 = b2
proof
let A1, A2 be set ; ::_thesis: ( ( for x being set holds
( x in A1 iff ( x in X or x in Y ) ) ) & ( for x being set holds
( x in A2 iff ( x in X or x in Y ) ) ) implies A1 = A2 )
assume that
A3: for x being set holds
( x in A1 iff ( x in X or x in Y ) ) and
A4: for x being set holds
( x in A2 iff ( x in X or x in Y ) ) ; ::_thesis: A1 = A2
now__::_thesis:_for_x_being_set_holds_
(_x_in_A1_iff_x_in_A2_)
let x be set ; ::_thesis: ( x in A1 iff x in A2 )
( x in A1 iff ( x in X or x in Y ) ) by A3;
hence ( x in A1 iff x in A2 ) by A4; ::_thesis: verum
end;
hence A1 = A2 by TARSKI:1; ::_thesis: verum
end;
commutativity
for b1, X, Y being set st ( for x being set holds
( x in b1 iff ( x in X or x in Y ) ) ) holds
for x being set holds
( x in b1 iff ( x in Y or x in X ) ) ;
idempotence
for X, x being set holds
( x in X iff ( x in X or x in X ) ) ;
funcX /\ Y -> set means :Def4: :: XBOOLE_0:def 4
for x being set holds
( x in it iff ( x in X & x in Y ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x in X & x in Y ) )
proof
defpred S1[ set ] means $1 in Y;
thus ex Z being set st
for x being set holds
( x in Z iff ( x in X & S1[x] ) ) from XBOOLE_0:sch_1(); ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in X & x in Y ) ) ) & ( for x being set holds
( x in b2 iff ( x in X & x in Y ) ) ) holds
b1 = b2
proof
let A1, A2 be set ; ::_thesis: ( ( for x being set holds
( x in A1 iff ( x in X & x in Y ) ) ) & ( for x being set holds
( x in A2 iff ( x in X & x in Y ) ) ) implies A1 = A2 )
assume that
A5: for x being set holds
( x in A1 iff ( x in X & x in Y ) ) and
A6: for x being set holds
( x in A2 iff ( x in X & x in Y ) ) ; ::_thesis: A1 = A2
now__::_thesis:_for_x_being_set_holds_
(_x_in_A1_iff_x_in_A2_)
let x be set ; ::_thesis: ( x in A1 iff x in A2 )
( x in A1 iff ( x in X & x in Y ) ) by A5;
hence ( x in A1 iff x in A2 ) by A6; ::_thesis: verum
end;
hence A1 = A2 by TARSKI:1; ::_thesis: verum
end;
commutativity
for b1, X, Y being set st ( for x being set holds
( x in b1 iff ( x in X & x in Y ) ) ) holds
for x being set holds
( x in b1 iff ( x in Y & x in X ) ) ;
idempotence
for X, x being set holds
( x in X iff ( x in X & x in X ) ) ;
funcX \ Y -> set means :Def5: :: XBOOLE_0:def 5
for x being set holds
( x in it iff ( x in X & not x in Y ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x in X & not x in Y ) )
proof
defpred S1[ set ] means not $1 in Y;
thus ex Z being set st
for x being set holds
( x in Z iff ( x in X & S1[x] ) ) from XBOOLE_0:sch_1(); ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in X & not x in Y ) ) ) & ( for x being set holds
( x in b2 iff ( x in X & not x in Y ) ) ) holds
b1 = b2
proof
let A1, A2 be set ; ::_thesis: ( ( for x being set holds
( x in A1 iff ( x in X & not x in Y ) ) ) & ( for x being set holds
( x in A2 iff ( x in X & not x in Y ) ) ) implies A1 = A2 )
assume that
A7: for x being set holds
( x in A1 iff ( x in X & not x in Y ) ) and
A8: for x being set holds
( x in A2 iff ( x in X & not x in Y ) ) ; ::_thesis: A1 = A2
now__::_thesis:_for_x_being_set_holds_
(_x_in_A1_iff_x_in_A2_)
let x be set ; ::_thesis: ( x in A1 iff x in A2 )
( x in A1 iff ( x in X & not x in Y ) ) by A7;
hence ( x in A1 iff x in A2 ) by A8; ::_thesis: verum
end;
hence A1 = A2 by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem defines {} XBOOLE_0:def_2_:_
{} = the empty set ;
:: deftheorem Def3 defines \/ XBOOLE_0:def_3_:_
for X, Y, b3 being set holds
( b3 = X \/ Y iff for x being set holds
( x in b3 iff ( x in X or x in Y ) ) );
:: deftheorem Def4 defines /\ XBOOLE_0:def_4_:_
for X, Y, b3 being set holds
( b3 = X /\ Y iff for x being set holds
( x in b3 iff ( x in X & x in Y ) ) );
:: deftheorem Def5 defines \ XBOOLE_0:def_5_:_
for X, Y, b3 being set holds
( b3 = X \ Y iff for x being set holds
( x in b3 iff ( x in X & not x in Y ) ) );
definition
let X, Y be set ;
funcX \+\ Y -> set equals :: XBOOLE_0:def 6
(X \ Y) \/ (Y \ X);
correctness
coherence
(X \ Y) \/ (Y \ X) is set ;
;
commutativity
for b1, X, Y being set st b1 = (X \ Y) \/ (Y \ X) holds
b1 = (Y \ X) \/ (X \ Y) ;
predX misses Y means :Def7: :: XBOOLE_0:def 7
X /\ Y = {} ;
symmetry
for X, Y being set st X /\ Y = {} holds
Y /\ X = {} ;
predX c< Y means :Def8: :: XBOOLE_0:def 8
( X c= Y & X <> Y );
irreflexivity
for X being set holds
( not X c= X or not X <> X ) ;
asymmetry
for X, Y being set st X c= Y & X <> Y & Y c= X holds
not Y <> X
proof
let X, Y be set ; ::_thesis: ( X c= Y & X <> Y & Y c= X implies not Y <> X )
assume A1: X c= Y ; ::_thesis: ( not X <> Y or not Y c= X or not Y <> X )
assume X <> Y ; ::_thesis: ( not Y c= X or not Y <> X )
assume Y c= X ; ::_thesis: not Y <> X
then for x being set holds
( x in X iff x in Y ) by A1, TARSKI:def_3;
hence not Y <> X by TARSKI:1; ::_thesis: verum
end;
predX,Y are_c=-comparable means :: XBOOLE_0:def 9
( X c= Y or Y c= X );
reflexivity
for X being set holds
( X c= X or X c= X ) ;
symmetry
for X, Y being set holds
( ( not X c= Y & not Y c= X ) or Y c= X or X c= Y ) ;
redefine pred X = Y means :: XBOOLE_0:def 10
( X c= Y & Y c= X );
compatibility
( X = Y iff ( X c= Y & Y c= X ) )
proof
thus ( X = Y implies ( X c= Y & Y c= X ) ) ; ::_thesis: ( X c= Y & Y c= X implies X = Y )
assume ( X c= Y & Y c= X ) ; ::_thesis: X = Y
then for x being set holds
( x in X iff x in Y ) by TARSKI:def_3;
hence X = Y by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem defines \+\ XBOOLE_0:def_6_:_
for X, Y being set holds X \+\ Y = (X \ Y) \/ (Y \ X);
:: deftheorem Def7 defines misses XBOOLE_0:def_7_:_
for X, Y being set holds
( X misses Y iff X /\ Y = {} );
:: deftheorem Def8 defines c< XBOOLE_0:def_8_:_
for X, Y being set holds
( X c< Y iff ( X c= Y & X <> Y ) );
:: deftheorem defines are_c=-comparable XBOOLE_0:def_9_:_
for X, Y being set holds
( X,Y are_c=-comparable iff ( X c= Y or Y c= X ) );
:: deftheorem defines = XBOOLE_0:def_10_:_
for X, Y being set holds
( X = Y iff ( X c= Y & Y c= X ) );
notation
let X, Y be set ;
antonym X meets Y for X misses Y;
end;
theorem :: XBOOLE_0:1
for x, X, Y being set holds
( x in X \+\ Y iff ( ( x in X & not x in Y ) or ( x in Y & not x in X ) ) )
proof
let x, X, Y be set ; ::_thesis: ( x in X \+\ Y iff ( ( x in X & not x in Y ) or ( x in Y & not x in X ) ) )
( x in X \+\ Y iff ( x in X \ Y or x in Y \ X ) ) by Def3;
hence ( x in X \+\ Y iff ( ( x in X & not x in Y ) or ( x in Y & not x in X ) ) ) by Def5; ::_thesis: verum
end;
theorem :: XBOOLE_0:2
for X, Y, Z being set st ( for x being set holds
( not x in X iff ( x in Y iff x in Z ) ) ) holds
X = Y \+\ Z
proof
let X, Y, Z be set ; ::_thesis: ( ( for x being set holds
( not x in X iff ( x in Y iff x in Z ) ) ) implies X = Y \+\ Z )
assume A1: for x being set holds
( not x in X iff ( x in Y iff x in Z ) ) ; ::_thesis: X = Y \+\ Z
now__::_thesis:_for_x_being_set_holds_
(_x_in_X_iff_x_in_Y_\+\_Z_)
let x be set ; ::_thesis: ( x in X iff x in Y \+\ Z )
( x in X iff ( ( x in Y & not x in Z ) or ( x in Z & not x in Y ) ) ) by A1;
then ( x in X iff ( x in Y \ Z or x in Z \ Y ) ) by Def5;
hence ( x in X iff x in Y \+\ Z ) by Def3; ::_thesis: verum
end;
hence X = Y \+\ Z by TARSKI:1; ::_thesis: verum
end;
registration
cluster {} -> empty ;
coherence
{} is empty ;
end;
registration
let x1 be set ;
cluster{x1} -> non empty ;
coherence
not {x1} is empty
proof
x1 in {x1} by TARSKI:def_1;
hence ex x being set st x in {x1} ; :: according to XBOOLE_0:def_1 ::_thesis: verum
end;
let x2 be set ;
cluster{x1,x2} -> non empty ;
coherence
not {x1,x2} is empty
proof
x1 in {x1,x2} by TARSKI:def_2;
hence ex x being set st x in {x1,x2} ; :: according to XBOOLE_0:def_1 ::_thesis: verum
end;
end;
registration
cluster non empty for set ;
existence
not for b1 being set holds b1 is empty
proof
take { the set } ; ::_thesis: not { the set } is empty
thus not { the set } is empty ; ::_thesis: verum
end;
end;
registration
let D be non empty set ;
let X be set ;
clusterD \/ X -> non empty ;
coherence
not D \/ X is empty
proof
consider x being set such that
A1: x in D by Def1;
x in D \/ X by A1, Def3;
hence ex x being set st x in D \/ X ; :: according to XBOOLE_0:def_1 ::_thesis: verum
end;
clusterX \/ D -> non empty ;
coherence
not X \/ D is empty ;
end;
Lm1: for X being set st X is empty holds
X = {}
proof
let X be set ; ::_thesis: ( X is empty implies X = {} )
assume for x being set holds not x in X ; :: according to XBOOLE_0:def_1 ::_thesis: X = {}
then for x being set holds
( x in {} iff x in X ) by Def1;
hence X = {} by TARSKI:1; ::_thesis: verum
end;
theorem Th3: :: XBOOLE_0:3
for X, Y being set holds
( X meets Y iff ex x being set st
( x in X & x in Y ) )
proof
let X, Y be set ; ::_thesis: ( X meets Y iff ex x being set st
( x in X & x in Y ) )
hereby ::_thesis: ( ex x being set st
( x in X & x in Y ) implies X meets Y )
assume X meets Y ; ::_thesis: ex x being set st
( x in X & x in Y )
then X /\ Y <> {} by Def7;
then not X /\ Y is empty by Lm1;
then consider x being set such that
A1: x in X /\ Y by Def1;
take x = x; ::_thesis: ( x in X & x in Y )
thus ( x in X & x in Y ) by A1, Def4; ::_thesis: verum
end;
given x being set such that A2: ( x in X & x in Y ) ; ::_thesis: X meets Y
x in X /\ Y by A2, Def4;
then X /\ Y <> {} by Def1;
hence X meets Y by Def7; ::_thesis: verum
end;
theorem :: XBOOLE_0:4
for X, Y being set holds
( X meets Y iff ex x being set st x in X /\ Y )
proof
let X, Y be set ; ::_thesis: ( X meets Y iff ex x being set st x in X /\ Y )
hereby ::_thesis: ( ex x being set st x in X /\ Y implies X meets Y )
assume X meets Y ; ::_thesis: ex x being set st x in X /\ Y
then X /\ Y <> {} by Def7;
then not X /\ Y is empty by Lm1;
then consider x being set such that
A1: x in X /\ Y by Def1;
take x = x; ::_thesis: x in X /\ Y
thus x in X /\ Y by A1; ::_thesis: verum
end;
assume ex x being set st x in X /\ Y ; ::_thesis: X meets Y
then X /\ Y <> {} by Def1;
hence X meets Y by Def7; ::_thesis: verum
end;
theorem :: XBOOLE_0:5
for X, Y, x being set st X misses Y & x in X \/ Y & not ( x in X & not x in Y ) holds
( x in Y & not x in X ) by Def3, Th3;
scheme :: XBOOLE_0:sch 2
Extensionality{ F1() -> set , F2() -> set , P1[ set ] } :
F1() = F2()
provided
A1: for x being set holds
( x in F1() iff P1[x] ) and
A2: for x being set holds
( x in F2() iff P1[x] )
proof
A3: for x being set st x in F2() holds
x in F1()
proof
let x be set ; ::_thesis: ( x in F2() implies x in F1() )
assume x in F2() ; ::_thesis: x in F1()
then P1[x] by A2;
hence x in F1() by A1; ::_thesis: verum
end;
for x being set st x in F1() holds
x in F2()
proof
let x be set ; ::_thesis: ( x in F1() implies x in F2() )
assume x in F1() ; ::_thesis: x in F2()
then P1[x] by A1;
hence x in F2() by A2; ::_thesis: verum
end;
hence F1() = F2() by A3, TARSKI:1; ::_thesis: verum
end;
scheme :: XBOOLE_0:sch 3
SetEq{ P1[ set ] } :
for X1, X2 being set st ( for x being set holds
( x in X1 iff P1[x] ) ) & ( for x being set holds
( x in X2 iff P1[x] ) ) holds
X1 = X2
proof
let X1, X2 be set ; ::_thesis: ( ( for x being set holds
( x in X1 iff P1[x] ) ) & ( for x being set holds
( x in X2 iff P1[x] ) ) implies X1 = X2 )
assume that
A1: for x being set holds
( x in X1 iff P1[x] ) and
A2: for x being set holds
( x in X2 iff P1[x] ) ; ::_thesis: X1 = X2
thus X1 = X2 from XBOOLE_0:sch_2(A1, A2); ::_thesis: verum
end;
begin
theorem :: XBOOLE_0:6
for X, Y being set st X c< Y holds
ex x being set st
( x in Y & not x in X )
proof
let X, Y be set ; ::_thesis: ( X c< Y implies ex x being set st
( x in Y & not x in X ) )
assume X c< Y ; ::_thesis: ex x being set st
( x in Y & not x in X )
then ( not for x being set holds
( x in X iff x in Y ) & X c= Y ) by Def8, TARSKI:1;
hence ex x being set st
( x in Y & not x in X ) by TARSKI:def_3; ::_thesis: verum
end;
theorem :: XBOOLE_0:7
for X being set st X <> {} holds
ex x being set st x in X
proof
let X be set ; ::_thesis: ( X <> {} implies ex x being set st x in X )
assume A1: X <> {} ; ::_thesis: ex x being set st x in X
assume for x being set holds not x in X ; ::_thesis: contradiction
then X is empty by Def1;
hence contradiction by A1, Lm1; ::_thesis: verum
end;