let V be Universe; for y being Element of V
for X being Subclass of V
for A being set
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & A c= X & y in Funcs (fs,A) holds
y in X
let y be Element of V; for X being Subclass of V
for A being set
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & A c= X & y in Funcs (fs,A) holds
y in X
let X be Subclass of V; for A being set
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & A c= X & y in Funcs (fs,A) holds
y in X
let A be set ; for fs being finite Subset of omega st X is closed_wrt_A1-A7 & A c= X & y in Funcs (fs,A) holds
y in X
let fs be finite Subset of omega; ( X is closed_wrt_A1-A7 & A c= X & y in Funcs (fs,A) implies y in X )
assume that
A1:
X is closed_wrt_A1-A7
and
A2:
A c= X
and
A3:
y in Funcs (fs,A)
; y in X
consider g being Function such that
A4:
y = g
and
A5:
dom g = fs
and
A6:
rng g c= A
by A3, FUNCT_2:def 2;
A7:
now for o being set st o in y holds
o in Xlet o be
set ;
( o in y implies o in X )assume A8:
o in y
;
o in Xthen consider p,
q being
object such that A9:
o = [p,q]
by A4, RELAT_1:def 1;
A10:
p in dom g
by A4, A8, A9, FUNCT_1:1;
q = g . p
by A4, A8, A9, FUNCT_1:1;
then
q in rng g
by A10, FUNCT_1:def 3;
then A11:
q in A
by A6;
A12:
omega c= X
by A1, Th7;
p in omega
by A5, A10;
hence
o in X
by A1, A2, A9, A12, A11, Th6;
verum end;
rng g is finite
by A5, FINSET_1:8;
then
[:(dom g),(rng g):] is finite
by A5;
then
y is finite
by A4, FINSET_1:1, RELAT_1:7;
hence
y in X
by A1, A7, Th13; verum