let V be Universe; :: thesis: for a, y being Element of V
for X being Subclass of V
for fs being finite Subset of omega
for n being Element of omega st X is closed_wrt_A1-A7 & a in X & a c= X & y in Funcs (fs,a) holds
{ ({[n,x]} \/ y) where x is Element of V : x in a } in X
let a, y be Element of V; :: thesis: for X being Subclass of V
for fs being finite Subset of omega
for n being Element of omega st X is closed_wrt_A1-A7 & a in X & a c= X & y in Funcs (fs,a) holds
{ ({[n,x]} \/ y) where x is Element of V : x in a } in X
let X be Subclass of V; :: thesis: for fs being finite Subset of omega
for n being Element of omega st X is closed_wrt_A1-A7 & a in X & a c= X & y in Funcs (fs,a) holds
{ ({[n,x]} \/ y) where x is Element of V : x in a } in X
let fs be finite Subset of omega; :: thesis: for n being Element of omega st X is closed_wrt_A1-A7 & a in X & a c= X & y in Funcs (fs,a) holds
{ ({[n,x]} \/ y) where x is Element of V : x in a } in X
let n be Element of omega ; :: thesis: ( X is closed_wrt_A1-A7 & a in X & a c= X & y in Funcs (fs,a) implies { ({[n,x]} \/ y) where x is Element of V : x in a } in X )
assume that
A1: X is closed_wrt_A1-A7 and
A2: a in X and
A3: ( a c= X & y in Funcs (fs,a) ) ; :: thesis: { ({[n,x]} \/ y) where x is Element of V : x in a } in X
set Z = { ({[n,x]} \/ y) where x is Element of V : x in a } ;
set s = {y};
set Y = { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } ;
A4: { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } = { ({[n,x]} \/ y) where x is Element of V : x in a }
proof
thus { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } c= { ({[n,x]} \/ y) where x is Element of V : x in a } :: according to XBOOLE_0:def 10 :: thesis: { ({[n,x]} \/ y) where x is Element of V : x in a } c= { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) }
proof
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } or p in { ({[n,x]} \/ y) where x is Element of V : x in a } )
assume p in { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } ; :: thesis: p in { ({[n,x]} \/ y) where x is Element of V : x in a }
then consider x, z being Element of V such that
A5: ( p = {[n,x]} \/ z & x in a ) and
A6: z in {y} ;
z = y by A6, TARSKI:def 1;
hence p in { ({[n,x]} \/ y) where x is Element of V : x in a } by A5; :: thesis: verum
end;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in { ({[n,x]} \/ y) where x is Element of V : x in a } or p in { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } )
assume p in { ({[n,x]} \/ y) where x is Element of V : x in a } ; :: thesis: p in { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) }
then A7: ex x being Element of V st
( p = {[n,x]} \/ y & x in a ) ;
y in {y} by TARSKI:def 1;
hence p in { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } by A7; :: thesis: verum
end;
y in X by A1, A3, Th14;
then {y} in X by A1, Th2;
hence { ({[n,x]} \/ y) where x is Element of V : x in a } in X by A1, A2, A4, Th12; :: thesis: verum