let V be Universe; for a, b, y being Element of V
for X being Subclass of V
for n being Element of omega
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & not n in fs & a in X & a c= X & y in Funcs (fs,a) & b c= Funcs ((fs \/ {n}),a) & b in X holds
{ x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X
let a, b, y be Element of V; for X being Subclass of V
for n being Element of omega
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & not n in fs & a in X & a c= X & y in Funcs (fs,a) & b c= Funcs ((fs \/ {n}),a) & b in X holds
{ x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X
let X be Subclass of V; for n being Element of omega
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & not n in fs & a in X & a c= X & y in Funcs (fs,a) & b c= Funcs ((fs \/ {n}),a) & b in X holds
{ x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X
let n be Element of omega ; for fs being finite Subset of omega st X is closed_wrt_A1-A7 & not n in fs & a in X & a c= X & y in Funcs (fs,a) & b c= Funcs ((fs \/ {n}),a) & b in X holds
{ x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X
let fs be finite Subset of omega; ( X is closed_wrt_A1-A7 & not n in fs & a in X & a c= X & y in Funcs (fs,a) & b c= Funcs ((fs \/ {n}),a) & b in X implies { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X )
assume that
A1:
X is closed_wrt_A1-A7
and
A2:
not n in fs
and
A3:
a in X
and
A4:
a c= X
and
A5:
y in Funcs (fs,a)
and
A6:
b c= Funcs ((fs \/ {n}),a)
and
A7:
b in X
; { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X
y in X
by A1, A4, A5, Th14;
then A8:
{y} in X
by A1, Th2;
set T = { ({[n,x]} \/ y) where x is Element of V : x in a } ;
set T9 = { ({[n,x]} \/ y) where x is Element of V : x in a } /\ b;
{ ({[n,x]} \/ y) where x is Element of V : x in a } in X
by A1, A3, A4, A5, Th15;
then A9:
{ ({[n,x]} \/ y) where x is Element of V : x in a } /\ b in X
by A1, A7, Th5;
then reconsider t9 = { ({[n,x]} \/ y) where x is Element of V : x in a } /\ b as Element of V ;
set S = { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ;
set s = {y};
set R = { (x \ z) where x, z is Element of V : ( x in t9 & z in {y} ) } ;
A10:
for x being Element of V st {[n,x]} \/ y in b holds
x in a
A14:
{ (x \ z) where x, z is Element of V : ( x in t9 & z in {y} ) } = { {[n,x]} where x is Element of V : {[n,x]} \/ y in b }
proof
thus
{ (x \ z) where x, z is Element of V : ( x in t9 & z in {y} ) } c= { {[n,x]} where x is Element of V : {[n,x]} \/ y in b }
XBOOLE_0:def 10 { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } c= { (x \ z) where x, z is Element of V : ( x in t9 & z in {y} ) } proof
let p be
object ;
TARSKI:def 3 ( not p in { (x \ z) where x, z is Element of V : ( x in t9 & z in {y} ) } or p in { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } )
assume
p in { (x \ z) where x, z is Element of V : ( x in t9 & z in {y} ) }
;
p in { {[n,x]} where x is Element of V : {[n,x]} \/ y in b }
then consider x,
z being
Element of
V such that A15:
p = x \ z
and A16:
x in t9
and A17:
z in {y}
;
A18:
x in b
by A16, XBOOLE_0:def 4;
x in { ({[n,x]} \/ y) where x is Element of V : x in a }
by A16, XBOOLE_0:def 4;
then consider x9 being
Element of
V such that A19:
x = {[n,x9]} \/ y
and
x9 in a
;
A20:
{[n,x9]} misses y
z = y
by A17, TARSKI:def 1;
then x \ z =
({[n,x9]} \ y) \/ (y \ y)
by A19, XBOOLE_1:42
.=
{[n,x9]} \/ (y \ y)
by A20, XBOOLE_1:83
.=
{[n,x9]} \/ {}
by XBOOLE_1:37
.=
{[n,x9]}
;
hence
p in { {[n,x]} where x is Element of V : {[n,x]} \/ y in b }
by A15, A18, A19;
verum
end;
let p be
object ;
TARSKI:def 3 ( not p in { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } or p in { (x \ z) where x, z is Element of V : ( x in t9 & z in {y} ) } )
assume
p in { {[n,x]} where x is Element of V : {[n,x]} \/ y in b }
;
p in { (x \ z) where x, z is Element of V : ( x in t9 & z in {y} ) }
then consider x being
Element of
V such that A24:
p = {[n,x]}
and A25:
{[n,x]} \/ y in b
;
reconsider x9 =
{[n,x]} \/ y as
Element of
V by A7, A25, Th1;
x in a
by A10, A25;
then
x9 in { ({[n,x]} \/ y) where x is Element of V : x in a }
;
then A26:
(
y in {y} &
x9 in t9 )
by A25, TARSKI:def 1, XBOOLE_0:def 4;
A27:
{[n,x]} misses y
x9 \ y =
({[n,x]} \ y) \/ (y \ y)
by XBOOLE_1:42
.=
{[n,x]} \/ (y \ y)
by A27, XBOOLE_1:83
.=
{[n,x]} \/ {}
by XBOOLE_1:37
.=
{[n,x]}
;
hence
p in { (x \ z) where x, z is Element of V : ( x in t9 & z in {y} ) }
by A24, A26;
verum
end;
X is closed_wrt_A6
by A1;
then
{ (x \ z) where x, z is Element of V : ( x in t9 & z in {y} ) } in X
by A9, A8;
then
union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } in X
by A1, A14, Th2;
then
union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ) in X
by A1, Th2;
then A31:
union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } )) in X
by A1, Th2;
set Z = { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } ;
A32:
{ x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } c= union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ))
proof
let p be
object ;
TARSKI:def 3 ( not p in { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } or p in union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } )) )
assume
p in { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) }
;
p in union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ))
then consider x being
Element of
V such that A33:
p = x
and
x in a
and A34:
{[n,x]} \/ y in b
;
A35:
[n,x] in {[n,x]}
by TARSKI:def 1;
A36:
{n,x} in {{n,x},{n}}
by TARSKI:def 2;
{[n,x]} in { {[n,x]} where x is Element of V : {[n,x]} \/ y in b }
by A34;
then
{{n,x},{n}} in union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b }
by A35, TARSKI:def 4;
then A37:
{n,x} in union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } )
by A36, TARSKI:def 4;
x in {n,x}
by TARSKI:def 2;
hence
p in union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ))
by A33, A37, TARSKI:def 4;
verum
end;
A38:
union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } )) c= { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } \/ {n}
proof
let p be
object ;
TARSKI:def 3 ( not p in union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } )) or p in { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } \/ {n} )
assume
p in union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ))
;
p in { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } \/ {n}
then consider C being
set such that A39:
p in C
and A40:
C in union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } )
by TARSKI:def 4;
consider D being
set such that A41:
C in D
and A42:
D in union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b }
by A40, TARSKI:def 4;
consider E being
set such that A43:
D in E
and A44:
E in { {[n,x]} where x is Element of V : {[n,x]} \/ y in b }
by A42, TARSKI:def 4;
consider x being
Element of
V such that A45:
E = {[n,x]}
and A46:
{[n,x]} \/ y in b
by A44;
D = [n,x]
by A43, A45, TARSKI:def 1;
then
(
p in {n,x} or
p in {n} )
by A39, A41, TARSKI:def 2;
then A47:
(
p = n or
p = x or
p in {n} )
by TARSKI:def 2;
x in a
by A10, A46;
then
(
p in { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } or
p in {n} )
by A46, A47, TARSKI:def 1;
hence
p in { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } \/ {n}
by XBOOLE_0:def 3;
verum
end;
per cases
( n in { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } or not n in { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } )
;
suppose
not
n in { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) }
;
{ x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in Xthen A48:
{ x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } misses {n}
by ZFMISC_1:50;
(union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ))) \ {n} c= ( { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } \/ {n}) \ {n}
by A38, XBOOLE_1:33;
then
(union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ))) \ {n} c= ( { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } \ {n}) \/ ({n} \ {n})
by XBOOLE_1:42;
then
(union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ))) \ {n} c= { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } \/ ({n} \ {n})
by A48, XBOOLE_1:83;
then A49:
(union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ))) \ {n} c= { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } \/ {}
by XBOOLE_1:37;
{ x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } \ {n} c= (union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ))) \ {n}
by A32, XBOOLE_1:33;
then
{ x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } c= (union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ))) \ {n}
by A48, XBOOLE_1:83;
then A50:
(union (union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ))) \ {n} = { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) }
by A49;
n in X
by A1, Lm12;
then
{n} in X
by A1, Th2;
hence
{ x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X
by A1, A31, A50, Th4;
verum end; end;