let V be Universe; :: thesis: for a, b being Element of V
for X being Subclass of V
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in Funcs (fs,omega) & b in X holds
{ (a (#) x) where x is Element of V : x in b } in X
let a, b be Element of V; :: thesis: for X being Subclass of V
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in Funcs (fs,omega) & b in X holds
{ (a (#) x) where x is Element of V : x in b } in X
let X be Subclass of V; :: thesis: for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in Funcs (fs,omega) & b in X holds
{ (a (#) x) where x is Element of V : x in b } in X
let fs be finite Subset of omega; :: thesis: ( X is closed_wrt_A1-A7 & a in Funcs (fs,omega) & b in X implies { (a (#) x) where x is Element of V : x in b } in X )
assume that
A1: X is closed_wrt_A1-A7 and
A2: a in Funcs (fs,omega) and
A3: b in X ; :: thesis: { (a (#) x) where x is Element of V : x in b } in X
Funcs (fs,omega) c= X by A1, Th8;
then A4: {a} in X by A1, A2, Th2;
set A = { (a (#) x) where x is Element of V : x in b } ;
set s = {a};
set B = { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } ;
A5: { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } c= { (a (#) x) where x is Element of V : x in b }
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } or q in { (a (#) x) where x is Element of V : x in b } )
assume q in { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } ; :: thesis: q in { (a (#) x) where x is Element of V : x in b }
then consider y, x being Element of V such that
A6: ( q = y (#) x & y in {a} ) and
A7: x in b ;
q = a (#) x by A6, TARSKI:def 1;
hence q in { (a (#) x) where x is Element of V : x in b } by A7; :: thesis: verum
end;
{ (a (#) x) where x is Element of V : x in b } c= { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) }
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { (a (#) x) where x is Element of V : x in b } or q in { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } )
assume q in { (a (#) x) where x is Element of V : x in b } ; :: thesis: q in { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) }
then A8: ex x being Element of V st
( q = a (#) x & x in b ) ;
a in {a} by TARSKI:def 1;
hence q in { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } by A8; :: thesis: verum
end;
then A9: { (a (#) x) where x is Element of V : x in b } = { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } by A5;
X is closed_wrt_A7 by A1;
hence { (a (#) x) where x is Element of V : x in b } in X by A3, A4, A9; :: thesis: verum