A1:
A is finite
;
defpred S1[ set ] means bool A is finite ;
consider G being set such that
A2:
for x being set holds
( x in G iff ( x in bool A & S1[x] ) )
from XFAMILY:sch 1();
defpred S2[ set ] means A in G;
A3:
bool {} is finite
by ZFMISC_1:1;
{} c= A
;
then A4:
S2[ {} ]
by A3, A2;
A5:
for x, B being set st x in A & B c= A & S2[B] holds
S2[B \/ {x}]
proof
let x,
B be
set ;
( x in A & B c= A & S2[B] implies S2[B \/ {x}] )
assume that A6:
x in A
and
B c= A
and A7:
B in G
;
S2[B \/ {x}]
A8:
(
x in B implies
S2[
B \/ {x}] )
by A7, XBOOLE_1:12, ZFMISC_1:31;
now ( not x in B implies S2[B \/ {x}] )assume A9:
not
x in B
;
S2[B \/ {x}]defpred S3[
object ,
object ]
means ex
Y being
set st
(
Y = A &
c2 = Y \/ {x} );
A10:
for
y,
y1,
y2 being
object st
y in bool B &
S3[
y,
y1] &
S3[
y,
y2] holds
y1 = y2
;
A11:
for
y being
object st
y in bool B holds
ex
z being
object st
S3[
y,
z]
consider f being
Function such that A12:
dom f = bool B
and A13:
for
y being
object st
y in bool B holds
S3[
y,
f . y]
from FUNCT_1:sch 2(A10, A11);
A14:
bool B is
finite
by A2, A7;
for
y being
object holds
(
y in rng f iff
y in (bool (B \/ {x})) \ (bool B) )
proof
let y be
object ;
( y in rng f iff y in (bool (B \/ {x})) \ (bool B) )
reconsider yy =
y as
set by TARSKI:1;
thus
(
y in rng f implies
y in (bool (B \/ {x})) \ (bool B) )
( y in (bool (B \/ {x})) \ (bool B) implies y in rng f )proof
assume
y in rng f
;
y in (bool (B \/ {x})) \ (bool B)
then consider x1 being
object such that A15:
x1 in dom f
and A16:
f . x1 = y
by FUNCT_1:def 3;
consider X1 being
set such that A17:
X1 = x1
and A18:
f . x1 = X1 \/ {x}
by A12, A13, A15;
A19:
X1 \/ {x} c= B \/ {x}
by A12, A15, A17, XBOOLE_1:13;
x in {x}
by TARSKI:def 1;
then
x in yy
by A16, A18, XBOOLE_0:def 3;
then
not
y in bool B
by A9;
hence
y in (bool (B \/ {x})) \ (bool B)
by A16, A18, A19, XBOOLE_0:def 5;
verum
end;
assume A20:
y in (bool (B \/ {x})) \ (bool B)
;
y in rng f
set Z =
yy \ {x};
A24:
yy \ {x} c= B
by A20, XBOOLE_1:43;
then consider X being
set such that A25:
X = yy \ {x}
and A26:
f . (yy \ {x}) = X \/ {x}
by A13;
X \/ {x} =
yy \/ {x}
by A25, XBOOLE_1:39
.=
y
by A21, ZFMISC_1:40
;
hence
y in rng f
by A12, A24, A26, FUNCT_1:def 3;
verum
end; then
rng f = (bool (B \/ {x})) \ (bool B)
by TARSKI:2;
then A27:
f .: (bool B) = (bool (B \/ {x})) \ (bool B)
by A12, RELAT_1:113;
A28:
bool B c= bool (B \/ {x})
by XBOOLE_1:7, ZFMISC_1:67;
A29:
((bool (B \/ {x})) \ (bool B)) \/ (bool B) =
(bool (B \/ {x})) \/ (bool B)
by XBOOLE_1:39
.=
bool (B \/ {x})
by A28, XBOOLE_1:12
;
A30:
{x} c= A
by A6, ZFMISC_1:31;
B in bool A
by A2, A7;
then
B \/ {x} c= A
by A30, XBOOLE_1:8;
hence
S2[
B \/ {x}]
by A2, A14, A27, A29;
verum end;
hence
S2[
B \/ {x}]
by A8;
verum
end;
S2[A]
from FINSET_1:sch 2(A1, A4, A5);
hence
bool A is finite
by A2; verum