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 ( Funcs ({},omega) = {{}} & {} in X ) by Th3, FUNCT_5:57;
then A2: S₁[ {} ] by ZFMISC_1:31;
A3: omega c= X by A1, Th7;
A4: 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 that
A5: o in fs and
B c= fs and
A6: Funcs (B,omega) c= X ; :: thesis: S₁[B \/ {o}]

now :: thesis: for p being object st p in Funcs ((B \/ {o}),omega) holds
p in X

let p be object ; :: thesis: ( p in Funcs ((B \/ {o}),omega) implies p in X )
assume p in Funcs ((B \/ {o}),omega) ; :: thesis: p in X
then consider g being Function such that
A7: p = g and
A8: dom g = B \/ {o} and
A9: rng g c= omega by FUNCT_2:def 2;
set A = g | B;
rng (g | B) c= rng g by RELAT_1:70;
then A10: rng (g | B) c= omega by A9;
set C = g | {o};
A11: dom (g | {o}) = (B \/ {o}) /\ {o} by A8, RELAT_1:61
.= {o} by XBOOLE_1:21 ;
then A12: g | {o} = {[o,((g | {o}) . o)]} by GRFUNC_1:7;
o in dom (g | {o}) by A11, TARSKI:def 1;
then A13: (g | {o}) . o in rng (g | {o}) by FUNCT_1:def 3;
rng (g | {o}) c= rng g by RELAT_1:70;
then rng (g | {o}) c= omega by A9;
then A14: (g | {o}) . o in omega by A13;
o in omega by A5;
then [o,((g | {o}) . o)] in X by A1, A3, A14, Th6;
then A15: g | {o} in X by A1, A12, Th2;
dom (g | B) = (B \/ {o}) /\ B by A8, RELAT_1:61
.= B by XBOOLE_1:21 ;
then A16: g | B in Funcs (B,omega) by A10, FUNCT_2:def 2;
g = g | (B \/ {o}) by A8
.= (g | B) \/ (g | {o}) by RELAT_1:78 ;
hence p in X by A1, A6, A7, A16, A15, Th4; :: thesis: verum

end;

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

end;

A17: fs is finite ;
thus S₁[fs] from FINSET_1:sch 2(A17, A2, A4); :: thesis: verum