:: FINSUB_1 semantic presentation

definition

let c₁ be set ;
attr a₁ is cup-closed means :Def1: :: FINSUB_1:def 1
for b₁, b₂ being set st b₁ in a₁ & b₂ in a₁ holds
b₁ \/ b₂ in a₁;
attr a₁ is cap-closed means :: FINSUB_1:def 2
for b₁, b₂ being set st b₁ in a₁ & b₂ in a₁ holds
b₁ /\ b₂ in a₁;
attr a₁ is diff-closed means :Def3: :: FINSUB_1:def 3
for b₁, b₂ being set st b₁ in a₁ & b₂ in a₁ holds
b₁ \ b₂ in a₁;

end;

:: deftheorem Def1 defines cup-closed FINSUB_1:def 1 :

:: deftheorem Def2 defines cap-closed FINSUB_1:def 2 :

:: deftheorem Def3 defines diff-closed FINSUB_1:def 3 :

definition

let c₁ be set ;
attr a₁ is preBoolean means :Def4: :: FINSUB_1:def 4
( a₁ is cup-closed & a₁ is diff-closed );

end;

:: deftheorem Def4 defines preBoolean FINSUB_1:def 4 :

registration

cluster preBoolean -> cup-closed diff-closed set ;
coherence by Def4;
cluster cup-closed diff-closed -> preBoolean set ;
coherence by Def4;

end;

registration

cluster non empty cup-closed cap-closed diff-closed preBoolean set ;
existence

proof end;

end;

theorem Th1: :: FINSUB_1:1

canceled;

theorem Th2: :: FINSUB_1:2

canceled;

theorem Th3: :: FINSUB_1:3

canceled;

theorem Th4: :: FINSUB_1:4

canceled;

theorem Th5: :: FINSUB_1:5

canceled;

theorem Th6: :: FINSUB_1:6

canceled;

theorem Th7: :: FINSUB_1:7

canceled;

theorem Th8: :: FINSUB_1:8

canceled;

theorem Th9: :: FINSUB_1:9

canceled;

theorem Th10: :: FINSUB_1:10

for b₁ being set holds
( b₁ is preBoolean iff for b₂, b₃ being set st b₂ in b₁ & b₃ in b₁ holds
( b₂ \/ b₃ in b₁ & b₂ \ b₃ in b₁ ) )

proof end;

definition

let c₁ be non empty preBoolean set ;
let c₂, c₃ be Element of c₁;
redefine func \/ as c₂ \/ c₃ -> Element of a₁;
correctness by Th10;
redefine func \ as c₂ \ c₃ -> Element of a₁;
correctness by Th10;

end;

theorem Th11: :: FINSUB_1:11

canceled;

theorem Th12: :: FINSUB_1:12

canceled;

theorem Th13: :: FINSUB_1:13

for b₁, b₂ being set
for b₃ being non empty preBoolean set st b₁ is Element of b₃ & b₂ is Element of b₃ holds
b₁ /\ b₂ is Element of b₃

proof end;

theorem Th14: :: FINSUB_1:14

for b₁, b₂ being set
for b₃ being non empty preBoolean set st b₁ is Element of b₃ & b₂ is Element of b₃ holds
b₁ \+\ b₂ is Element of b₃

proof end;

theorem Th15: :: FINSUB_1:15

for b₁ being non empty set st ( for b₂, b₃ being Element of b₁ holds
( b₂ \+\ b₃ in b₁ & b₂ \ b₃ in b₁ ) ) holds
b₁ is preBoolean

proof end;

theorem Th16: :: FINSUB_1:16

for b₁ being non empty set st ( for b₂, b₃ being Element of b₁ holds
( b₂ \+\ b₃ in b₁ & b₂ /\ b₃ in b₁ ) ) holds
b₁ is preBoolean

proof end;

theorem Th17: :: FINSUB_1:17

for b₁ being non empty set st ( for b₂, b₃ being Element of b₁ holds
( b₂ \+\ b₃ in b₁ & b₂ \/ b₃ in b₁ ) ) holds
b₁ is preBoolean

proof end;

definition

let c₁ be non empty preBoolean set ;
let c₂, c₃ be Element of c₁;
redefine func /\ as c₂ /\ c₃ -> Element of a₁;
coherence by Th13;
redefine func \+\ as c₂ \+\ c₃ -> Element of a₁;
coherence by Th14;

end;

theorem Th18: :: FINSUB_1:18

for b₁ being non empty preBoolean set holds {} in b₁

proof end;

theorem Th19: :: FINSUB_1:19

canceled;

theorem Th20: :: FINSUB_1:20

for b₁ being set holds bool b₁ is preBoolean

proof end;

registration

let c₁ be set ;
cluster bool a₁ -> cup-closed diff-closed preBoolean ;
coherence by Th20;

end;

theorem Th21: :: FINSUB_1:21

for b₁, b₂ being non empty preBoolean set holds
( not b₁ /\ b₂ is empty & b₁ /\ b₂ is preBoolean )

proof end;

definition

let c₁ be set ;
func Fin c₁ -> preBoolean set means :Def5: :: FINSUB_1:def 5
for b₁ being set holds
( b₁ in a₂ iff ( b₁ c= a₁ & b₁ is finite ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Fin FINSUB_1:def 5 :

registration

let c₁ be set ;
cluster Fin a₁ -> non empty cup-closed diff-closed preBoolean ;
coherence

proof end;

end;

registration

let c₁ be set ;
cluster -> finite Element of Fin a₁;
coherence by Def5;

end;

theorem Th22: :: FINSUB_1:22

canceled;

theorem Th23: :: FINSUB_1:23

for b₁, b₂ being set st b₁ c= b₂ holds
Fin b₁ c= Fin b₂

proof end;

theorem Th24: :: FINSUB_1:24

for b₁, b₂ being set holds Fin (b₁ /\ b₂) = (Fin b₁) /\ (Fin b₂)

proof end;

theorem Th25: :: FINSUB_1:25

for b₁, b₂ being set holds (Fin b₁) \/ (Fin b₂) c= Fin (b₁ \/ b₂)

proof end;

theorem Th26: :: FINSUB_1:26

for b₁ being set holds Fin b₁ c= bool b₁

proof end;

theorem Th27: :: FINSUB_1:27

for b₁ being set st b₁ is finite holds
Fin b₁ = bool b₁

proof end;

theorem Th28: :: FINSUB_1:28

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

definition

let c₁ be set ;
mode Finite_Subset of a₁ is Element of Fin a₁;

end;

theorem Th29: :: FINSUB_1:29

canceled;

theorem Th30: :: FINSUB_1:30

for b₁ being set
for b₂ being Finite_Subset of b₁ holds b₂ is finite ;

theorem Th31: :: FINSUB_1:31

canceled;

theorem Th32: :: FINSUB_1:32

for b₁ being set
for b₂ being Finite_Subset of b₁ holds b₂ is Subset of b₁ by Def5;

theorem Th33: :: FINSUB_1:33

canceled;

theorem Th34: :: FINSUB_1:34

for b₁ being set
for b₂ being Subset of b₁ st b₁ is finite holds
b₂ is Finite_Subset of b₁

proof end;