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

proof

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

proof

let x be set ; :: 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 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 x in [:A,{y}:] by A4, A5, ZFMISC_1:129; :: 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 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 x in rng f by A4, A7, FUNCT_1:def 5; :: thesis: verum

end;

end;

then rng f = [:A,{y}:] by TARSKI:2;
then f .: A = [:A,{y}:] by A4, RELAT_1:146;
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
A10: for x being set holds
( x in G iff ( x in bool [:A,B:] & S₁[x] ) ) from XBOOLE_0:sch 1();
for x being set holds
( x in union G iff x in [:A,B:] )

proof

let x be set ; :: 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
A11: x in X and
A12: X in G by TARSKI:def 4;
X in bool [:A,B:] by A10, A12;
hence x in [:A,B:] by A11; :: thesis: verum

end;

assume x in [:A,B:] ; :: thesis: x in union G
then consider y, z being 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 x in union G by A15, A16, TARSKI:def 4; :: thesis: verum

end;

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

proof

let x be set ; :: thesis: ( x in rng g iff x in G )
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 set 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 x in G by A10, A18, A19, A21; :: thesis: verum

end;

assume x in G ; :: thesis: x in rng g
then consider y being set such that
A22: y in B and
A23: x = [:A,{y}:] by A10;
x = g . y by A18, A22, A23;
hence x in rng g by A18, A22, FUNCT_1:def 5; :: thesis: verum

end;

then rng g = G by TARSKI:2;
then B24: g .: B = G by A18, RELAT_1:146;
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 A10;
hence X is finite by A3; :: thesis: verum

end;

hence [:A,B:] is finite by A17, B24, Lm3; :: thesis: verum