let V be Universe; :: thesis: 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; :: 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 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 ; :: thesis: { 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
proof
let x be Element of V; :: thesis: ( {[n,x]} \/ y in b implies x in a )
A11: [n,x] in {[n,x]} by TARSKI:def 1;
assume {[n,x]} \/ y in b ; :: thesis: x in a
then consider g being Function such that
A12: {[n,x]} \/ y = g and
dom g = fs \/ {n} and
A13: rng g c= a by A6, FUNCT_2:def 2;
{[n,x]} c= g by A12, XBOOLE_1:7;
then ( n in dom g & x = g . n ) by A11, FUNCT_1:1;
then x in rng g by FUNCT_1:def 3;
hence x in a by A13; :: thesis: verum
end;
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 } :: 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 t9 & z in {y} ) }
proof
let p be object ; :: according to TARSKI:def 3 :: thesis: ( 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} ) } ; :: 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
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
proof
assume not {[n,x9]} misses y ; :: thesis: contradiction
then consider r being object such that
A21: r in {[n,x9]} and
A22: r in y by XBOOLE_0:3;
A23: ex g being Function st
( y = g & dom g = fs & rng g c= a ) by A5, FUNCT_2:def 2;
r = [n,x9] by A21, TARSKI:def 1;
hence contradiction by A2, A22, A23, FUNCT_1:1; :: thesis: verum
end;
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; :: thesis: verum
end;
let p be object ; :: 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 t9 & 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 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
proof
assume not {[n,x]} misses y ; :: thesis: contradiction
then consider r being object such that
A28: r in {[n,x]} and
A29: r in y by XBOOLE_0:3;
A30: ex g being Function st
( y = g & dom g = fs & rng g c= a ) by A5, FUNCT_2:def 2;
r = [n,x] by A28, TARSKI:def 1;
hence contradiction by A2, A29, A30, FUNCT_1:1; :: thesis: verum
end;
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; :: thesis: 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 ; :: 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
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; :: thesis: 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 ; :: 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
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; :: 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:31;
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 A31, A32, A38, 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 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; :: thesis: verum
end;
end;