A1: for y being set holds [:A,{y}:] is finite

proof

let y be set ; :: thesis: [:A,{y}:] is finite
deffunc H₁( object ) -> object = [A,y];
consider f being Function such that
A2: ( dom f = A & ( for x being object st x in A holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
for x being object holds
( x in rng f iff x in [:A,{y}:] )

proof

let x be object ; :: thesis: ( x in rng f iff x in [:A,{y}:] )
thus ( x in rng f implies x in [:A,{y}:] ) :: thesis: ( x in [:A,{y}:] implies x in rng f )

proof

assume x in rng f ; :: thesis: x in [:A,{y}:]
then consider z being object such that
A3: z in dom f and
A4: f . z = x by FUNCT_1:def 3;
x = [z,y] by A2, A3, A4;
hence x in [:A,{y}:] by A2, A3, ZFMISC_1:106; :: thesis: verum

end;

thus ( x in [:A,{y}:] implies x in rng f ) :: thesis: verum

proof

assume x in [:A,{y}:] ; :: thesis: x in rng f
then consider x1, x2 being object such that
A5: x1 in A and
A6: x2 in {y} and
A7: x = [x1,x2] by ZFMISC_1:def 2;
x2 = y by A6, TARSKI:def 1;
then x = f . x1 by A2, A5, A7;
hence x in rng f by A2, A5, FUNCT_1:def 3; :: thesis: verum

end;

end;

then rng f = [:A,{y}:] by TARSKI:2;
then f .: A = [:A,{y}:] by A2, RELAT_1:113;
hence [:A,{y}:] is finite ; :: thesis: verum

end;

defpred S₁[ set ] means ex y being set st
( y in B & A = [:A,{y}:] );
consider G being set such that
A8: for x being set holds
( x in G iff ( x in bool [:A,B:] & S₁[x] ) ) from XFAMILY:sch 1();
for x being object holds
( x in union G iff x in [:A,B:] )

proof

let x be object ; :: thesis: ( x in union G iff x in [:A,B:] )
thus ( x in union G implies x in [:A,B:] ) :: thesis: ( x in [:A,B:] implies x in union G )

proof

assume x in union G ; :: thesis: x in [:A,B:]
then consider X being set such that
A9: x in X and
A10: X in G by TARSKI:def 4;
X in bool [:A,B:] by A8, A10;
hence x in [:A,B:] by A9; :: thesis: verum

end;

assume x in [:A,B:] ; :: thesis: x in union G
then consider y, z being object such that
A11: y in A and
A12: z in B and
A13: x = [y,z] by ZFMISC_1:def 2;
A14: [y,z] in [:A,{z}:] by A11, ZFMISC_1:106;
{z} c= B by A12, ZFMISC_1:31;
then [:A,{z}:] c= [:A,B:] by ZFMISC_1:95;
then [:A,{z}:] in G by A8, A12;
hence x in union G by A13, A14, TARSKI:def 4; :: thesis: verum

end;

then A15: union G = [:A,B:] by TARSKI:2;
deffunc H₁( object ) -> set = [:A,{A}:];
consider g being Function such that
A16: ( dom g = B & ( for x being object st x in B holds
g . x = H₁(x) ) ) from FUNCT_1:sch 3();
for x being object holds
( x in rng g iff x in G )

proof

let x be object ; :: thesis: ( x in rng g iff x in G )
reconsider xx = x as set by TARSKI:1;
thus ( x in rng g implies x in G ) :: thesis: ( x in G implies x in rng g )

proof

assume x in rng g ; :: thesis: x in G
then consider y being object such that
A17: y in dom g and
A18: g . y = x by FUNCT_1:def 3;
A19: x = [:A,{y}:] by A16, A17, A18;
{y} c= B by A16, A17, ZFMISC_1:31;
then xx c= [:A,B:] by A19, ZFMISC_1:95;
hence x in G by A8, A16, A17, A19; :: thesis: verum

end;

assume x in G ; :: thesis: x in rng g
then consider y being set such that
A20: y in B and
A21: x = [:A,{y}:] by A8;
x = g . y by A16, A20, A21;
hence x in rng g by A16, A20, FUNCT_1:def 3; :: thesis: verum

end;

then rng g = G by TARSKI:2;
then A22: g .: B = G by A16, RELAT_1:113;
for X being set st X in G holds
X is finite

proof

let X be set ; :: thesis: ( X in G implies X is finite )
assume X in G ; :: thesis: X is finite
then ex y being set st
( y in B & X = [:A,{y}:] ) by A8;
hence X is finite by A1; :: thesis: verum

end;

hence [:A,B:] is finite by A15, A22, Lm3; :: thesis: verum