Copyright (c) 1989 Association of Mizar Users
environ
vocabulary SUBSET_1, MCART_1, BOOLE;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, MCART_1;
constructors TARSKI, ENUMSET1, MCART_1, XBOOLE_0;
clusters SUBSET_1, XBOOLE_0, ZFMISC_1;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, SUBSET_1, MCART_1, ZFMISC_1, XBOOLE_0;
begin
reserve a,b,c,d for set;
reserve D,X1,X2,X3,X4 for non empty set;
reserve x1,y1,z1 for Element of X1,
x2 for Element of X2,
x3 for Element of X3,
x4 for Element of X4;
reserve A1,B1 for Subset of X1;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::
:: Domains and their elements
::
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
canceled 8;
theorem
a in [:X1,X2:] implies ex x1,x2 st a=[x1,x2]
proof assume a in [:X1,X2:];
then consider x1,x2 being set such that
A1: x1 in X1 and
A2: x2 in X2 and
A3: a=[x1,x2] by ZFMISC_1:def 2;
reconsider x1 as Element of X1 by A1;
reconsider x2 as Element of X2 by A2;
take x1,x2;
thus thesis by A3;
end;
canceled 2;
theorem
for x,y being Element of [:X1,X2:] st x`1=y`1 & x`2=y`2 holds x=y
proof let x,y be Element of [:X1,X2:];
[x`1,x`2]=x & [y`1,y`2]=y by MCART_1:23;
hence thesis;
end;
definition let X1,X2,x1,x2;
redefine func [x1,x2] -> Element of [:X1,X2:];
coherence by ZFMISC_1:106;
end;
definition let X1,X2; let x be Element of [:X1,X2:];
redefine func x`1 -> Element of X1;
coherence by MCART_1:10;
redefine func x`2 -> Element of X2;
coherence by MCART_1:10;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::
:: Cartesian products of three sets
::
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
canceled 2;
theorem Th15:
a in [: X1,X2,X3 :] iff ex x1,x2,x3 st a = [x1,x2,x3]
proof
thus a in [: X1,X2,X3 :] implies ex x1,x2,x3 st a = [x1,x2,x3]
proof assume a in [: X1,X2,X3 :];
then a in [:[:X1,X2:],X3:] by ZFMISC_1:def 3;
then consider x12, x3 being set such that
A1: x12 in [:X1,X2:] and
A2: x3 in X3 and
A3: a = [x12,x3] by ZFMISC_1:def 2;
consider x1,x2 being set such that
A4: x1 in X1 and
A5: x2 in X2 and
A6: x12 = [x1,x2] by A1,ZFMISC_1:def 2;
reconsider x1 as Element of X1 by A4;
reconsider x2 as Element of X2 by A5;
reconsider x3 as Element of X3 by A2;
a = [x1,x2,x3] by A3,A6,MCART_1:def 3;
hence ex x1,x2,x3 st a = [x1,x2,x3];
end;
given x1,x2,x3 such that
A7: a = [x1,x2,x3];
a = [[x1,x2],x3] by A7,MCART_1:def 3;
then a in [:[:X1,X2:],X3:];
hence a in [: X1,X2,X3 :] by ZFMISC_1:def 3;
end;
theorem Th16:
(for a holds a in D iff ex x1,x2,x3 st a = [x1,x2,x3]) implies
D = [: X1,X2,X3 :]
proof
assume
A1: for a holds a in D iff ex x1,x2,x3 st a = [x1,x2,x3];
now let a;
thus a in D implies a in [:[:X1,X2:],X3:]
proof assume a in D; then consider x1,x2,x3 such that
A2: a = [x1,x2,x3] by A1;
a = [[x1,x2],x3] by A2,MCART_1:def 3;
hence a in [:[:X1,X2:],X3:];
end;
assume a in [:[:X1,X2:],X3:];
then consider x12,x3 being set such that
A3: x12 in [:X1,X2:] and
A4: x3 in X3 and
A5: a = [x12,x3] by ZFMISC_1:def 2;
consider x1,x2 being set such that
A6: x1 in X1 and
A7: x2 in X2 and
A8: x12 = [x1,x2] by A3,ZFMISC_1:def 2;
reconsider x1 as Element of X1 by A6;
reconsider x2 as Element of X2 by A7;
reconsider x3 as Element of X3 by A4;
a = [x1,x2,x3] by A5,A8,MCART_1:def 3;
hence a in D by A1;
end;
then D = [:[:X1,X2:],X3:] by TARSKI:2;
hence D = [: X1,X2,X3 :] by ZFMISC_1:def 3;
end;
theorem
D = [: X1,X2,X3 :] iff
for a holds a in D iff ex x1,x2,x3 st a = [x1,x2,x3] by Th15,Th16;
reserve x,y for Element of [:X1,X2,X3:];
definition let X1,X2,X3,x1,x2,x3;
redefine func [x1,x2,x3] -> Element of [:X1,X2,X3:];
coherence by MCART_1:73;
end;
canceled 6;
theorem
a =x`1 iff for x1,x2,x3 st x = [x1,x2,x3] holds a = x1
proof
thus a =x`1 implies for x1,x2,x3 st x = [x1,x2,x3] holds a = x1
proof assume
A1: a = x`1;
let x1,x2,x3 such that
A2: x = [x1,x2,x3];
x = [x`1,x`2,x`3] by MCART_1:48;
hence thesis by A1,A2,MCART_1:28;
end;
thus thesis by MCART_1:69;
end;
theorem
b =x`2 iff for x1,x2,x3 st x = [x1,x2,x3] holds b = x2
proof
thus b =x`2 implies for x1,x2,x3 st x = [x1,x2,x3] holds b = x2
proof assume
A1: b = x`2;
let x1,x2,x3 such that
A2: x = [x1,x2,x3];
x = [x`1,x`2,x`3] by MCART_1:48;
hence thesis by A1,A2,MCART_1:28;
end;
thus thesis by MCART_1:70;
end;
theorem
c =x`3 iff for x1,x2,x3 st x = [x1,x2,x3] holds c = x3
proof
thus c =x`3 implies for x1,x2,x3 st x = [x1,x2,x3] holds c = x3
proof assume
A1: c = x`3;
let x1,x2,x3 such that
A2: x = [x1,x2,x3];
x = [x`1,x`2,x`3] by MCART_1:48;
hence thesis by A1,A2,MCART_1:28;
end;
thus thesis by MCART_1:71;
end;
canceled;
theorem
x`1=y`1 & x`2=y`2 & x`3=y`3 implies x=y
proof [x`1,x`2,x`3]=x & [y`1,y`2,y`3]=y by MCART_1:48;
hence thesis;
end;
canceled 2;
theorem Th31:
a in [: X1,X2,X3,X4 :] iff ex x1,x2,x3,x4 st a = [x1,x2,x3,x4]
proof
thus a in [: X1,X2,X3,X4 :] implies ex x1,x2,x3,x4 st a = [x1,x2,x3,x4]
proof assume a in [: X1,X2,X3,X4 :];
then a in [:[:X1,X2,X3:],X4:] by ZFMISC_1:def 4;
then consider x123, x4 being set such that
A1: x123 in [:X1,X2,X3:] and
A2: x4 in X4 and
A3: a = [x123,x4] by ZFMISC_1:def 2;
consider x1 being (Element of X1),
x2 being (Element of X2),
x3 being Element of X3 such that
A4: x123 = [x1,x2,x3] by A1,Th15;
reconsider x4 as Element of X4 by A2;
a = [x1,x2,x3,x4] by A3,A4,MCART_1:def 4;
hence ex x1,x2,x3,x4 st a = [x1,x2,x3,x4];
end;
given x1,x2,x3,x4 such that
A5: a = [x1,x2,x3,x4];
a = [[x1,x2,x3],x4] by A5,MCART_1:def 4;
then a in [:[:X1,X2,X3:],X4:];
hence a in [: X1,X2,X3,X4 :] by ZFMISC_1:def 4;
end;
theorem Th32:
(for a holds a in D iff ex x1,x2,x3,x4 st a = [x1,x2,x3,x4]) implies
D = [: X1,X2,X3,X4 :]
proof
assume
A1: for a holds a in D iff ex x1,x2,x3,x4 st a = [x1,x2,x3,x4];
now let a;
thus a in D implies a in [:[:X1,X2,X3:],X4:]
proof assume a in D; then consider x1,x2,x3,x4 such that
A2: a = [x1,x2,x3,x4] by A1;
a = [[x1,x2,x3],x4] by A2,MCART_1:def 4;
hence a in [:[:X1,X2,X3:],X4:];
end;
assume a in [:[:X1,X2,X3:],X4:];
then consider x123,x4 being set such that
A3: x123 in [:X1,X2,X3:] and
A4: x4 in X4 and
A5: a = [x123,x4] by ZFMISC_1:def 2;
reconsider x4 as Element of X4 by A4;
consider x1,x2,x3 such that
A6: x123 = [x1,x2,x3] by A3,Th15;
a = [x1,x2,x3,x4] by A5,A6,MCART_1:def 4;
hence a in D by A1;
end;
then D = [:[:X1,X2,X3:],X4:] by TARSKI:2;
hence D = [: X1,X2,X3,X4 :] by ZFMISC_1:def 4;
end;
theorem
D = [: X1,X2,X3,X4 :] iff
for a holds a in D iff ex x1,x2,x3,x4 st a = [x1,x2,x3,x4] by Th31,Th32;
reserve x for Element of [:X1,X2,X3,X4:];
definition let X1,X2,X3,X4,x1,x2,x3,x4;
redefine func [x1,x2,x3,x4] -> Element of [:X1,X2,X3,X4:];
coherence by MCART_1:84;
end;
canceled 6;
theorem
a=x`1 iff for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds a = x1
proof
thus a =x`1 implies for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds a = x1
proof assume
A1: a = x`1;
let x1,x2,x3,x4 such that
A2: x = [x1,x2,x3,x4];
x = [x`1,x`2,x`3,x`4] by MCART_1:60;
hence thesis by A1,A2,MCART_1:33;
end;
thus thesis by MCART_1:79;
end;
theorem
b=x`2 iff for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds b = x2
proof
thus b =x`2 implies for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds b = x2
proof assume
A1: b = x`2;
let x1,x2,x3,x4 such that
A2: x = [x1,x2,x3,x4];
x = [x`1,x`2,x`3,x`4] by MCART_1:60;
hence thesis by A1,A2,MCART_1:33;
end;
thus thesis by MCART_1:80;
end;
theorem
c = x`3 iff for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds c = x3
proof
thus c =x`3 implies for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds c = x3
proof assume
A1: c = x`3;
let x1,x2,x3,x4 such that
A2: x = [x1,x2,x3,x4];
x = [x`1,x`2,x`3,x`4] by MCART_1:60;
hence thesis by A1,A2,MCART_1:33;
end;
thus thesis by MCART_1:81;
end;
theorem
d=x`4 iff for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds d = x4
proof
thus d =x`4 implies for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds d = x4
proof assume
A1: d = x`4;
let x1,x2,x3,x4 such that
A2: x = [x1,x2,x3,x4];
x = [x`1,x`2,x`3,x`4] by MCART_1:60;
hence thesis by A1,A2,MCART_1:33;
end;
thus thesis by MCART_1:82;
end;
canceled;
theorem
for x,y being Element of [:X1,X2,X3,X4:]
st x`1=y`1 & x`2=y`2 & x`3=y`3 & x`4=y`4 holds x=y
proof let x,y be Element of [:X1,X2,X3,X4:];
[x`1,x`2,x`3,x`4]=x & [y`1,y`2,y`3,y`4]=y by MCART_1:60;
hence thesis;
end;
reserve A2 for Subset of X2,
A3 for Subset of X3,
A4 for Subset of X4;
scheme Fraenkel1 {P[set]}:
for X1 holds { x1 : P[x1] } is Subset of X1
proof let X1;
{ x1 : P[x1] } c= X1
proof let a; assume a in { x1 : P[x1] };
then ex x1 st a = x1 & P[x1];
hence thesis;
end;
hence thesis;
end;
scheme Fraenkel2 {P[set,set]}:
for X1,X2 holds { [x1,x2] : P[x1,x2] } is Subset of [:X1,X2:]
proof let X1,X2;
{ [x1,x2] : P[x1,x2] } c= [:X1,X2:]
proof let a; assume a in { [x1,x2] : P[x1,x2] };
then ex x1,x2 st a = [x1,x2] & P[x1,x2];
hence thesis;
end;
hence thesis;
end;
scheme Fraenkel3 {P[set,set,set]}:
for X1,X2,X3 holds { [x1,x2,x3] : P[x1,x2,x3] } is Subset of [:X1,X2,X3:]
proof let X1,X2,X3;
{ [x1,x2,x3] : P[x1,x2,x3] } c= [:X1,X2,X3:]
proof let a; assume a in { [x1,x2,x3] : P[x1,x2,x3] };
then ex x1,x2,x3 st a = [x1,x2,x3] & P[x1,x2,x3];
hence thesis;
end;
hence thesis;
end;
scheme Fraenkel4 {P[set,set,set,set]}:
for X1,X2,X3,X4 holds
{ [x1,x2,x3,x4] : P[x1,x2,x3,x4] } is Subset of [:X1,X2,X3,X4:]
proof let X1,X2,X3,X4;
{ [x1,x2,x3,x4] : P[x1,x2,x3,x4] } c= [:X1,X2,X3,X4:]
proof let a; assume a in { [x1,x2,x3,x4] : P[x1,x2,x3,x4] };
then ex x1,x2,x3,x4 st a = [x1,x2,x3,x4] & P[x1,x2,x3,x4];
hence thesis;
end;
hence thesis;
end;
scheme Fraenkel5 {P[set],Q[set]}:
for X1 st for x1 holds P[x1] implies Q[x1]
holds { y1 : P[y1] } c= { z1 : Q[z1] }
proof let X1 such that
A1: P[x1] implies Q[x1];
let a; assume a in { x1 : P[x1] };
then consider x1 such that
A2: a = x1 and
A3: P[x1];
Q[x1] by A1,A3;
hence thesis by A2;
end;
scheme Fraenkel6 {P[set],Q[set]}:
for X1 st for x1 holds P[x1] iff Q[x1]
holds { y1 : P[y1] } = { z1 : Q[z1] }
proof
defpred p[set] means P[$1];
defpred q[set] means Q[$1];
A1: for X1 st for x1 holds p[x1] implies q[x1]
holds { y1 : p[y1] } c= { z1 : q[z1] } from Fraenkel5;
A2: for X1 st for x1 holds q[x1] implies p[x1]
holds { y1 : q[y1] } c= { z1 : p[z1] } from Fraenkel5;
let X1; assume
A3: P[x1] iff Q[x1];
hence { y1 : P[y1] } c= { z1 : Q[z1] } by A1;
thus { y1 : Q[y1] } c= { z1 : P[z1] } by A2,A3;
end;
scheme SubsetD{D() -> non empty set,P[set]}:
{d where d is Element of D() : P[d]} is Subset of D()
proof
defpred R[set] means P[$1];
for D being non empty set holds
{d where d is Element of D : R[d]} is Subset of D
from Fraenkel1;
hence thesis;
end;
canceled 2;
theorem
X1 = { x1 : not contradiction }
proof
defpred P[set] means not contradiction;
A1: y1 in { x1 : not contradiction };
{ x1 : P[x1] } is Subset of X1 from SubsetD;
hence thesis by A1,SUBSET_1:49;
end;
theorem
[:X1,X2:] = { [x1,x2] : not contradiction }
proof
A1: for x being Element of [:X1,X2:] holds x in { [x1,x2] : not contradiction }
proof let x be Element of [:X1,X2:]; x = [x`1,x`2] by MCART_1:23;
hence x in { [x1,x2] : not contradiction };
end;
defpred P[set,set] means not contradiction;
for X1,X2 holds { [x1,x2] : P[x1,x2] } is Subset of [:X1,X2:]
from Fraenkel2;
then { [x1,x2] : not contradiction } is Subset of [:X1,X2:];
hence thesis by A1,SUBSET_1:49;
end;
theorem
[:X1,X2,X3:] = { [x1,x2,x3] : not contradiction }
proof
A1: for x being Element of [:X1,X2,X3:]
holds x in { [x1,x2,x3] : not contradiction }
proof let x be Element of [:X1,X2,X3:]; x = [x`1,x`2,x`3] by MCART_1:48;
hence x in { [x1,x2,x3] : not contradiction };
end;
defpred P[set,set,set] means not contradiction;
for X1,X2,X3 holds
{ [x1,x2,x3] : P[x1,x2,x3] } is Subset of [:X1,X2,X3:]
from Fraenkel3;
then { [x1,x2,x3] : not contradiction } is Subset of [:X1,X2,X3:];
hence thesis by A1,SUBSET_1:49;
end;
theorem
[:X1,X2,X3,X4:] = { [x1,x2,x3,x4] : not contradiction }
proof
A1: for x being Element of [:X1,X2,X3,X4:]
holds x in { [x1,x2,x3,x4] : not contradiction }
proof let x be Element of [:X1,X2,X3,X4:]; x = [x`1,x`2,x`3,x`4] by MCART_1:
60;
hence x in { [x1,x2,x3,x4] : not contradiction };
end;
defpred P[set,set,set,set] means not contradiction;
for X1,X2,X3,X4 holds
{ [x1,x2,x3,x4] : P[x1,x2,x3,x4] } is Subset of [:X1,X2,X3,X4:]
from Fraenkel4;
then { [x1,x2,x3,x4] : not contradiction } is Subset of [:X1,X2,X3,X4:];
hence thesis by A1,SUBSET_1:49;
end;
theorem
A1 = { x1 : x1 in A1 }
proof
thus A1 c= { x1 : x1 in A1 }
proof let a; assume
a in A1;
hence a in { x1 : x1 in A1 };
end;
let a;
assume a in { x1 : x1 in A1 };
then ex x1 st a = x1 & x1 in A1;
hence a in A1;
end;
theorem
[:A1,A2:] = { [x1,x2] : x1 in A1 & x2 in A2 }
proof
thus [:A1,A2:] c= { [x1,x2] : x1 in A1 & x2 in A2 }
proof let a; assume
A1: a in [:A1,A2:];
then reconsider x = a as Element of [:X1,X2:];
x = [x`1,x`2] & x`1 in A1 & x`2 in A2 by A1,MCART_1:10,23;
hence a in { [x1,x2] : x1 in A1 & x2 in A2 };
end;
let a;
assume a in { [x1,x2] : x1 in A1 & x2 in A2 };
then ex x1,x2 st a = [x1,x2] & x1 in A1 & x2 in A2;
hence a in [:A1,A2:] by ZFMISC_1:106;
end;
theorem
[:A1,A2,A3:] = { [x1,x2,x3] : x1 in A1 & x2 in A2 & x3 in A3 }
proof
thus [:A1,A2,A3:] c= { [x1,x2,x3] : x1 in A1 & x2 in A2 & x3 in A3 }
proof let a; assume
A1: a in [:A1,A2,A3:];
then reconsider x = a as Element of [:X1,X2,X3:];
x = [x`1,x`2,x`3] & x`1 in A1 & x`2 in A2 & x`3 in
A3 by A1,MCART_1:48,76;
hence a in { [x1,x2,x3] : x1 in A1 & x2 in A2 & x3 in A3 };
end;
let a;
assume a in { [x1,x2,x3] : x1 in A1 & x2 in A2 & x3 in A3 };
then ex x1,x2,x3 st a= [x1,x2,x3] & x1 in A1 & x2 in A2 & x3 in A3;
hence a in [:A1,A2,A3:] by MCART_1:73;
end;
theorem
[:A1,A2,A3,A4:] = { [x1,x2,x3,x4] : x1 in A1 & x2 in A2 & x3 in A3 & x4 in
A4 }
proof
thus
[:A1,A2,A3,A4:] c= { [x1,x2,x3,x4] : x1 in A1 & x2 in A2 & x3 in A3 & x4
in
A4 }
proof let a; assume
A1: a in [:A1,A2,A3,A4:];
then reconsider x = a as Element of [:X1,X2,X3,X4:];
x = [x`1,x`2,x`3,x`4] & x`1 in A1 & x`2 in A2 & x`3 in A3 & x`4 in A4
by A1,MCART_1:60,87;
hence a in { [x1,x2,x3,x4] : x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 };
end;
let a;
assume a in { [x1,x2,x3,x4] : x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 };
then ex x1,x2,x3,x4 st
a = [x1,x2,x3,x4] & x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4;
hence a in [:A1,A2,A3,A4:] by MCART_1:84;
end;
theorem
{} X1 = { x1 : contradiction }
proof
thus {} X1 c= { x1 : contradiction }
proof let a; thus thesis; end;
let a;
assume a in { x1 : contradiction };
then ex x1 st a = x1 & contradiction;
hence a in {} X1;
end;
theorem
A1` = { x1 : not x1 in A1 }
proof
thus A1` c= { x1 : not x1 in A1 }
proof let a; assume a in A1`;
then not a in A1 & a is Element of X1 by SUBSET_1:54;
hence a in { x1 : not x1 in A1 };
end;
let a;
assume a in { x1 : not x1 in A1 };
then ex x1 st a = x1 & not x1 in A1;
hence a in A1` by SUBSET_1:50;
end;
theorem
A1 /\ B1 = { x1 : x1 in A1 & x1 in B1 }
proof
thus A1 /\ B1 c= { x1 : x1 in A1 & x1 in B1 }
proof let a; assume
A1: a in A1 /\ B1;
then reconsider x = a as Element of X1;
x in A1 & x in B1 by A1,XBOOLE_0:def 3;
hence a in { x1 : x1 in A1 & x1 in B1 };
end;
let a;
assume a in { x1 : x1 in A1 & x1 in B1 };
then ex x1 st a = x1 & x1 in A1 & x1 in B1;
hence a in A1 /\ B1 by XBOOLE_0:def 3;
end;
theorem
A1 \/ B1 = { x1 : x1 in A1 or x1 in B1 }
proof
thus A1 \/ B1 c= { x1 : x1 in A1 or x1 in B1 }
proof let a; assume
A1: a in A1 \/ B1;
then reconsider x = a as Element of X1;
x in A1 or x in B1 by A1,XBOOLE_0:def 2;
hence a in { x1 : x1 in A1 or x1 in B1 };
end;
let a;
assume a in { x1 : x1 in A1 or x1 in B1 };
then ex x1 st a = x1 & (x1 in A1 or x1 in B1);
hence a in A1 \/ B1 by XBOOLE_0:def 2;
end;
theorem
A1 \ B1 = { x1 : x1 in A1 & not x1 in B1 }
proof
thus A1 \ B1 c= { x1 : x1 in A1 & not x1 in B1 }
proof let a; assume
A1: a in A1 \ B1;
then reconsider x = a as Element of X1;
x in A1 & not x in B1 by A1,XBOOLE_0:def 4;
hence a in { x1 : x1 in A1 & not x1 in B1 };
end;
let a;
assume a in { x1 : x1 in A1 & not x1 in B1 };
then ex x1 st a = x1 & x1 in A1 & not x1 in B1;
hence a in A1 \ B1 by XBOOLE_0:def 4;
end;
theorem Th61:
A1 \+\ B1 = { x1 : x1 in A1 & not x1 in B1 or not x1 in A1 & x1 in B1 }
proof
thus A1 \+\ B1 c= { x1 : x1 in A1 & not x1 in B1 or not x1 in A1 & x1 in B1}
proof let a; assume
A1: a in A1 \+\ B1;
then reconsider x = a as Element of X1;
x in A1 & not x in B1 or not x in A1 & x in B1 by A1,XBOOLE_0:1;
hence a in { x1 : x1 in A1 & not x1 in B1 or not x1 in A1 & x1 in B1 };
end;
let a;
assume a in { x1 : x1 in A1 & not x1 in B1 or not x1 in A1 & x1 in B1 };
then ex x1 st a = x1 & (x1 in A1 & not x1 in B1 or not x1 in A1 & x1 in B1);
hence a in A1 \+\ B1 by XBOOLE_0:1;
end;
theorem Th62:
A1 \+\ B1 = { x1 : not x1 in A1 iff x1 in B1 }
proof
A1: for x1 holds
(x1 in A1 & not x1 in B1 or not x1 in A1 & x1 in B1)
iff (not x1 in A1 iff x1 in B1);
defpred P[set] means $1 in A1 & not $1 in B1 or not $1 in A1 & $1 in B1;
defpred Q[set] means not $1 in A1 iff $1 in B1;
A2: for X1 st
for x1 holds P[x1] iff Q[x1]
holds { y1 : P[y1] } = { z1 : Q[z1] } from Fraenkel6;
A1 \+\ B1 = { x1 : x1 in A1 & not x1 in B1 or not x1 in A1 & x1 in
B1 } by Th61;
hence thesis by A1,A2;
end;
theorem
A1 \+\ B1 = { x1 : x1 in A1 iff not x1 in B1 }
proof
A1: for x1 holds (not x1 in A1 iff x1 in B1) iff (x1 in A1 iff not x1 in B1);
defpred P[set] means not $1 in A1 iff $1 in B1;
defpred Q[set] means $1 in A1 iff not $1 in B1;
A2: for X1 st
for x1 holds P[x1] iff Q[x1]
holds { y1 : P[y1] } = { z1 : Q[z1] } from Fraenkel6;
A1 \+\ B1 = { x1 : not x1 in A1 iff x1 in B1 } by Th62;
hence thesis by A1,A2;
end;
theorem
A1 \+\ B1 = { x1 : not(x1 in A1 iff x1 in B1) }
proof
A1: for x1 holds (not x1 in A1 iff x1 in B1) iff not(x1 in A1 iff x1 in B1);
defpred P[set] means not $1 in A1 iff $1 in B1;
defpred Q[set] means not($1 in A1 iff $1 in B1);
A2: for X1 st
for x1 holds P[x1] iff Q[x1]
holds { y1 : P[y1] } = { z1 : Q[z1] } from Fraenkel6;
A1 \+\ B1 = { x1 : not x1 in A1 iff x1 in B1 } by Th62;
hence thesis by A1,A2;
end;
definition let D be non empty set;
let x1 be Element of D;
redefine func {x1} -> Subset of D;
coherence by SUBSET_1:55;
let x2 be Element of D;
redefine func {x1,x2} -> Subset of D;
coherence by SUBSET_1:56;
let x3 be Element of D;
redefine func {x1,x2,x3} -> Subset of D;
coherence by SUBSET_1:57;
let x4 be Element of D;
redefine func {x1,x2,x3,x4} -> Subset of D;
coherence by SUBSET_1:58;
let x5 be Element of D;
redefine func {x1,x2,x3,x4,x5} -> Subset of D;
coherence by SUBSET_1:59;
let x6 be Element of D;
redefine func {x1,x2,x3,x4,x5,x6} -> Subset of D;
coherence by SUBSET_1:60;
let x7 be Element of D;
redefine func {x1,x2,x3,x4,x5,x6,x7} -> Subset of D;
coherence by SUBSET_1:61;
let x8 be Element of D;
redefine func {x1,x2,x3,x4,x5,x6,x7,x8} -> Subset of D;
coherence by SUBSET_1:62;
end;