let V be Universe; :: thesis: for a, y, b 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, y, b be Element of V; :: thesis: 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; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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 A1: ( 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 ) ; :: thesis: { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X
then A2: X is closed_wrt_A6 by Def13;
A3: for x being Element of V st {[n,x]} \/ y in b holds
x in a

proof

let x be Element of V; :: thesis: ( {[n,x]} \/ y in b implies x in a )
assume {[n,x]} \/ y in b ; :: thesis: x in a
then consider g being Function such that
A4: ( {[n,x]} \/ y = g & dom g = fs \/ {n} & rng g c= a ) by A1, FUNCT_2:def 2;
A5: {[n,x]} c= g by A4, XBOOLE_1:7;
[n,x] in {[n,x]} by TARSKI:def 1;
then ( n in dom g & x = g . n ) by A5, FUNCT_1:8;
then x in rng g by FUNCT_1:def 5;
hence x in a by A4; :: thesis: verum

end;

set T = { ({[n,x]} \/ y) where x is Element of V : x in a } ;
A6: { ({[n,x]} \/ y) where x is Element of V : x in a } in X by A1, Th15;
set T' = { ({[n,x]} \/ y) where x is Element of V : x in a } /\ b;
A7: { ({[n,x]} \/ y) where x is Element of V : x in a } /\ b in X by A1, A6, Th5;
then reconsider t' = { ({[n,x]} \/ y) where x is Element of V : x in a } /\ b as Element of V ;
y in X by A1, Th14;
then A8: {y} in X by A1, Th2;
set s = {y};
set R = { (x \ z) where x, z is Element of V : ( x in t' & z in {y} ) } ;
A9: { (x \ z) where x, z is Element of V : ( x in t' & z in {y} ) } in X by A2, A7, A8, Def11;
set S = { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ;
{ (x \ z) where x, z is Element of V : ( x in t' & 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 t' & z in {y} ) } c= { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } :: according to XBOOLE_0:def 10 :: thesis: { {[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 t' & z in {y} ) }

proof

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in { (x \ z) where x, z is Element of V : ( x in t' & 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 t' & z in {y} ) } ; :: thesis: 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
A10: ( p = x \ z & x in t' & z in {y} ) ;
A11: z = y by A10, TARSKI:def 1;
A12: ( x in { ({[n,x]} \/ y) where x is Element of V : x in a } & x in b ) by A10, XBOOLE_0:def 4;
then consider x' being Element of V such that
A13: ( x = {[n,x']} \/ y & x' in a ) ;
A14: {[n,x']} misses y

proof

assume not {[n,x']} misses y ; :: thesis: contradiction
then consider r being set such that
A15: ( r in {[n,x']} & r in y ) by XBOOLE_0:3;
consider g being Function such that
A16: ( y = g & dom g = fs & rng g c= a ) by A1, FUNCT_2:def 2;
r = [n,x'] by A15, TARSKI:def 1;
hence contradiction by A1, A15, A16, FUNCT_1:8; :: thesis: verum

end;

x \ z = ({[n,x']} \ y) \/ (y \ y) by A11, A13, XBOOLE_1:42
.= {[n,x']} \/ (y \ y) by A14, XBOOLE_1:83
.= {[n,x']} \/ {} by XBOOLE_1:37
.= {[n,x']} ;
hence p in { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } by A10, A12, A13; :: thesis: verum

end;

let p be set ; :: according to TARSKI:def 3 :: thesis: ( 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 t' & z in {y} ) } )
assume p in { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ; :: thesis: p in { (x \ z) where x, z is Element of V : ( x in t' & z in {y} ) }
then consider x being Element of V such that
A17: ( p = {[n,x]} & {[n,x]} \/ y in b ) ;
A18: {[n,x]} misses y

proof

assume not {[n,x]} misses y ; :: thesis: contradiction
then consider r being set such that
A19: ( r in {[n,x]} & r in y ) by XBOOLE_0:3;
consider g being Function such that
A20: ( y = g & dom g = fs & rng g c= a ) by A1, FUNCT_2:def 2;
r = [n,x] by A19, TARSKI:def 1;
hence contradiction by A1, A19, A20, FUNCT_1:8; :: thesis: verum

end;

reconsider x' = {[n,x]} \/ y as Element of V by A1, A17, Th1;
A21: y in {y} by TARSKI:def 1;
x in a by A3, A17;
then x' in { ({[n,x]} \/ y) where x is Element of V : x in a } ;
then A22: x' in t' by A17, XBOOLE_0:def 4;
x' \ y = ({[n,x]} \ y) \/ (y \ y) by XBOOLE_1:42
.= {[n,x]} \/ (y \ y) by A18, 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 t' & z in {y} ) } by A17, A21, A22; :: thesis: verum

end;

then union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } in X by A1, A9, Th2;
then union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ) in X by A1, Th2;
then A23: 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 ) } ;
A24: { 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 set ; :: according to TARSKI:def 3 :: thesis: ( 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 ) } ; :: thesis: 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
A25: ( p = x & x in a & {[n,x]} \/ y in b ) ;
A26: {[n,x]} in { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } by A25;
[n,x] in {[n,x]} by TARSKI:def 1;
then A27: {{n,x},{n}} in union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } by A26, TARSKI:def 4;
{n,x} in {{n,x},{n}} by TARSKI:def 2;
then A28: {n,x} in union (union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ) by A27, 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 A25, A28, TARSKI:def 4; :: thesis: verum

end;

A29: 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 set ; :: according to TARSKI:def 3 :: thesis: ( 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 } )) ; :: thesis: 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
A30: ( p in C & 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
A31: ( C in D & D in union { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ) by A30, TARSKI:def 4;
consider E being set such that
A32: ( D in E & E in { {[n,x]} where x is Element of V : {[n,x]} \/ y in b } ) by A31, TARSKI:def 4;
consider x being Element of V such that
A33: ( E = {[n,x]} & {[n,x]} \/ y in b ) by A32;
A34: x in a by A3, A33;
D = [n,x] by A32, A33, TARSKI:def 1;
then ( p in {n,x} or p in {n} ) by A30, A31, TARSKI:def 2;
then ( p = n or p = x or p in {n} ) by TARSKI:def 2;
then ( p in { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } or p in {n} ) by A33, A34, 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; :: thesis: 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 n in { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } ; :: thesis: { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X

then {n} c= { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } by ZFMISC_1:37;
then { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } \/ {n} = { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } by XBOOLE_1:12;
hence { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X by A23, A24, A29, XBOOLE_0:def 10; :: thesis: verum

end;

suppose not n in { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } ; :: thesis: { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X

then A35: { x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } misses {n} by ZFMISC_1:56;
{ 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 A24, XBOOLE_1:33;
then A36: { 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 A35, XBOOLE_1:83;
(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 A29, 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 A35, XBOOLE_1:83;
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 ) } \/ {} by XBOOLE_1:37;
then A37: (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 A36, XBOOLE_0:def 10;
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, A23, A37, Th4; :: thesis: verum

end;

end;