Copyright (c) 1989 Association of Mizar Users
environ
vocabulary FUNCT_1, RELAT_1, ORDINAL2, BOOLE, ORDINAL1, ORDINAL3, SETFAM_1,
TARSKI, MCART_1, FINSET_1;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
MCART_1, SETFAM_1, ORDINAL1, ORDINAL2, ORDINAL3;
constructors ENUMSET1, MCART_1, ORDINAL3, SETFAM_1, XBOOLE_0;
clusters FUNCT_1, ORDINAL2, RELAT_1, ARYTM_3, ORDINAL1, SUBSET_1, ZFMISC_1,
XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0;
theorems FUNCT_1, ENUMSET1, MCART_1, ZFMISC_1, TARSKI, RELAT_1, ORDINAL3,
ORDINAL2, ORDINAL1, SETFAM_1, XBOOLE_0, XBOOLE_1;
schemes FUNCT_1, PARTFUN1, ORDINAL2, XBOOLE_0;
begin
definition let IT be set;
attr IT is finite means
:Def1: ex p being Function st rng p = IT & dom p in omega;
antonym IT is infinite;
end;
reserve A, B, C, D, X, Y, Z, x, y for set;
reserve f for Function;
Lm1: {x} is finite
proof
deffunc F(set) = x;
consider p being Function such that
A1: dom p = {{}} and
A2: for y st y in {{}} holds p.y = F(y) from Lambda;
take p;
for y holds y in {x} iff ex x st x in dom p & y = p.x
proof let y;
thus y in {x} implies ex x st x in dom p & y = p.x
proof assume y in {x};
then A3: y = x by TARSKI:def 1;
take {};
thus {} in dom p by A1,TARSKI:def 1;
{} in {{}} by TARSKI:def 1;
hence y = p.{} by A2,A3;
end;
assume ex z be set st z in dom p & y = p.z;
then y = x by A1,A2;
hence y in {x} by TARSKI:def 1;
end;
hence rng p = {x} by FUNCT_1:def 5;
thus thesis by A1,ORDINAL1:41,ORDINAL2:19,def 4,ORDINAL3:18;
end;
definition
cluster non empty finite set;
existence proof consider x; {x} is finite by Lm1; hence thesis; end;
end;
definition
cluster empty -> finite set;
coherence
proof let A be set;
assume
A1: A is empty;
take {};
thus rng {} = A by A1;
thus thesis by ORDINAL2:def 5;
end;
end;
definition let X be set;
cluster empty finite Subset of X;
existence
proof
take {} X;
thus thesis;
end;
end;
scheme OLambdaC{A()->set,C[set],F(set)->set,G(set)->set}:
ex f being Function st dom f = A() &
for x being Ordinal st x in A() holds
(C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x))
proof
defpred C'[set] means C[$1];
deffunc F'(set) = F($1);
deffunc G'(set) = G($1);
consider f being Function such that
A1: dom f = A() &
for x being set st x in A() holds
(C'[x] implies f.x = F'(x)) & (not C'[x] implies f.x = G'(x))
from LambdaC;
take f;
thus thesis by A1;
end;
Lm2: A is finite & B is finite implies A \/ B is finite
proof
given p be Function such that
A1: rng p = A and
A2: dom p in omega;
given q be Function such that
A3: rng q = B and
A4: dom q in omega;
reconsider domp = dom p, domq = dom q as Ordinal by A2,A4,ORDINAL1:23;
deffunc F(Ordinal) = p.$1;
deffunc G(Ordinal) = q.($1-^domp);
defpred P[set] means $1 in domp;
consider f such that
A5: dom f = domp+^domq and
A6: for x being Ordinal st x in domp+^domq holds
(P[x] implies f.x = F(x)) & (not P[x] implies f.x = G(x))
from OLambdaC;
take f;
reconsider domp, domq as natural Ordinal by A2,A4,ORDINAL2:def 21;
thus rng f = A \/ B
proof
thus rng f c= A \/ B
proof let y; assume y in rng f;
then consider x such that
A7: x in dom f & y = f.x by FUNCT_1:def 5;
reconsider x as Ordinal by A5,A7,ORDINAL1:23;
per cases;
suppose x in domp;
then y = p.x & p.x in rng p by A5,A6,A7,FUNCT_1:def 5;
hence thesis by A1,XBOOLE_0:def 2;
suppose not x in domp;
then A8: domp c= x & y = q.(x-^domp) by A5,A6,A7,ORDINAL1:26;
then (domp)+^(x-^domp) = x & y = q.(x-^domp)
by ORDINAL3:def 6;
then x-^domp in dom q by A5,A7,ORDINAL3:25;
then y in B by A3,A8,FUNCT_1:def 5;
hence thesis by XBOOLE_0:def 2;
end;
let x;
assume
A9: x in A \/ B;
per cases by A1,A3,A9,XBOOLE_0:def 2;
suppose x in rng p;
then consider y such that
A10: y in dom p and
A11: x = p.y by FUNCT_1:def 5;
y in domp by A10;
then A12: y is Ordinal by ORDINAL1:23;
A13: dom p c= dom f by A5,ORDINAL3:27;
then x = f.y by A5,A6,A10,A11,A12;
hence x in rng f by A10,A13,FUNCT_1:def 5;
suppose x in rng q;
then consider y such that
A14: y in domq and
A15: x = q.y by FUNCT_1:def 5;
reconsider y as Ordinal by A14,ORDINAL1:23;
set z = domp +^ y;
domp c= z by ORDINAL3:27;
then A16: not z in domp by ORDINAL1:7;
A17: z in dom f by A5,A14,ORDINAL3:20;
x = q.(z-^domp) by A15,ORDINAL3:65
.= f.z by A5,A6,A16,A17;
hence x in rng f by A17,FUNCT_1:def 5;
end;
domp+^domq is natural;
hence thesis by A5,ORDINAL2:def 21;
end;
definition let x be set;
cluster {x} -> finite;
coherence by Lm1;
end;
definition let X be non empty set;
cluster non empty finite Subset of X;
existence
proof
consider x being set such that
A1:x in X by XBOOLE_0:def 1;
take {x};
thus thesis by A1,ZFMISC_1:37;
end;
end;
definition
let x,y be set;
cluster {x,y} -> finite;
coherence
proof
{x,y} is finite
proof
{x,y} = {x} \/ {y} & {x} is finite & {y} is finite by ENUMSET1:41;
hence thesis by Lm2;
end;
hence thesis;
end;
end;
definition
let x,y,z be set;
cluster {x,y,z} -> finite;
coherence
proof
{x,y,z} is finite
proof
{x,y,z} = {x} \/ {y,z} & {x} is finite & {y,z}is finite
by ENUMSET1:42;
hence thesis by Lm2;
end;
hence thesis;
end;
end;
definition
let x1,x2,x3,x4 be set;
cluster {x1,x2,x3,x4} -> finite;
coherence
proof
{x1,x2,x3,x4} is finite
proof
{x1,x2,x3,x4} = {x1} \/ {x2,x3,x4} & {x1} is finite & {x2,x3,x4}is
finite
by ENUMSET1:44;
hence thesis by Lm2;
end;
hence thesis;
end;
end;
definition
let x1,x2,x3,x4,x5 be set;
cluster {x1,x2,x3,x4,x5} -> finite;
coherence
proof
{x1,x2,x3,x4,x5} is finite
proof
{x1,x2,x3,x4,x5} = {x1} \/ {x2,x3,x4,x5} & {x1} is finite &
{x2,x3,x4,x5} is finite by ENUMSET1:47;
hence thesis by Lm2;
end;
hence thesis;
end;
end;
definition
let x1,x2,x3,x4,x5,x6 be set;
cluster {x1,x2,x3,x4,x5,x6} -> finite;
coherence
proof
{x1,x2,x3,x4,x5,x6} is finite
proof
{x1,x2,x3,x4,x5,x6} = {x1} \/ {x2,x3,x4,x5,x6} & {x1} is finite &
{x2,x3,x4,x5,x6} is finite by ENUMSET1:51;
hence thesis by Lm2;
end;
hence thesis;
end;
end;
definition
let x1,x2,x3,x4,x5,x6,x7 be set;
cluster {x1,x2,x3,x4,x5,x6,x7} -> finite;
coherence
proof
{x1,x2,x3,x4,x5,x6,x7} is finite
proof
{x1,x2,x3,x4,x5,x6,x7} = {x1} \/ {x2,x3,x4,x5,x6,x7} & {x1} is finite &
{x2,x3,x4,x5,x6,x7} is finite by ENUMSET1:56;
hence thesis by Lm2;
end;
hence thesis;
end;
end;
definition
let x1,x2,x3,x4,x5,x6,x7,x8 be set;
cluster {x1,x2,x3,x4,x5,x6,x7,x8} -> finite;
coherence
proof
{x1,x2,x3,x4,x5,x6,x7,x8} is finite
proof
{x1,x2,x3,x4,x5,x6,x7,x8} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8} &
{x1} is finite &
{x2,x3,x4,x5,x6,x7,x8} is finite by ENUMSET1:62;
hence thesis by Lm2;
end;
hence thesis;
end;
end;
definition let B be finite set;
cluster -> finite Subset of B;
coherence
proof let A be Subset of B;
per cases;
suppose A is empty;
then A = {};
hence thesis;
suppose A is non empty;
then consider x1 be set such that
A1: x1 in A by XBOOLE_0:def 1;
consider p be Function such that
A2: rng p = B and
A3: dom p in omega by Def1;
deffunc F(set) = p.$1;
deffunc G(set) = x1;
defpred P[set] means p.$1 in A;
consider q be Function such that
A4: dom q = dom p and
A5: for x st x in dom p holds
(P[x] implies q.x = F(x)) &
(not P[x] implies q.x = G(x)) from LambdaC;
now let y;
thus y in A implies ex x st x in dom q & y = q.x
proof assume
A6: y in A;
then consider x such that
A7: x in dom p and
A8: p.x = y by A2,FUNCT_1:def 5;
take x;
thus x in dom q by A4,A7;
thus y = q.x by A5,A6,A7,A8;
end;
given x such that
A9: x in dom q and
A10: y = q.x;
per cases;
suppose p.x in A;
hence y in A by A4,A5,A9,A10;
suppose not p.x in A;
hence y in A by A1,A4,A5,A9,A10;
end;
then rng q = A by FUNCT_1:def 5;
hence thesis by A3,A4,Def1;
end;
end;
definition let X,Y be finite set;
cluster X \/ Y -> finite;
coherence by Lm2;
end;
canceled 12;
theorem
Th13: A c= B & B is finite implies A is finite
proof
assume that A1: A c= B and A2: B is finite;
reconsider B as finite set by A2;
reconsider A as Subset of B by A1;
A is finite;
hence thesis;
end;
theorem
A is finite & B is finite implies A \/ B is finite by Lm2;
definition let A be set, B be finite set;
cluster A /\ B -> finite;
coherence
proof
A /\ B is finite
proof
A /\ B c= B by XBOOLE_1:17;
hence thesis by Th13;
end;
hence thesis;
end;
end;
definition let A be finite set, B be set;
cluster A /\ B -> finite;
coherence
proof
A /\ B is finite
proof
A /\ B c= A by XBOOLE_1:17;
hence thesis by Th13;
end;
hence thesis;
end;
cluster A \ B -> finite;
coherence
proof
A \ B is finite
proof
A \ B c= A by XBOOLE_1:36;
hence thesis by Th13;
end;
hence thesis;
end;
end;
theorem Th15:
A is finite implies A /\ B is finite
proof
A /\ B c= A & B /\ A c= A by XBOOLE_1:17;
hence thesis by Th13;
end;
theorem
A is finite implies A \ B is finite
proof
A \ B c= A by XBOOLE_1:36;
hence thesis by Th13;
end;
theorem
Th17: A is finite implies f.:A is finite
proof
set B = dom f /\ A;
assume A is finite;
then B is finite by Th15;
then consider p be Function such that
A1: rng p=B and
A2: dom p in omega by Def1;
take f*p;
rng (f*p) = f.:B by A1,RELAT_1:160;
hence rng (f*p) = f.:A by RELAT_1:145;
B c= dom f by XBOOLE_1:17;
hence dom(f*p) in omega by A1,A2,RELAT_1:46;
end;
definition let f be Function, A be finite set;
cluster f.:A -> finite;
coherence by Th17;
end;
reserve O for Ordinal;
theorem
Th18: A is finite implies for X being Subset-Family of A st X <> {}
ex x being set st
x in X & for B being set st B in X holds x c= B implies B = x
proof
assume A1: A is finite;
let X be Subset-Family of A such that A2: X <> {};
consider p be Function such that
A3: rng p = A and
A4: dom p in omega by A1,Def1;
defpred P[set] means p.:$1 in X;
consider G being set such that
A5: for x holds x in G iff x in bool dom p & P[x] from Separation;
G c= bool dom p
proof
let x; assume x in G;
hence thesis by A5;
end;
then reconsider GX=G as Subset-Family of dom p by SETFAM_1:def 7;
consider x being Element of X;
x is Subset of A by A2,TARSKI:def 3;
then A6: p.:(p"x) = x by A3,FUNCT_1:147;
p"x c= dom p by RELAT_1:167;
then A7: GX <> {} by A2,A5,A6;
defpred P[set] means
$1 in omega implies for X being Subset-Family of $1 st X <> {}
ex x being set st
x in X & for B being set st B in X holds x c= B implies B = x;
A8: P[{}]
proof assume {} in omega;
let X be Subset-Family of {}; assume X <> {};
then A9: X = {{}} by ZFMISC_1:1,39;
take {};
thus thesis by A9,TARSKI:def 1;
end;
A10: P[O] implies P[succ O]
proof
assume A11: O in omega implies
for X being Subset-Family of O st X <> {}
ex x being set st
x in X & for B being set st B in X holds x c= B implies B = x;
thus succ O in omega implies
for X being Subset-Family of succ O st X <> {}
ex x being set st
x in X & for B being set st B in X holds x c= B implies B = x
proof assume succ O in omega;
then A12: succ O c= omega by ORDINAL1:def 2;
let X be Subset-Family of succ O such that A13: X <> {};
defpred P[set] means ex A st A in X & $1 = A \ {O};
consider X1 being set such that
A14: for x holds x in X1 iff x in bool O &
P[x] from Separation;
X1 c= bool O
proof
let x; assume x in X1;
hence thesis by A14;
end;
then reconsider X2=X1 as Subset-Family of O by SETFAM_1:def 7;
consider y being Element of X;
A15: succ O = O \/ {O} by ORDINAL1:def 1;
y is Subset of succ O by A13,TARSKI:def 3;
then y \ {O} c= (O \/ {O}) \ {O} by A15,XBOOLE_1:33;
then A16: y \ {O} c= O \ {O} by XBOOLE_1:40;
A17: O in succ O by ORDINAL1:10;
A18: not O in O;
then y \ {O} c= O by A16,ZFMISC_1:65;
then X2 <> {} by A13,A14;
then consider Z such that A19: Z in X2 &
for B being set st B in
X2 holds Z c= B implies B = Z by A11,A12,A17;
consider X1 being set such that
A20: X1 in X & Z=X1 \ {O} by A14,A19;
A21: O in {O} by TARSKI:def 1;
then A22: not O in Z by A20,XBOOLE_0:def 4;
A23: now assume A24: Z \/ {O} in X;
take A=Z \/ {O};
for B being set st B in X holds A c= B implies B = A
proof
let B such that A25: B in X;
assume A26: A c= B;
A27: now assume A28: O in B;
set Y = B \ {O};
{O} c= B by A28,ZFMISC_1:37;
then A29: B = Y \/ {O} by XBOOLE_1:45;
A \ {O} c= Y by A26,XBOOLE_1:33;
then Z \ {O} c= Y & not O in Z by A20,A21,XBOOLE_0:def 4,
XBOOLE_1:40;
then A30: Z c= Y by ZFMISC_1:65;
Y c= (O \/ {O}) \ {O} by A15,A25,XBOOLE_1:33;
then Y c= O \ {O} by XBOOLE_1:40;
then Y c= O by A18,ZFMISC_1:65;
then Y in X2 by A14,A25;
hence thesis by A19,A29,A30;
end;
now assume A31: not O in B;
O in {O} by TARSKI:def 1;
then O in A by XBOOLE_0:def 2;
hence contradiction by A26,A31;
end;
hence thesis by A27;
end;
hence thesis by A24;
end;
now assume A32: not Z \/ {O} in X;
take A=Z;
now assume O in X1;
then X1 = X1 \/ {O} by ZFMISC_1:46
.= Z \/ {O} by A20,XBOOLE_1:39;
hence contradiction by A20,A32;
end;
then A33: A in X by A20,ZFMISC_1:65;
for B being set st B in X holds A c= B implies B = A
proof
let B; assume A34: B in X;
then B \ {O} c= (O \/ {O}) \ {O} by A15,XBOOLE_1:33;
then B \ {O} c= O \ {O} by XBOOLE_1:40;
then B \ {O} c= O by A18,ZFMISC_1:65;
then A35: B \ {O} in X2 by A14,A34;
assume A36: A c= B;
then A \ {O} c= B \ {O} by XBOOLE_1:33;
then A37: A c= B \ {O} by A22,ZFMISC_1:65;
A38: now assume A39: O in B;
A \/ {O} = (B \ {O}) \/ {O} by A19,A35,A37
.= B \/ {O} by XBOOLE_1:39
.= B by A39,ZFMISC_1:46;
hence contradiction by A32,A34;
end;
B c= O
proof
let x such that A40: x in B;
x in O or x in {O} by A15,A34,A40,XBOOLE_0:def 2;
hence thesis by A38,A40,TARSKI:def 1;
end;
then B \ {O} = B & B in bool O by A38,ZFMISC_1:65;
then B in X2 by A14,A34;
hence thesis by A19,A36;
end;
hence thesis by A33;
end;
hence thesis by A23;
end;
end;
A41: O <> {} & O is_limit_ordinal & (for B being Ordinal st B in O holds P[B])
implies P[O]
proof assume that
A42: O <> {} and
A43: O is_limit_ordinal and for B being Ordinal st B in O holds P[B] and
A44: O in omega;
{} in O by A42,ORDINAL1:24;
then omega c= O by A43,ORDINAL2:def 5;
then O in O by A44;
hence thesis;
end;
A45: P[O] from Ordinal_Ind(A8,A10,A41);
dom p is Ordinal by A4,ORDINAL1:23;
then consider g being set such that
A46: g in GX &
for B being set st B in GX holds g c= B implies B=g by A4,A7,A45;
take p.:g;
for B st B in X holds p.:g c= B implies B = p.:g
proof
let B; assume A47: B in X;
assume p.:g c= B;
then A48: p"(p.:g) c= p"B by RELAT_1:178;
g c= p"(p.:g) by A46,FUNCT_1:146;
then A49: g c= p"B by A48,XBOOLE_1:1;
A50: p.:(p"B) = B by A3,A47,FUNCT_1:147;
p"B c= dom p by RELAT_1:167;
then p"B in GX by A5,A47,A50;
hence thesis by A46,A49,A50;
end;
hence thesis by A5,A46;
end;
scheme Finite{A()->set,P[set]} : P[A()]
provided
A1: A() is finite and
A2: P[{}] and
A3: for x,B being set st x in A() & B c= A() & P[B] holds P[B \/ {x}]
proof
now assume A() <> {};
defpred R[set] means ex B st B=$1 & P[B];
consider G being set such that
A4: for x holds x in G iff x in bool A() & R[x] from Separation;
G c= bool A()
proof
let x; assume x in G;
hence thesis by A4;
end;
then reconsider GA=G as Subset-Family of A() by SETFAM_1:def 7;
{} c= A() by XBOOLE_1:2;
then GA <> {} by A2,A4;
then consider B such that A5:
B in GA & for X being set st X in GA holds B c= X implies B=X by A1,Th18;
A6: B in bool A() & ex A st A = B & P[A] by A4,A5;
now consider x being Element of A() \ B;
assume B <> A();
then not A() c= B by A5,XBOOLE_0:def 10;
then A7: A() \ B <> {} by XBOOLE_1:37;
then A8: x in A() by XBOOLE_0:def 4;
then A9: P[B \/ {x}] by A3,A6;
{x} c= A() by A8,ZFMISC_1:37;
then B \/ {x} c= A() by A5,XBOOLE_1:8;
then A10: B \/ {x} in GA by A4,A9;
not x in B by A7,XBOOLE_0:def 4;
then not {x} c= B by ZFMISC_1:37;
then B c= B \/ {x} & B \/ {x} <> B by XBOOLE_1:7;
hence contradiction by A5,A10;
end;
hence thesis by A6;
end;
hence thesis by A2;
end;
Lm3:
A is finite & (for X st X in A holds X is finite) implies union A is finite
proof
assume that A1:A is finite and
A2:(for X st X in A holds X is finite);
defpred P[set] means ex B st B=$1 & union B is finite;
consider G being set such that
A3: for x holds x in G iff x in bool A & P[x] from Separation;
defpred P[set] means $1 in G;
{} c= A by XBOOLE_1:2;
then A4: P[{}] by A3,ZFMISC_1:2;
A5: for x,B being set st x in A & B c= A & P[B] holds P[B \/ {x}]
proof
let x,B be set;
assume that A6: x in A and B c= A and A7: B in G;
ex X st X=B & union X is finite by A3,A7;
then A8: union B is finite & x is finite by A2,A6;
union (B \/ {x}) = union B \/ union {x} by ZFMISC_1:96
.= union B \/ x by ZFMISC_1:31;
then A9: union (B \/ {x}) is finite by A8,Lm2;
{x} c= A by A6,ZFMISC_1:37;
then B in bool A & {x} in bool A by A3,A7;
then B \/ {x} c= A by XBOOLE_1:8;
hence thesis by A3,A9;
end;
P[A] from Finite(A1,A4,A5);
then ex X st X=A & union X is finite by A3;
hence thesis;
end;
theorem Th19:
A is finite & B is finite implies [:A,B:] is finite
proof
assume that A1: A is finite and A2: B is finite;
A3: for y holds [:A,{y}:] is finite
proof
let y;
deffunc F(set) = [$1,y];
consider f such that A4: dom f=A &
for x st x in A holds f.x=F(x) from Lambda;
for x holds x in rng f iff x in [:A,{y}:]
proof
let x;
thus x in rng f implies x in [:A,{y}:]
proof
assume x in rng f;
then consider z be set such that A5: z in dom f and A6: f.z = x
by FUNCT_1:def 5;
x = [z,y] & y in {y} by A4,A5,A6,TARSKI:def 1;
hence thesis by A4,A5,ZFMISC_1:129;
end;
thus x in [:A,{y}:] implies x in rng f
proof
assume x in [:A,{y}:];
then consider x1,x2 be set such that A7: x1 in A and A8: x2 in {y} and
A9: x=[x1,x2] by ZFMISC_1:def 2;
x2=y by A8,TARSKI:def 1;
then x = f.x1 by A4,A7,A9;
hence thesis by A4,A7,FUNCT_1:def 5;
end;
end;
then rng f = [:A,{y}:] by TARSKI:2;
then f.:A=[:A,{y}:] by A4,RELAT_1:146;
hence thesis by A1,Th17;
end;
defpred P[set] means ex y st y in B & $1 = [:A,{y}:];
consider G being set such that
A10: for x holds x in G iff x in bool [:A,B:] & P[x] from Separation;
for x holds x in union G iff x in [:A,B:]
proof
let x;
thus x in union G implies x in [:A,B:]
proof
assume x in union G;
then consider X such that A11: x in X and A12: X in G by TARSKI:def 4;
X in bool [:A,B:]by A10,A12;
hence thesis by A11;
end;
assume x in [:A,B:];
then consider y,z be set such that
A13: y in A and A14: z in B and A15: x=[y,z]
by ZFMISC_1:def 2;
A16: [y,z] in [:A,{z}:] by A13,ZFMISC_1:129;
{z} c= B by A14,ZFMISC_1:37;
then [:A,{z}:] c= [:A,B:] by ZFMISC_1:118;
then [:A,{z}:] in G by A10,A14;
hence thesis by A15,A16,TARSKI:def 4;
end;
then A17: union G = [:A,B:] by TARSKI:2;
deffunc F(set) = [:A,{$1}:];
consider g being Function such that A18: dom g = B &
for x st x in B holds g.x = F(x) from Lambda;
for x holds x in rng g iff x in G
proof
let x;
thus x in rng g implies x in G
proof
assume x in rng g;
then consider y such that A19: y in dom g and A20: g.y = x by FUNCT_1:def
5;
A21: x = [:A,{y}:] by A18,A19,A20;
{y} c= B by A18,A19,ZFMISC_1:37;
then x c= [:A,B:] by A21,ZFMISC_1:118;
hence thesis by A10,A18,A19,A21;
end;
assume x in G;
then consider y such that A22: y in B and A23: x = [:A,{y}:] by A10;
x = g.y by A18,A22,A23;
hence thesis by A18,A22,FUNCT_1:def 5;
end;
then rng g = G by TARSKI:2;
then g.:B = G by A18,RELAT_1:146;
then A24: G is finite by A2,Th17;
for X st X in G holds X is finite
proof
let X; assume X in G;
then ex y st y in B & X=[:A,{y}:] by A10;
hence thesis by A3;
end;
hence thesis by A17,A24,Lm3;
end;
definition let A,B be finite set;
cluster [:A,B:] -> finite;
coherence by Th19;
end;
theorem Th20:
A is finite & B is finite & C is finite
implies [:A,B,C:] is finite
proof
assume A1: A is finite & B is finite & C is finite;
then [:A,B:] is finite by Th19;
then [:[:A,B:],C:] is finite by A1,Th19;
hence thesis by ZFMISC_1:def 3;
end;
definition let A,B,C be finite set;
cluster [:A,B,C:] -> finite;
coherence by Th20;
end;
theorem Th21:
A is finite & B is finite & C is finite & D is finite
implies [:A,B,C,D:] is finite
proof
assume A1: A is finite & B is finite & C is finite & D is finite;
then [:A,B,C:] is finite by Th20;
then [:[:A,B,C:],D:] is finite by A1,Th19;
hence thesis by ZFMISC_1:def 4;
end;
definition let A,B,C,D be finite set;
cluster [:A,B,C,D:] -> finite;
coherence by Th21;
end;
theorem
B <> {} & [:A,B:] is finite implies A is finite
proof
assume that A1: B<>{} and A2: [:A,B:] is finite;
deffunc F(set) = $1`1;
consider f such that A3: dom f = [:A,B:] and
A4: for x st x in [:A,B:] holds f.x = F(x) from Lambda;
x in rng f iff x in A
proof
thus x in rng f implies x in A
proof
assume x in rng f;
then consider y such that A5: y in dom f and A6: f.y = x by FUNCT_1:def
5;
x = y`1 by A3,A4,A5,A6;
hence thesis by A3,A5,MCART_1:10;
end;
assume A7: x in A;
consider y being Element of B;
A8: [x,y] in dom f by A1,A3,A7,ZFMISC_1:106;
then f.([x,y]) = [x,y]`1 by A3,A4
.= x by MCART_1:7;
hence thesis by A8,FUNCT_1:def 5;
end;
then rng f = A by TARSKI:2;
then f.:[:A,B:] = A by A3,RELAT_1:146;
hence A is finite by A2,Th17;
end;
theorem
A <> {} & [:A,B:] is finite implies B is finite
proof
assume that A1: A<>{} and A2: [:A,B:] is finite;
deffunc F(set) = $1`2;
consider f such that A3: dom f = [:A,B:] and
A4: for x st x in [:A,B:] holds f.x = F(x) from Lambda;
y in rng f iff y in B
proof
thus y in rng f implies y in B
proof
assume y in rng f;
then consider x such that A5: x in dom f and A6: f.x = y by FUNCT_1:def
5;
y = x`2 by A3,A4,A5,A6;
hence thesis by A3,A5,MCART_1:10;
end;
assume A7: y in B;
consider x being Element of A;
A8: [x,y] in dom f by A1,A3,A7,ZFMISC_1:106;
[x,y]`2 = y by MCART_1:7;
then f.([x,y]) = y by A3,A4,A8;
hence thesis by A8,FUNCT_1:def 5;
end;
then rng f = B by TARSKI:2;
then f.:[:A,B:] = B by A3,RELAT_1:146;
hence B is finite by A2,Th17;
end;
theorem Th24:
A is finite iff bool A is finite
proof
thus A is finite implies bool A is finite
proof
assume A1: A is finite;
defpred P[set] means ex B st B=$1 & bool B is finite;
consider G being set such that A2: for x holds x in G iff
x in bool A & P[x] from Separation;
defpred P[set] means $1 in G;
{} c= A by XBOOLE_1:2;
then A3: P[{}] by A2,ZFMISC_1:1;
A4: for x,B being set st x in A & B c= A & P[B] holds P[B \/ {x}]
proof
let x,B be set; assume that A5:x in A and B c= A and A6:B in G;
A7: now assume x in B;
then {x} c= B by ZFMISC_1:37;
hence thesis by A6,XBOOLE_1:12;
end;
now assume A8: not x in B;
defpred P[set,set] means ex Y st Y=$1 & $2=Y \/ {x};
A9: for y,y1,y2 be set st y in bool B & P[y,y1] & P[y,y2] holds y1 = y2;
A10: for y st y in bool B ex z be set st P[y,z]
proof
let y such that y in bool B;
ex Y st Y=y & y \/ {x} = Y \/ {x};
hence thesis;
end;
consider f such that A11: dom f = bool B and
A12: for y st y in bool B holds P[y,f.y] from FuncEx(A9,A10);
A13: ex A st B=A & bool A is finite by A2,A6;
then A14: f.:(bool B) is finite by Th17;
y in rng f iff y in bool(B \/ {x}) \ bool B
proof
thus y in rng f implies y in bool(B \/ {x}) \ bool B
proof
assume y in rng f;
then consider x1 be set such that A15: x1 in dom f and A16: f.x1=y
by FUNCT_1:def 5;
consider X1 being set such that A17: X1=x1 & f.x1= X1 \/ {x}
by A11,A12,A15;
A18: X1 \/ {x} c= B \/ {x} by A11,A15,A17,XBOOLE_1:13;
x in {x} by TARSKI:def 1;
then x in y & not x in B by A8,A16,A17,XBOOLE_0:def 2;
then not y in bool B;
hence thesis by A16,A17,A18,XBOOLE_0:def 4;
end;
assume A19: y in bool(B \/ {x}) \ bool B;
then A20: y in bool(B \/ {x}) & not y in bool B by XBOOLE_0:def 4;
set Z=y \ {x};
A21: now assume A22: not x in y;
y c= B
proof
let z be set; assume z in y;
then z in B \/ {x} & not z in {x} by A20,A22,TARSKI:def 1;
hence thesis by XBOOLE_0:def 2;
end;
hence contradiction by A19,XBOOLE_0:def 4;
end;
A23: Z c= B by A20,XBOOLE_1:43;
then consider X such that A24: X=Z and A25: f.Z = X \/ {x} by A12;
X \/ {x} = y \/ {x} by A24,XBOOLE_1:39
.= y by A21,ZFMISC_1:46;
hence thesis by A11,A23,A25,FUNCT_1:def 5;
end;
then rng f = bool(B \/ {x}) \ bool B by TARSKI:2;
then A26: f.:(bool B) = bool(B \/ {x}) \ bool B by A11,RELAT_1:146;
B c= B \/ {x} by XBOOLE_1:7;
then A27: bool B c= bool(B \/ {x}) by ZFMISC_1:79;
(bool(B \/ {x}) \ bool B) \/ bool B = bool(B \/ {x}) \/
bool B by XBOOLE_1:39
.= bool(B \/ {x}) by A27,XBOOLE_1:12;
then A28: bool(B \/ {x}) is finite by A13,A14,A26,Lm2;
{x} c= A by A5,ZFMISC_1:37;
then B in bool A & {x} in bool A by A2,A6;
then B \/ {x} c= A by XBOOLE_1:8;
hence thesis by A2,A28;
end;
hence thesis by A7;
end;
P[A] from Finite(A1,A3,A4);
then ex X st X=A & bool X is finite by A2;
hence thesis;
end;
thus bool A is finite implies A is finite
proof
assume A29: bool A is finite;
defpred P[set] means ex y st $1={y};
consider X being set such that
A30: for x holds x in X iff x in bool A & P[x] from Separation;
for x holds x in union X iff x in A
proof
let x;
thus x in union X implies x in A
proof
assume x in union X;
then consider B such that A31: x in B and A32: B in X by TARSKI:def 4;
B in bool A by A30,A32;
hence thesis by A31;
end;
assume x in A;
then {x} c= A by ZFMISC_1:37;
then A33: {x} in X by A30;
x in {x} by TARSKI:def 1;
hence thesis by A33,TARSKI:def 4;
end;
then A34: union X = A by TARSKI:2;
A35: for B st B in X holds B is finite
proof
let B; assume B in X;
then ex y st B = {y} by A30;
hence thesis;
end;
X c= bool A
proof
let x; assume x in X;
hence thesis by A30;
end;
then X is finite by A29,Th13;
hence thesis by A34,A35,Lm3;
end;
end;
theorem
A is finite & (for X st X in A holds X is finite) iff union A is finite
proof
thus A is finite & (for X st X in A holds X is finite) implies
union A is finite by Lm3;
thus union A is finite implies
A is finite & for X st X in A holds X is finite
proof
assume A1: union A is finite;
then A2: bool union A is finite by Th24;
A c= bool union A by ZFMISC_1:100;
hence A is finite by A2,Th13;
thus for X st X in A holds X is finite
proof
let X; assume X in A;
then X c= union A by ZFMISC_1:92;
hence thesis by A1,Th13;
end;
end;
end;
theorem
dom f is finite implies rng f is finite
proof
assume dom f is finite;
then f.:(dom f) is finite by Th17;
hence thesis by RELAT_1:146;
end;
theorem
Y c= rng f & f"Y is finite implies Y is finite
proof
assume that A1: Y c= rng f and A2: f"Y is finite;
f.:(f"Y) = Y by A1,FUNCT_1:147;
hence thesis by A2,Th17;
end;