:: Boolean Domains
:: by Andrzej Trybulec and Agata Darmochwa\l
::
:: Received April 14, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users

definition

let IT be set ;

attr IT is cup-closed means :Def1: :: FINSUB_1:def 1
for X, Y being set st X in IT & Y in IT holds
X \/ Y in IT;

attr IT is cap-closed means :: FINSUB_1:def 2
for X, Y being set st X in IT & Y in IT holds
X /\ Y in IT;

attr IT is diff-closed means :Def3: :: FINSUB_1:def 3
for X, Y being set st X in IT & Y in IT holds
X \ Y in IT;

end;

:: deftheorem Def1 defines cup-closed FINSUB_1:def 1 :
for IT being set holds
( IT is cup-closed iff for X, Y being set st X in IT & Y in IT holds
X \/ Y in IT );

:: deftheorem defines cap-closed FINSUB_1:def 2 :
for IT being set holds
( IT is cap-closed iff for X, Y being set st X in IT & Y in IT holds
X /\ Y in IT );

:: deftheorem Def3 defines diff-closed FINSUB_1:def 3 :
for IT being set holds
( IT is diff-closed iff for X, Y being set st X in IT & Y in IT holds
X \ Y in IT );

definition

let IT be set ;

attr IT is preBoolean means :: FINSUB_1:def 4
( IT is cup-closed & IT is diff-closed );

end;

:: deftheorem defines preBoolean FINSUB_1:def 4 :
for IT being set holds
( IT is preBoolean iff ( IT is cup-closed & IT is diff-closed ) );

registration

cluster preBoolean -> cup-closed diff-closed for set ;

coherence
for b₁ being set st b₁ is preBoolean holds
( b₁ is cup-closed & b₁ is diff-closed ) ;

cluster cup-closed diff-closed -> preBoolean for set ;

coherence
for b₁ being set st b₁ is cup-closed & b₁ is diff-closed holds
b₁ is preBoolean ;

end;

registration

cluster non empty cup-closed cap-closed diff-closed for set ;

existence
ex b₁ being set st
( not b₁ is empty & b₁ is cup-closed & b₁ is cap-closed & b₁ is diff-closed )

proof end;

end;

theorem Th1: :: FINSUB_1:1

for A being set holds
( A is preBoolean iff for X, Y being set st X in A & Y in A holds
( X \/ Y in A & X \ Y in A ) )

proof end;

definition

let A be non empty preBoolean set ;
let X, Y be Element of A;
:: original: \/
redefine func X \/ Y -> Element of A;
correctness
coherence
X \/ Y is Element of A;
by Th1;
:: original: \
redefine func X \ Y -> Element of A;
correctness
coherence
X \ Y is Element of A;
by Th1;

end;

theorem Th2: :: FINSUB_1:2

for X, Y being set
for A being non empty preBoolean set st X is Element of A & Y is Element of A holds
X /\ Y is Element of A

proof end;

theorem Th3: :: FINSUB_1:3

for X, Y being set
for A being non empty preBoolean set st X is Element of A & Y is Element of A holds
X \+\ Y is Element of A

proof end;

theorem :: FINSUB_1:4

for A being non empty set st ( for X, Y being Element of A holds
( X \+\ Y in A & X \ Y in A ) ) holds
A is preBoolean

proof end;

theorem :: FINSUB_1:5

for A being non empty set st ( for X, Y being Element of A holds
( X \+\ Y in A & X /\ Y in A ) ) holds
A is preBoolean

proof end;

theorem :: FINSUB_1:6

for A being non empty set st ( for X, Y being Element of A holds
( X \+\ Y in A & X \/ Y in A ) ) holds
A is preBoolean

proof end;

definition

let A be non empty preBoolean set ;
let X, Y be Element of A;
:: original: /\
redefine func X /\ Y -> Element of A;
coherence
X /\ Y is Element of A by Th2;
:: original: \+\
redefine func X \+\ Y -> Element of A;
coherence
X \+\ Y is Element of A by Th3;

end;

theorem Th7: :: FINSUB_1:7

for A being non empty preBoolean set holds {} in A

proof end;

theorem Th8: :: FINSUB_1:8

for A being set holds bool A is preBoolean

proof end;

registration

let A be set ;

cluster bool A -> preBoolean ;

coherence
bool A is preBoolean by Th8;

end;

theorem :: FINSUB_1:9

for A, B being non empty preBoolean set holds
( not A /\ B is empty & A /\ B is preBoolean )

proof end;

:: The set of all finite subsets of a set

definition

let A be set ;

func Fin A -> preBoolean set means :Def5: :: FINSUB_1:def 5
for X being set holds
( X in it iff ( X c= A & X is finite ) );

existence
ex b₁ being preBoolean set st
for X being set holds
( X in b₁ iff ( X c= A & X is finite ) )

proof end;

uniqueness
for b₁, b₂ being preBoolean set st ( for X being set holds
( X in b₁ iff ( X c= A & X is finite ) ) ) & ( for X being set holds
( X in b₂ iff ( X c= A & X is finite ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines Fin FINSUB_1:def 5 :
for A being set
for b₂ being preBoolean set holds
( b₂ = Fin A iff for X being set holds
( X in b₂ iff ( X c= A & X is finite ) ) );

registration

let A be set ;

cluster Fin A -> non empty preBoolean ;

coherence
not Fin A is empty

proof end;

end;

registration

let A be set ;

cluster -> finite for Element of Fin A;

coherence
for b₁ being Element of Fin A holds b₁ is finite by Def5;

end;

theorem Th10: :: FINSUB_1:10

for A, B being set st A c= B holds
Fin A c= Fin B

proof end;

theorem :: FINSUB_1:11

for A, B being set holds Fin (A /\ B) = (Fin A) /\ (Fin B)

proof end;

theorem :: FINSUB_1:12

for A, B being set holds (Fin A) \/ (Fin B) c= Fin (A \/ B)

proof end;

theorem Th13: :: FINSUB_1:13

for A being set holds Fin A c= bool A

proof end;

theorem Th14: :: FINSUB_1:14

for A being set st A is finite holds
Fin A = bool A

proof end;

theorem :: FINSUB_1:15

Fin {} = {{}} by Th14, ZFMISC_1:1;

theorem :: FINSUB_1:16

for A being set
for X being Element of Fin A holds X is Subset of A by Def5;

theorem :: FINSUB_1:17

for A being set
for X being Subset of A st A is finite holds
X is Element of Fin A by Def5;