:: Boolean Properties of Sets - Definitions
:: by Library Committee
::
:: Received April 6, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users


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] ) )
proofend;

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
proofend;
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 ) )
proofend;
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
proofend;
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 ) )
proofend;
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
proofend;
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 ) )
proofend;
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
proofend;
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 &amp; 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 &amp; X <> Y &amp; Y c= X holds
not Y <> X
proofend;
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 &amp; not Y c= X ) or Y c= X or X c= Y ) ;
redefine pred X = Y means :: XBOOLE_0:def 10
( X c= Y &amp; Y c= X );
compatibility
 ( X = Y iff ( X c= Y &amp; Y c= X ) )
proofend;
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 &amp; 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 &amp; 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 &amp; not x in Y ) or ( x in Y &amp; not x in X ) ) )
proofend;

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
proofend;

registration
cluster {}  ->  empty ;
coherence
 {} is empty ;
end;

registration
let x1 be set ;
cluster{x1} ->  non empty ;
coherence
 not {x1} is empty
proofend;
let x2 be set ;
cluster{x1,x2} ->  non empty ;
coherence
 not {x1,x2} is empty
proofend;
end;

registration
cluster non empty for set ;
existence
 not for b1 being set holds b1 is empty
proofend;
end;

registration
let D be non empty set ;
let X be set ;
clusterD \/ X ->  non empty ;
coherence
 not D \/ X is empty
proofend;
clusterX \/ D ->  non empty ;
coherence
 not X \/ D is empty ;
end;

Lm1:  for X being set st X is empty holds
X = {}
proofend;

theorem Th3: :: XBOOLE_0:3
for X, Y being set holds
( X meets Y iff ex x being set st
( x in X &amp; x in Y ) )
proofend;

theorem :: XBOOLE_0:4
for X, Y being set holds
( X meets Y iff ex x being set st x in X /\ Y )
proofend;

theorem :: XBOOLE_0:5
for X, Y, x being set st X misses Y &amp; x in X \/ Y &amp; not ( x in X &amp; not x in Y ) holds
( x in Y &amp; 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] )
proofend;

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] ) ) &amp; ( for x being set holds
( x in X2 iff P1[x] ) ) holds
X1 = X2
proofend;

begin

:: from RLSUB_2, 2006.12.02, AT
theorem :: XBOOLE_0:6
for X, Y being set st X c< Y holds
ex x being set st
( x in Y &amp; not x in X )
proofend;

:: 2008.08.07, A.T.
theorem :: XBOOLE_0:7
for X being set st X <> {} holds
ex x being set st x in X
proofend;