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

scheme :: XBOOLE_0:sch 1
Separation{ F₁() -> set , P₁[ object ] } :

ex X being set st
for x being object holds
( x in X iff ( x in F₁() & P₁[x] ) )

proof end;

definition

let X be set ;

attr X is empty means :Def1: :: XBOOLE_0:def 1
for x being object 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 object holds not x in X );

registration

cluster empty for set ;

existence
ex b₁ being set st b₁ is empty

proof end;

end;

definition

func {} -> set equals :: XBOOLE_0:def 2
the empty set ;

coherence
the empty set is set ;
let X, Y be set ;

func X \/ Y -> set means :Def3: :: XBOOLE_0:def 3
for x being object holds
( x in it iff ( x in X or x in Y ) );

existence
ex b₁ being set st
for x being object holds
( x in b₁ iff ( x in X or x in Y ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff ( x in X or x in Y ) ) ) & ( for x being object holds
( x in b₂ iff ( x in X or x in Y ) ) ) holds
b₁ = b₂

proof end;

commutativity
for b₁, X, Y being set st ( for x being object holds
( x in b₁ iff ( x in X or x in Y ) ) ) holds
for x being object holds
( x in b₁ iff ( x in Y or x in X ) ) ;
idempotence
for X being set
for x being object holds
( x in X iff ( x in X or x in X ) ) ;

func X /\ Y -> set means :Def4: :: XBOOLE_0:def 4
for x being object holds
( x in it iff ( x in X & x in Y ) );

existence
ex b₁ being set st
for x being object holds
( x in b₁ iff ( x in X & x in Y ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff ( x in X & x in Y ) ) ) & ( for x being object holds
( x in b₂ iff ( x in X & x in Y ) ) ) holds
b₁ = b₂

proof end;

commutativity
for b₁, X, Y being set st ( for x being object holds
( x in b₁ iff ( x in X & x in Y ) ) ) holds
for x being object holds
( x in b₁ iff ( x in Y & x in X ) ) ;
idempotence
for X being set
for x being object holds
( x in X iff ( x in X & x in X ) ) ;

func X \ Y -> set means :Def5: :: XBOOLE_0:def 5
for x being object holds
( x in it iff ( x in X & not x in Y ) );

existence
ex b₁ being set st
for x being object holds
( x in b₁ iff ( x in X & not x in Y ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff ( x in X & not x in Y ) ) ) & ( for x being object holds
( x in b₂ iff ( x in X & not x in Y ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines {} XBOOLE_0:def 2 :
{} = the empty set ;

:: deftheorem Def3 defines \/ XBOOLE_0:def 3 :
for X, Y, b₃ being set holds
( b₃ = X \/ Y iff for x being object holds
( x in b₃ iff ( x in X or x in Y ) ) );

:: deftheorem Def4 defines /\ XBOOLE_0:def 4 :
for X, Y, b₃ being set holds
( b₃ = X /\ Y iff for x being object holds
( x in b₃ iff ( x in X & x in Y ) ) );

:: deftheorem Def5 defines \ XBOOLE_0:def 5 :
for X, Y, b₃ being set holds
( b₃ = X \ Y iff for x being object holds
( x in b₃ iff ( x in X & not x in Y ) ) );

definition

let X, Y be set ;

func X \+\ Y -> set equals :: XBOOLE_0:def 6
(X \ Y) \/ (Y \ X);

correctness
coherence
(X \ Y) \/ (Y \ X) is set ;
;
commutativity
for b₁, X, Y being set st b₁ = (X \ Y) \/ (Y \ X) holds
b₁ = (Y \ X) \/ (X \ Y) ;

pred X misses Y means :: XBOOLE_0:def 7
X /\ Y = {} ;

symmetry
for X, Y being set st X /\ Y = {} holds
Y /\ X = {} ;

pred X 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 by TARSKI:2;

pred X,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 ) ) by TARSKI:2;

end;

:: deftheorem defines \+\ XBOOLE_0:def 6 :
for X, Y being set holds X \+\ Y = (X \ Y) \/ (Y \ X);

:: deftheorem 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, Y being set
for x being object holds
( x in X \+\ Y iff ( ( x in X & not x in Y ) or ( x in Y & not x in X ) ) )

proof end;

theorem :: XBOOLE_0:2

for X, Y, Z being set st ( for x being object holds
( not x in X iff ( x in Y iff x in Z ) ) ) holds
X = Y \+\ Z

proof end;

registration

cluster {} -> empty ;

coherence
{} is empty ;

end;

registration

let x be object ;

cluster {x} -> non empty ;

coherence
not {x} is empty

proof end;

let y be object ;

cluster {x,y} -> non empty ;

coherence
not {x,y} is empty

proof end;

end;

registration

cluster non empty for set ;

existence
not for b₁ being set holds b₁ is empty

proof end;

end;

registration

let D be non empty set ;
let X be set ;

cluster D \/ X -> non empty ;

coherence
not D \/ X is empty

proof end;

cluster X \/ D -> non empty ;

coherence
not X \/ D is empty ;

end;

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

proof end;

theorem Th3: :: XBOOLE_0:3

for X, Y being set holds
( X meets Y iff ex x being object st
( x in X & x in Y ) )

proof end;

theorem :: XBOOLE_0:4

for X, Y being set holds
( X meets Y iff ex x being object st x in X /\ Y )

proof end;

theorem :: XBOOLE_0:5

for X, Y being set
for x being object 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{ F₁() -> set , F₂() -> set , P₁[ object ] } :

F₁() = F₂()

provided

A1: for x being object holds
( x in F₁() iff P₁[x] ) and
A2: for x being object holds
( x in F₂() iff P₁[x] )

proof end;

scheme :: XBOOLE_0:sch 3
SetEq{ P₁[ object ] } :

for X1, X2 being set st ( for x being object holds
( x in X1 iff P₁[x] ) ) & ( for x being object holds
( x in X2 iff P₁[x] ) ) holds
X1 = X2

proof end;

:: from RLSUB_2, 2006.12.02, AT

theorem Th6: :: XBOOLE_0:6

for X, Y being set st X c< Y holds
ex x being object st
( x in Y & not x in X ) by Def8, TARSKI:def 3;

:: 2008.08.07, A.T.

theorem :: XBOOLE_0:7

for X being set st X <> {} holds
ex x being object st x in X by Def1, Lm1;

:: 2012.10.08, A.T.

theorem :: XBOOLE_0:8

for X, Y being set st X c< Y holds
ex x being object st
( x in Y & X c= Y \ {x} )

proof end;

notation

let x, y be set ;
antonym x c/= y for x c= y;

end;

notation

let x be object ;
let y be set ;
antonym x nin y for x in y;

end;