:: FINSET_1 semantic presentation

definition
let c1 be set ;
attr a1 is finite means :Def1: :: FINSET_1:def 1
ex b1 being Function st
( rng b1 = a1 & dom b1 in omega );
end;

:: deftheorem Def1 defines finite FINSET_1:def 1 :
for b1 being set holds
( b1 is finite iff ex b2 being Function st
( rng b2 = b1 & dom b2 in omega ) );

notation
let c1 be set ;
antonym infinite c1 for finite c1;
end;

Lemma2: for b1 being set holds {b1} is finite
proof end;

registration
cluster non empty finite set ;
existence
ex b1 being set st
( not b1 is empty & b1 is finite )
proof end;
end;

registration
cluster empty -> finite set ;
coherence
for b1 being set st b1 is empty holds
b1 is finite
proof end;
end;

registration
let c1 be set ;
cluster empty finite Element of bool a1;
existence
ex b1 being Subset of c1 st
( b1 is empty & b1 is finite )
proof end;
end;

scheme :: FINSET_1:sch 1
s1{ F1() -> set , P1[ set ], F2( set ) -> set , F3( set ) -> set } :
ex b1 being Function st
( dom b1 = F1() & ( for b2 being Ordinal st b2 in F1() holds
( ( P1[b2] implies b1 . b2 = F2(b2) ) & ( P1[b2] implies b1 . b2 = F3(b2) ) ) ) )
proof end;

Lemma3: for b1, b2 being set st b1 is finite & b2 is finite holds
b1 \/ b2 is finite
proof end;

registration
let c1 be set ;
cluster {a1} -> finite ;
coherence
{c1} is finite by Lemma2;
end;

registration
let c1 be non empty set ;
cluster non empty finite Element of bool a1;
existence
ex b1 being Subset of c1 st
( not b1 is empty & b1 is finite )
proof end;
end;

registration
let c1, c2 be set ;
cluster {a1,a2} -> finite ;
coherence
{c1,c2} is finite
proof end;
end;

registration
let c1, c2, c3 be set ;
cluster {a1,a2,a3} -> finite ;
coherence
{c1,c2,c3} is finite
proof end;
end;

registration
let c1, c2, c3, c4 be set ;
cluster {a1,a2,a3,a4} -> finite ;
coherence
{c1,c2,c3,c4} is finite
proof end;
end;

registration
let c1, c2, c3, c4, c5 be set ;
cluster {a1,a2,a3,a4,a5} -> finite ;
coherence
{c1,c2,c3,c4,c5} is finite
proof end;
end;

registration
let c1, c2, c3, c4, c5, c6 be set ;
cluster {a1,a2,a3,a4,a5,a6} -> finite ;
coherence
{c1,c2,c3,c4,c5,c6} is finite
proof end;
end;

registration
let c1, c2, c3, c4, c5, c6, c7 be set ;
cluster {a1,a2,a3,a4,a5,a6,a7} -> finite ;
coherence
{c1,c2,c3,c4,c5,c6,c7} is finite
proof end;
end;

registration
let c1, c2, c3, c4, c5, c6, c7, c8 be set ;
cluster {a1,a2,a3,a4,a5,a6,a7,a8} -> finite ;
coherence
{c1,c2,c3,c4,c5,c6,c7,c8} is finite
proof end;
end;

registration
let c1 be finite set ;
cluster -> finite Element of bool a1;
coherence
for b1 being Subset of c1 holds b1 is finite
proof end;
end;

registration
let c1, c2 be finite set ;
cluster a1 \/ a2 -> finite ;
coherence
c1 \/ c2 is finite by Lemma3;
end;

theorem Th1: :: FINSET_1:1
canceled;

theorem Th2: :: FINSET_1:2
canceled;

theorem Th3: :: FINSET_1:3
canceled;

theorem Th4: :: FINSET_1:4
canceled;

theorem Th5: :: FINSET_1:5
canceled;

theorem Th6: :: FINSET_1:6
canceled;

theorem Th7: :: FINSET_1:7
canceled;

theorem Th8: :: FINSET_1:8
canceled;

theorem Th9: :: FINSET_1:9
canceled;

theorem Th10: :: FINSET_1:10
canceled;

theorem Th11: :: FINSET_1:11
canceled;

theorem Th12: :: FINSET_1:12
canceled;

theorem Th13: :: FINSET_1:13
for b1, b2 being set st b1 c= b2 & b2 is finite holds
b1 is finite
proof end;

theorem Th14: :: FINSET_1:14
for b1, b2 being set st b1 is finite & b2 is finite holds
b1 \/ b2 is finite by Lemma3;

registration
let c1 be set ;
let c2 be finite set ;
cluster a1 /\ a2 -> finite ;
coherence
c1 /\ c2 is finite
proof end;
end;

