let V be Universe; for a, b being Element of V
for X being Subclass of V
for n being Element of omega st X is closed_wrt_A1-A7 & a in X & b in X holds
{ ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } in X
let a, b be Element of V; for X being Subclass of V
for n being Element of omega st X is closed_wrt_A1-A7 & a in X & b in X holds
{ ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } in X
let X be Subclass of V; for n being Element of omega st X is closed_wrt_A1-A7 & a in X & b in X holds
{ ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } in X
let n be Element of omega ; ( X is closed_wrt_A1-A7 & a in X & b in X implies { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } in X )
assume that
A1:
X is closed_wrt_A1-A7
and
A2:
a in X
and
A3:
b in X
; { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } in X
A4:
Funcs ({n},a) in X
by A1, A2, Th9;
then reconsider F = Funcs ({n},a) as Element of V ;
set Z = { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } ;
set Y = { (x \/ y) where x, y is Element of V : ( x in F & y in b ) } ;
A5:
{ (x \/ y) where x, y is Element of V : ( x in F & y in b ) } = { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) }
proof
thus
{ (x \/ y) where x, y is Element of V : ( x in F & y in b ) } c= { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) }
XBOOLE_0:def 10 { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } c= { (x \/ y) where x, y is Element of V : ( x in F & y in b ) } proof
let p be
object ;
TARSKI:def 3 ( not p in { (x \/ y) where x, y is Element of V : ( x in F & y in b ) } or p in { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } )
assume
p in { (x \/ y) where x, y is Element of V : ( x in F & y in b ) }
;
p in { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) }
then consider x,
y being
Element of
V such that A6:
p = x \/ y
and A7:
x in F
and A8:
y in b
;
consider g being
Function such that A9:
x = g
and A10:
dom g = {n}
and A11:
rng g c= a
by A7, FUNCT_2:def 2;
n in dom g
by A10, TARSKI:def 1;
then A12:
g . n in rng g
by FUNCT_1:def 3;
then reconsider z =
g . n as
Element of
V by A2, A11, Th1;
p = {[n,z]} \/ y
by A6, A9, A10, GRFUNC_1:7;
hence
p in { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) }
by A8, A11, A12;
verum
end;
let p be
object ;
TARSKI:def 3 ( not p in { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } or p in { (x \/ y) where x, y is Element of V : ( x in F & y in b ) } )
assume
p in { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) }
;
p in { (x \/ y) where x, y is Element of V : ( x in F & y in b ) }
then consider x,
y being
Element of
V such that A13:
p = {[n,x]} \/ y
and A14:
x in a
and A15:
y in b
;
reconsider g =
{[n,x]} as
Function ;
rng g = {x}
by RELAT_1:9;
then
(
dom g = {n} &
rng g c= a )
by A14, RELAT_1:9, ZFMISC_1:31;
then A16:
{[n,x]} in F
by FUNCT_2:def 2;
then reconsider z =
{[n,x]} as
Element of
V by A4, Th1;
p = z \/ y
by A13;
hence
p in { (x \/ y) where x, y is Element of V : ( x in F & y in b ) }
by A15, A16;
verum
end;
X is closed_wrt_A5
by A1;
hence
{ ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } in X
by A3, A4, A5; verum