:: by Library Committee

::

:: Received April 6, 2002

:: Copyright (c) 2002 Association of Mizar Users

begin

definition
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 );

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 set holds

( x in it iff ( x in X or x in Y ) );

existence

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x in X or x in Y ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x in X or x in Y ) ) ) & ( for x being set holds

( x in b_{2} iff ( x in X or x in Y ) ) ) holds

b_{1} = b_{2}

for b_{1}, X, Y being set st ( for x being set holds

( x in b_{1} iff ( x in X or x in Y ) ) ) holds

for x being set holds

( x in b_{1} 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 ) ) ;

func X /\ 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 b_{1} being set st

for x being set holds

( x in b_{1} iff ( x in X & x in Y ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x in X & x in Y ) ) ) & ( for x being set holds

( x in b_{2} iff ( x in X & x in Y ) ) ) holds

b_{1} = b_{2}

for b_{1}, X, Y being set st ( for x being set holds

( x in b_{1} iff ( x in X & x in Y ) ) ) holds

for x being set holds

( x in b_{1} iff ( x in Y & x in X ) )
;

idempotence

for X, x being set holds

( x in X iff ( x in X & x in X ) ) ;

func X \ 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 b_{1} being set st

for x being set holds

( x in b_{1} iff ( x in X & not x in Y ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x in X & not x in Y ) ) ) & ( for x being set holds

( x in b_{2} iff ( x in X & not x in Y ) ) ) holds

b_{1} = b_{2}

end;
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 set holds

( x in it iff ( x in X or x in Y ) );

existence

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

commutativity for b

( x in b

for x being set holds

( x in b

idempotence

for X, x being set 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 set holds

( x in it iff ( x in X & x in Y ) );

existence

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

commutativity for b

( x in b

for x being set holds

( x in b

idempotence

for X, x being set holds

( x in X iff ( x in X & x in X ) ) ;

func X \ 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 b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem defines {} XBOOLE_0:def 2 :

{} = the empty set ;

:: deftheorem Def3 defines \/ XBOOLE_0:def 3 :

for X, Y, b

( b

( x in b

:: deftheorem Def4 defines /\ XBOOLE_0:def 4 :

for X, Y, b

( b

( x in b

:: deftheorem Def5 defines \ XBOOLE_0:def 5 :

for X, Y, b

( b

( x in b

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_{1}, X, Y being set st b_{1} = (X \ Y) \/ (Y \ X) holds

b_{1} = (Y \ X) \/ (X \ Y)
;

pred X misses Y means :Def7: :: 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

( 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 ) )

end;
func X \+\ Y -> set equals :: XBOOLE_0:def 6

(X \ Y) \/ (Y \ X);

correctness

coherence

(X \ Y) \/ (Y \ X) is set ;

;

commutativity

for b

b

pred X misses Y means :Def7: :: 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

proof end;

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 ) )

proof 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 ) );

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 ) ) )

( 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 set holds

( not x in X iff ( x in Y iff x in Z ) ) ) holds

X = Y \+\ Z

( not x in X iff ( x in Y iff x in Z ) ) ) holds

X = Y \+\ Z

proof end;

registration

let x1 be set ;

cluster {x1} -> non empty ;

coherence

not {x1} is empty

cluster {x1,x2} -> non empty ;

coherence

not {x1,x2} is empty

end;
cluster {x1} -> non empty ;

coherence

not {x1} is empty

proof end;

let x2 be set ;cluster {x1,x2} -> non empty ;

coherence

not {x1,x2} is empty

proof end;

registration
end;

registration

let D be non empty set ;

let X be set ;

cluster D \/ X -> non empty ;

coherence

not D \/ X is empty

coherence

not X \/ D is empty ;

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

Lm1: for X being set st X is empty holds

X = {}

proof end;

theorem Th3: :: XBOOLE_0:3

proof end;

theorem :: XBOOLE_0:4

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

( x in Y & not x in X ) by Def3, Th3;

scheme :: XBOOLE_0:sch 2

Extensionality{ F_{1}() -> set , F_{2}() -> set , P_{1}[ set ] } :

provided

Extensionality{ F

provided

A1:
for x being set holds

( x in F_{1}() iff P_{1}[x] )
and

A2: for x being set holds

( x in F_{2}() iff P_{1}[x] )

( x in F

A2: for x being set holds

( x in F

proof end;

scheme :: XBOOLE_0:sch 3

SetEq{ P_{1}[ set ] } :

SetEq{ P

for X1, X2 being set st ( for x being set holds

( x in X1 iff P_{1}[x] ) ) & ( for x being set holds

( x in X2 iff P_{1}[x] ) ) holds

X1 = X2

( x in X1 iff P

( x in X2 iff P

X1 = X2

proof end;

begin

theorem :: XBOOLE_0:6

proof end;

theorem :: XBOOLE_0:7

proof end;