:: Domains and Their Cartesian Products
:: by Andrzej Trybulec
::
:: Received April 3, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, SUBSET_1, ZFMISC_1, MCART_1, TARSKI, ORDINAL1,
RECDEF_2;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1,
FUNCT_1, MCART_1;
constructors TARSKI, ENUMSET1, MCART_1, ORDINAL1, PARTFUN1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, XTUPLE_0, MCART_1;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0, ORDINAL1;
equalities TARSKI, SUBSET_1, XTUPLE_0;
expansions TARSKI;
theorems TARSKI, SUBSET_1, MCART_1, ZFMISC_1, XBOOLE_0;
begin
reserve s for set,
a,b,c,d for object,
D,X1,X2,X3,X4 for non empty set,
x1,y1,z1 for Element of X1,
x2 for Element of X2,
x3 for Element of X3,
x4 for Element of X4,
A1,B1 for Subset of X1;
:: Domains and their elements
theorem
a in [:X1,X2:] implies ex x1,x2 st a = [x1,x2]
proof
assume a in [:X1,X2:];
then consider x1,x2 being object such that
A1: x1 in X1 and
A2: x2 in X2 and
A3: a = [x1,x2] by ZFMISC_1:def 2;
reconsider x2 as Element of X2 by A2;
reconsider x1 as Element of X1 by A1;
take x1,x2;
thus thesis by A3;
end;
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;
hence thesis by MCART_1:21;
end;
definition
let X1,X2,x1,x2;
redefine func [x1,x2] -> Element of [:X1,X2:]; :: redefines [ (TARSKI, definition)
coherence by ZFMISC_1:87;
end;
definition
let X1,X2;
let x be Element of [:X1,X2:];
redefine func x`1 -> Element of X1; :: redefines `1 (XTUPLE_0, definition)
coherence by MCART_1:10;
redefine func x`2 -> Element of X2; :: redefines `2 (XTUPLE_0, definition)
coherence by MCART_1:10;
end;
:: Cartesian products of three sets
theorem Th3:
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 object such that
A1: x12 in [:X1,X2:] and
A2: x3 in X3 and
A3: a = [x12,x3] by ZFMISC_1:def 2;
reconsider x3 as Element of X3 by A2;
consider x1,x2 being object such that
A4: x1 in X1 and
A5: x2 in X2 and
A6: x12 = [x1,x2] by A1,ZFMISC_1:def 2;
reconsider x2 as Element of X2 by A5;
reconsider x1 as Element of X1 by A4;
a = [x1,x2,x3] by A3,A6;
hence thesis;
end;
given x1,x2,x3 such that
A7: a = [x1,x2,x3];
a = [[x1,x2],x3] by A7;
then a in [:[:X1,X2:],X3:];
hence thesis by ZFMISC_1:def 3;
end;
theorem Th4:
(for s holds s in D iff ex x1,x2,x3 st s = [x1,x2,x3]) implies
D = [: X1,X2,X3 :]
proof
assume
A1: for s holds s in D iff ex x1,x2,x3 st s = [x1,x2,x3];
now
let a be object;
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;
hence thesis;
end;
assume a in [:[:X1,X2:],X3:];
then consider x12,x3 being object such that
A3: x12 in [:X1,X2:] and
A4: x3 in X3 and
A5: a = [x12,x3] by ZFMISC_1:def 2;
reconsider x3 as Element of X3 by A4;
consider x1,x2 being object such that
A6: x1 in X1 and
A7: x2 in X2 and
A8: x12 = [x1,x2] by A3,ZFMISC_1:def 2;
reconsider x2 as Element of X2 by A7;
reconsider x1 as Element of X1 by A6;
a = [x1,x2,x3] by A5,A8;
hence a in D by A1;
end;
then D = [:[:X1,X2:],X3:] by TARSKI:2;
hence thesis by ZFMISC_1:def 3;
end;
theorem
D = [: X1,X2,X3 :] iff
for s holds s in D iff ex x1,x2,x3 st s = [x1,x2,x3] by Th3,Th4;
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:]; :: redefines [ (XTUPLE_0, definition)
coherence by MCART_1:69;
end;
theorem
a = x`1_3 iff for x1,x2,x3 st x = [x1,x2,x3] holds a = x1
by MCART_1:65;
theorem
b = x`2_3 iff for x1,x2,x3 st x = [x1,x2,x3] holds b = x2
by MCART_1:66;
theorem
c = x`3_3 iff for x1,x2,x3 st x = [x1,x2,x3] holds c = x3
by MCART_1:67;
AA:
for X1,X2,X3 being non empty set
for x being Element of [:X1,X2,
X3:] holds x = [x`1_3,x`2_3,x`3_3];
theorem
x`1_3 = y`1_3 & x`2_3 = y`2_3 & x`3_3 = y`3_3 implies x = y
proof
[x`1_3,x`2_3,x`3_3]=x;
hence thesis by AA;
end;
theorem Th10:
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 object such that
A1: x123 in [:X1,X2,X3:] and
A2: x4 in X4 and
A3: a = [x123,x4] by ZFMISC_1:def 2;
reconsider x4 as Element of X4 by A2;
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,Th3;
a = [x1,x2,x3,x4] by A3,A4;
hence thesis;
end;
given x1,x2,x3,x4 such that
A5: a = [x1,x2,x3,x4];
a = [[x1,x2,x3],x4] by A5;
then a in [:[:X1,X2,X3:],X4:];
hence thesis by ZFMISC_1:def 4;
end;
theorem Th11:
(for s holds s in D iff ex x1,x2,x3,x4 st s = [x1,x2,x3,x4])
implies D = [: X1,X2,X3,X4 :]
proof
assume
A1: for s holds s in D iff ex x1,x2,x3,x4 st s = [x1,x2,x3,x4];
now
let a be object;
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;
hence thesis;
end;
assume a in [:[:X1,X2,X3:],X4:];
then consider x123,x4 being object 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,Th3;
a = [x1,x2,x3,x4] by A5,A6;
hence a in D by A1;
end;
then D = [:[:X1,X2,X3:],X4:] by TARSKI:2;
hence thesis by ZFMISC_1:def 4;
end;
theorem
D = [: X1,X2,X3,X4 :] iff for s holds s in D iff ex x1,x2,x3,x4 st s =
[x1,x2,x3,x4] by Th10,Th11;
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:]; :: redefines [ (XTUPLE_0, definition)
coherence by MCART_1:80;
end;
theorem
a = x`1_4 iff for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds a = x1
by MCART_1:75;
theorem
b = x`2_4 iff for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds b = x2
by MCART_1:76;
theorem
c = x`3_4 iff for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds c = x3
by MCART_1:77;
theorem
d = x`4_4 iff for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds d = x4
by MCART_1:78;
AB: for X1,X2,X3,X4 being non empty set
for x being Element of
[:X1,X2,X3,X4:] holds x = [x`1_4,x`2_4,x`3_4,x`4_4];
theorem
for x,y being Element of [:X1,X2,X3,X4:]
st x`1_4=y`1_4 & x`2_4=y`2_4 & x`3_4=y
`3_4 & x`4_4=y`4_4 holds x=y
proof
let x,y be Element of [:X1,X2,X3,X4:];
[x`1_4,x`2_4,x`3_4,x`4_4]=x;
hence thesis by AB;
end;
reserve A2 for Subset of X2,
A3 for Subset of X3,
A4 for Subset of X4;
scheme
Fraenkel1 {P[object]}: for X1 holds { x1 : P[x1] } is Subset of X1 proof
let X1;
{ x1 : P[x1] } c= X1
proof
let a be object;
assume a in { x1 : P[x1] };
then ex x1 st a = x1 & P[x1];
hence thesis;
end;
hence thesis;
end;
scheme
Fraenkel2 {P[object,object]}:
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 be object;
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[object,object,object]}:
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 be object;
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[object,object,object,object]}:
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 be object;
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,Q[object]}: 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 be object;
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,Q[object]}: for X1 st for x1 holds P[x1] iff Q[x1] holds { y1
: P[y1] } = { z1 : Q[z1] } proof
let X1;
assume
A1: P[x1] iff Q[x1];
for X1 st for x1 holds P[x1] implies Q[x1] holds { y1 : P[y1] } c= { z1
: Q[z1] } from Fraenkel5;
hence { y1 : P[y1] } c= { z1 : Q[z1] } by A1;
for X1 st for x1 holds Q[x1] implies P[x1] holds { y1 : Q[y1] } c= { z1
: P[z1] } from Fraenkel5;
hence thesis by A1;
end;
scheme
SubsetD{D() -> non empty set,P[object]}: {d where d is Element of D() : P[d]}
is Subset of D() proof
for D being non empty set holds {d where d is Element of D : P[d]} is
Subset of D from Fraenkel1;
hence thesis;
end;
theorem
X1 = the set of all x1
proof
defpred P[set] means not contradiction;
A1: y1 in the set of all x1 ;
{ x1 : P[x1] } is Subset of X1 from SubsetD;
hence thesis by A1,SUBSET_1:28;
end;
theorem
[:X1,X2:] = the set of all [x1,x2]
proof
defpred P[set,set] means not contradiction;
A1: for x being Element of [:X1,X2:] holds x in the set of all [x1,x2]
proof
let x be Element of [:X1,X2:];
x = [x`1,x`2];
hence thesis;
end;
for X1,X2 holds { [x1,x2] : P[x1,x2] } is Subset of [:X1,X2:] from
Fraenkel2;
then the set of all [x1,x2] is Subset of [:X1,X2:];
hence thesis by A1,SUBSET_1:28;
end;
theorem
[:X1,X2,X3:] = the set of all [x1,x2,x3]
proof
defpred P[set,set,set] means not contradiction;
A1: for x being Element of [:X1,X2,X3:] holds x in the set of all [x1,x2,x3]
proof
let x be Element of [:X1,X2,X3:];
x = [x`1_3,x`2_3,x`3_3];
hence thesis;
end;
for X1,X2,X3 holds { [x1,x2,x3] : P[x1,x2,x3] } is Subset of [:X1,X2,X3
:] from Fraenkel3;
then the set of all [x1,x2,x3] is Subset of [:X1,X2,X3:];
hence thesis by A1,SUBSET_1:28;
end;
theorem
[:X1,X2,X3,X4:] = the set of all [x1,x2,x3,x4]
proof
defpred P[set,set,set,set] means not contradiction;
A1: for x being Element of [:X1,X2,X3,X4:] holds x in the set of all
[x1,x2,x3,x4]
proof
let x be Element of [:X1,X2,X3,X4:];
x = [x`1_4,x`2_4,x`3_4,x`4_4];
hence thesis;
end;
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 the set of all [x1,x2,x3,x4] is Subset of [:X1,X2,X3,X4:];
hence thesis by A1,SUBSET_1:28;
end;
theorem
A1 = { x1 : x1 in A1 }
proof
thus A1 c= { x1 : x1 in A1 };
let a be object;
assume a in { x1 : x1 in A1 };
then ex x1 st a = x1 & x1 in A1;
hence thesis;
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 be object;
assume
A1: a in [:A1,A2:];
then reconsider x = a as Element of [:X1,X2:];
A2: x = [x`1,x`2];
x`1 in A1 & x`2 in A2 by A1,MCART_1:10;
hence thesis by A2;
end;
let a be object;
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 thesis by ZFMISC_1:87;
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 be object;
assume
A1: a in [:A1,A2,A3:];
reconsider A1 as non empty Subset of X1 by A1,MCART_1:31;
reconsider A2 as non empty Subset of X2 by A1,MCART_1:31;
reconsider A3 as non empty Subset of X3 by A1,MCART_1:31;
A2: a in [:A1,A2,A3:] by A1;
reconsider x = a as Element of [:X1,X2,X3:] by A2;
A3: x = [x`1_3,x`2_3,x`3_3];
A4: x`3_3 in A3 by A2,MCART_1:72;
x`1_3 in A1 & x`2_3 in A2 by A2,MCART_1:72;
hence thesis by A4,A3;
end;
let a be object;
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 thesis by MCART_1:69;
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 be object;
assume
A1: a in [:A1,A2,A3,A4:];
reconsider A1 as non empty Subset of X1 by A1,MCART_1:51;
reconsider A2 as non empty Subset of X2 by A1,MCART_1:51;
reconsider A3 as non empty Subset of X3 by A1,MCART_1:51;
reconsider A4 as non empty Subset of X4 by A1,MCART_1:51;
A2: a in [:A1,A2,A3,A4:] by A1;
then reconsider x = a as Element of [:X1,X2,X3,X4:];
A3: x`3_4 in A3 & x`4_4 in A4 by A2,MCART_1:83;
A4: x = [x`1_4,x`2_4,x`3_4,x`4_4];
x`1_4 in A1 & x`2_4 in A2 by A2,MCART_1:83;
hence thesis by A4,A3;
end;
let a be object;
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 thesis by MCART_1:80;
end;
theorem
{} X1 = { x1 : contradiction }
proof
thus {} X1 c= { x1 : contradiction };
let a be object;
assume a in { x1 : contradiction };
then ex x1 st a = x1 & contradiction;
hence thesis;
end;
theorem
A1` = { x1 : not x1 in A1 }
proof
thus A1` c= { x1 : not x1 in A1 }
proof
let a be object;
assume
A1: a in A1`;
then not a in A1 by XBOOLE_0:def 5;
hence thesis by A1;
end;
let a be object;
assume a in { x1 : not x1 in A1 };
then ex x1 st a = x1 & not x1 in A1;
hence thesis by SUBSET_1:29;
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 be object;
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 4;
hence thesis;
end;
let a be object;
assume a in { x1 : x1 in A1 & x1 in B1 };
then ex x1 st a = x1 & x1 in A1 & x1 in B1;
hence thesis by XBOOLE_0:def 4;
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 be object;
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 3;
hence thesis;
end;
let a be object;
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 thesis by XBOOLE_0:def 3;
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 be object;
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 5;
hence thesis;
end;
let a be object;
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 thesis by XBOOLE_0:def 5;
end;
theorem Th31:
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 be object;
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 thesis;
end;
let a be object;
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 thesis by XBOOLE_0:1;
end;
theorem Th32:
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 Q[set] means not $1 in A1 iff $1 in B1;
defpred P[set] means $1 in A1 & not $1 in B1 or not $1 in A1 & $1 in B1;
A2: A1 \+\ B1 = { x1 : x1 in A1 & not x1 in B1 or not x1 in A1 & x1 in B1 }
by Th31;
for X1 st for x1 holds P[x1] iff Q[x1] holds { y1 : P[y1] } = { z1 : Q[
z1] } from Fraenkel6;
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 Q[set] means $1 in A1 iff not $1 in B1;
defpred P[set] means not $1 in A1 iff $1 in B1;
A2: A1 \+\ B1 = { x1 : not x1 in A1 iff x1 in B1 } by Th32;
for X1 st for x1 holds P[x1] iff Q[x1] holds { y1 : P[y1] } = { z1 : Q[
z1] } from Fraenkel6;
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 Q[set] means not($1 in A1 iff $1 in B1);
defpred P[set] means not $1 in A1 iff $1 in B1;
A2: A1 \+\ B1 = { x1 : not x1 in A1 iff x1 in B1 } by Th32;
for X1 st for x1 holds P[x1] iff Q[x1] holds { y1 : P[y1] } = { z1 : Q[
z1] } from Fraenkel6;
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; :: redefines { (TARSKI, definition)
coherence by SUBSET_1:33;
let x2 be Element of D;
redefine func {x1,x2} -> Subset of D; :: redefines { (TARSKI, definition)
coherence by SUBSET_1:34;
let x3 be Element of D;
redefine func {x1,x2,x3} -> Subset of D; :: redefines { (ENUMSET1, definition)
coherence by SUBSET_1:35;
let x4 be Element of D;
redefine func {x1,x2,x3,x4} -> Subset of D; :: redefines { (ENUMSET1, definition)
coherence by SUBSET_1:36;
let x5 be Element of D;
redefine func {x1,x2,x3,x4,x5} -> Subset of D; :: redefines { (ENUMSET1, definition)
coherence by SUBSET_1:37;
let x6 be Element of D;
redefine func {x1,x2,x3,x4,x5,x6} -> Subset of D; :: redefines { (ENUMSET1, definition)
coherence by SUBSET_1:38;
let x7 be Element of D;
redefine func {x1,x2,x3,x4,x5,x6,x7} -> Subset of D; :: redefines { (ENUMSET1, definition)
coherence by SUBSET_1:39;
let x8 be Element of D;
redefine func {x1,x2,x3,x4,x5,x6,x7,x8} -> Subset of D; :: redefines { (ENUMSET1, definition)
coherence by SUBSET_1:40;
let x9 be Element of D;
redefine func {x1,x2,x3,x4,x5,x6,x7,x8,x9} -> Subset of D; :: redefines { (ENUMSET1, definition)
coherence by SUBSET_1:52;
let x10 be Element of D;
redefine func {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} -> Subset of D; :: redefines { (ENUMSET1, definition)
coherence by SUBSET_1:53;
end;
begin :: Addenda
:: from COMPLSP1
scheme
SubsetFD { A, D() -> non empty set, F(object) -> Element of D(), P[object] }:
{ F(x) where x is Element of A(): P[x]} is Subset of D() proof
set X = { F(x) where x is Element of A(): P[x]};
X c= D()
proof
let y be object;
assume y in X;
then ex z being Element of A() st y = F(z) & P[z];
hence thesis;
end;
hence thesis;
end;
scheme
SubsetFD2 { A, B, D() -> non empty set, F(object,object) -> Element of D(),
P[object,object] }:
{ F(x,y) where x is Element of A(), y is Element of B(): P[x,y]}
is Subset of D()
proof
set X = { F(x,y) where x is Element of A(), y is Element of B(): P[x,y]};
X c= D()
proof
let w be object;
assume w in X;
then
ex x being Element of A(), y being Element of B() st w = F(x,y) & P[ x ,y];
hence thesis;
end;
hence thesis;
end;
definition
let D1,D2,D3 be non empty set, x be Element of [:[:D1,D2:],D3:];
redefine func x`11 -> Element of D1; :: redefines `11 (MCART_1, definition)
coherence
proof
x`11 = x`1`1 by MCART_1:def 14;
hence thesis;
end;
redefine func x`12 -> Element of D2; :: redefines `12 (MCART_1, definition)
coherence
proof
x`12 = x`1`2 by MCART_1:def 15;
hence thesis;
end;
end;
definition
let D1,D2,D3 be non empty set, x be Element of [:D1,[:D2,D3:]:];
redefine func x`21 -> Element of D2; :: redefines `21 (MCART_1, definition)
coherence
proof
x`21 = x`2`1 by MCART_1:def 16;
hence thesis;
end;
redefine func x`22 -> Element of D3; :: redefines `22 (MCART_1, definition)
coherence
proof
x`22 = x`2`2 by MCART_1:def 17;
hence thesis;
end;
end;
:: from JORDAN_A, 2005.10.12 , A.T.
scheme
AndScheme{A()-> non empty set, P,Q[object]}: { a where a is Element of A():
P[a] & Q[a] } = { a1 where a1 is Element of A(): P[a1] } /\ { a2 where a2 is
Element of A(): Q[a2] } proof
set A = { a where a is Element of A(): P[a] & Q[a] }, A1 = { a1 where a1 is
Element of A(): P[a1] }, A2 = { a2 where a2 is Element of A(): Q[a2] };
thus A c= A1 /\ A2
proof
let x be object;
assume x in A;
then consider a being Element of A() such that
A1: x = a and
A2: ( P[a])& Q[a];
a in A1 & a in A2 by A2;
hence thesis by A1,XBOOLE_0:def 4;
end;
let x be object;
assume
A3: x in A1 /\ A2;
then x in A2 by XBOOLE_0:def 4;
then
A4: ex a being Element of A() st x = a & Q[a];
x in A1 by A3,XBOOLE_0:def 4;
then ex a being Element of A() st x = a & P[a];
hence thesis by A4;
end;
:: from HAHNBAN, 2011.04.26, A.T.
registration
let A be non empty set;
cluster c=-linear non empty for Subset of A;
existence
proof
set a = the Element of A;
reconsider B = { a } as non empty Subset of A;
take B;
B is c=-linear
proof
let x,y be set;
assume that
A1: x in B and
A2: y in B;
x = a by A1,TARSKI:def 1;
hence thesis by A2,TARSKI:def 1;
end;
hence thesis;
end;
end;