let V be Universe; :: thesis: for X being Subclass of V
for fs being finite Subset of omega st X is closed_wrt_A1-A7 holds
Funcs fs,omega c= X
let X be Subclass of V; :: thesis: for fs being finite Subset of omega st X is closed_wrt_A1-A7 holds
Funcs fs,omega c= X
let fs be finite Subset of omega ; :: thesis: ( X is closed_wrt_A1-A7 implies Funcs fs,omega c= X )
defpred S₁[ set ] means Funcs $1,omega c= X;
assume A1: X is closed_wrt_A1-A7 ; :: thesis: Funcs fs,omega c= X
then A2: omega c= X by Th7;
A3: fs is finite ;
A4: S₁[ {} ]

proof

A5: Funcs {} ,omega = {{} } by FUNCT_5:64;
{} in X by A1, Th3;
hence S₁[ {} ] by A5, ZFMISC_1:37; :: thesis: verum

end;

A6: for o, B being set st o in fs & B c= fs & S₁[B] holds
S₁[B \/ {o}]

proof

let o, B be set ; :: thesis: ( o in fs & B c= fs & S₁[B] implies S₁[B \/ {o}] )
assume A7: ( o in fs & B c= fs & Funcs B,omega c= X ) ; :: thesis: S₁[B \/ {o}]

now

let p be set ; :: thesis: ( p in Funcs (B \/ {o}),omega implies p in X )
assume A8: p in Funcs (B \/ {o}),omega ; :: thesis: p in X
A9: o in omega by A7;
consider g being Function such that
A10: ( p = g & dom g = B \/ {o} & rng g c= omega ) by A8, FUNCT_2:def 2;
set A = g | B;
set C = g | {o};
A11: g | B in X

proof

A12: dom (g | B) = (B \/ {o}) /\ B by A10, RELAT_1:90
.= B by XBOOLE_1:21 ;
rng (g | B) c= rng g by RELAT_1:99;
then rng (g | B) c= omega by A10, XBOOLE_1:1;
then g | B in Funcs B,omega by A12, FUNCT_2:def 2;
hence g | B in X by A7; :: thesis: verum

end;

A13: g | {o} in X

proof

A14: dom (g | {o}) = (B \/ {o}) /\ {o} by A10, RELAT_1:90
.= {o} by XBOOLE_1:21 ;
then A15: g | {o} = {[o,((g | {o}) . o)]} by GRFUNC_1:18;
rng (g | {o}) c= rng g by RELAT_1:99;
then A16: rng (g | {o}) c= omega by A10, XBOOLE_1:1;
o in dom (g | {o}) by A14, TARSKI:def 1;
then (g | {o}) . o in rng (g | {o}) by FUNCT_1:def 5;
then (g | {o}) . o in omega by A16;
then [o,((g | {o}) . o)] in X by A1, A2, A9, Th6;
hence g | {o} in X by A1, A15, Th2; :: thesis: verum

end;

g = g | (B \/ {o}) by A10, RELAT_1:97
.= (g | B) \/ (g | {o}) by RELAT_1:107 ;
hence p in X by A1, A10, A11, A13, Th4; :: thesis: verum

end;

hence S₁[B \/ {o}] by TARSKI:def 3; :: thesis: verum

end;

thus S₁[fs] from FINSET_1:sch 2(A3, A4, A6); :: thesis: verum