let V be Universe; 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; 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; ( X is closed_wrt_A1-A7 implies Funcs (fs,omega) c= X )
defpred S1[ set ] means Funcs ($1,omega) c= X;
assume A1:
X is closed_wrt_A1-A7
; Funcs (fs,omega) c= X
then
( Funcs ({},omega) = {{}} & {} in X )
by Th3, FUNCT_5:57;
then A2:
S1[ {} ]
by ZFMISC_1:31;
A3:
omega c= X
by A1, Th7;
A4:
for o, B being set st o in fs & B c= fs & S1[B] holds
S1[B \/ {o}]
proof
let o,
B be
set ;
( o in fs & B c= fs & S1[B] implies S1[B \/ {o}] )
assume that A5:
o in fs
and
B c= fs
and A6:
Funcs (
B,
omega)
c= X
;
S1[B \/ {o}]
now for p being object st p in Funcs ((B \/ {o}),omega) holds
p in Xlet p be
object ;
( p in Funcs ((B \/ {o}),omega) implies p in X )assume
p in Funcs (
(B \/ {o}),
omega)
;
p in Xthen 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;
verum end;
hence
S1[
B \/ {o}]
by TARSKI:def 3;
verum
end;
A17:
fs is finite
;
thus
S1[fs]
from FINSET_1:sch 2(A17, A2, A4); verum