registration
let c1 be finite set ;
let c2 be set ;
cluster a1 /\ a2 -> finite ;
coherence
c1 /\ c2 is finite ;
cluster a1 \ a2 -> finite ;
coherence
c1 \ c2 is finite
proof end;
end;

theorem Th15: :: FINSET_1:15
for b1, b2 being set st b1 is finite holds
b1 /\ b2 is finite
proof end;

theorem Th16: :: FINSET_1:16
for b1, b2 being set st b1 is finite holds
b1 \ b2 is finite
proof end;

theorem Th17: :: FINSET_1:17
for b1 being set
for b2 being Function st b1 is finite holds
b2 .: b1 is finite
proof end;

registration
let c1 be Function;
let c2 be finite set ;
cluster a1 .: a2 -> finite ;
coherence
c1 .: c2 is finite by Th17;
end;

theorem Th18: :: FINSET_1:18
for b1 being set st b1 is finite holds
for b2 being Subset-Family of b1 st b2 <> {} holds
ex b3 being set st
( b3 in b2 & ( for b4 being set st b4 in b2 & b3 c= b4 holds
b4 = b3 ) )
proof end;

scheme :: FINSET_1:sch 2
s2{ F1() -> set , P1[ set ] } :
P1[F1()]
provided
E9: F1() is finite and
E10: P1[ {} ] and
E11: for b1, b2 being set st b1 in F1() & b2 c= F1() & P1[b2] holds
P1[b2 \/ {b1}]
proof end;

Lemma9: for b1 being set st b1 is finite & ( for b2 being set st b2 in b1 holds
b2 is finite ) holds
union b1 is finite
proof end;

theorem Th19: :: FINSET_1:19
for b1, b2 being set st b1 is finite & b2 is finite holds
[:b1,b2:] is finite
proof end;

registration
let c1, c2 be finite set ;
cluster [:a1,a2:] -> finite ;
coherence
[:c1,c2:] is finite by Th19;
end;

theorem Th20: :: FINSET_1:20
for b1, b2, b3 being set st b1 is finite & b2 is finite & b3 is finite holds
[:b1,b2,b3:] is finite
proof end;

registration
let c1, c2, c3 be finite set ;
cluster [:a1,a2,a3:] -> finite ;
coherence
[:c1,c2,c3:] is finite by Th20;
end;

theorem Th21: :: FINSET_1:21
for b1, b2, b3, b4 being set st b1 is finite & b2 is finite & b3 is finite & b4 is finite holds
[:b1,b2,b3,b4:] is finite
proof end;

registration
let c1, c2, c3, c4 be finite set ;
cluster [:a1,a2,a3,a4:] -> finite ;
coherence
[:c1,c2,c3,c4:] is finite by Th21;
end;

theorem Th22: :: FINSET_1:22
for b1, b2 being set st b1 <> {} & [:b2,b1:] is finite holds
b2 is finite
proof end;

theorem Th23: :: FINSET_1:23
for b1, b2 being set st b1 <> {} & [:b1,b2:] is finite holds
b2 is finite
proof end;

theorem Th24: :: FINSET_1:24
for b1 being set holds
( b1 is finite iff bool b1 is finite )
proof end;

theorem Th25: :: FINSET_1:25
for b1 being set holds
( ( b1 is finite & ( for b2 being set st b2 in b1 holds
b2 is finite ) ) iff union b1 is finite )
proof end;

theorem Th26: :: FINSET_1:26
for b1 being Function st dom b1 is finite holds
rng b1 is finite
proof end;

theorem Th27: :: FINSET_1:27
for b1 being set
for b2 being Function st b1 c= rng b2 & b2 " b1 is finite holds
b1 is finite
proof end;

theorem Th28: :: FINSET_1:28
for b1, b2 being set st b1 is finite & b2 is finite holds
b1 \+\ b2 is finite
proof end;

registration
let c1, c2 be finite set ;
cluster a1 \+\ a2 -> finite ;
coherence
c1 \+\ c2 is finite ;
end;

registration
let c1 be non empty set ;
cluster non empty finite Element of bool a1;
existence
ex b1 being Subset of c1 st
( b1 is finite & not b1 is empty )
proof end;
end;

theorem Th29: :: FINSET_1:29
for b1 being Function holds
( dom b1 is finite iff b1 is finite )
proof end;

theorem Th30: :: FINSET_1:30
for b1 being set st b1 is finite & b1 <> {} & b1 is c=-linear holds
ex b2 being set st
( b2 in b1 & ( for b3 being set st b3 in b1 holds
b2 c= b3 ) )
proof end;

theorem Th31: :: FINSET_1:31
for b1 being set st b1 is finite & b1 <> {} & b1 is c=-linear holds
ex b2 being set st
( b2 in b1 & ( for b3 being set st b3 in b1 holds
b3 c= b2 ) )
proof end;