mcart_1.miz
begin
reserve v,x,x1,x2,x3,x4,y,y1,y2,y3,y4,z,z1,z2 for
object,
X,X1,X2,X3,X4,Y,Y1,Y2,Y3,Y4,Y5,Z,Z1,Z2,Z3,Z4,Z5 for
set;
reserve p for
pair
object;
::$Canceled
theorem ::
MCART_1:9
X
<>
{} implies ex v st v
in X & not ex x, y st (x
in X or y
in X) & v
=
[x, y]
proof
assume X
<>
{} ;
then
consider Y such that
A1: Y
in X and
A2: not ex Y1 st Y1
in Y & not Y1
misses X by
XREGULAR: 2;
take v = Y;
thus v
in X by
A1;
given x, y such that
A3: x
in X or y
in X and
A4: v
=
[x, y];
A5:
{x, y}
in Y by
A4,
TARSKI:def 2;
x
in
{x, y} & y
in
{x, y} by
TARSKI:def 2;
hence contradiction by
A2,
A5,
A3,
XBOOLE_0: 3;
end;
theorem ::
MCART_1:10
Th4: z
in
[:X, Y:] implies (z
`1 )
in X & (z
`2 )
in Y
proof
assume z
in
[:X, Y:];
then
consider x,y be
object such that
A1: x
in X & y
in Y & z
=
[x, y] by
ZFMISC_1:def 2;
thus thesis by
A1;
end;
::$Canceled
theorem ::
MCART_1:12
z
in
[:
{x}, Y:] implies (z
`1 )
= x & (z
`2 )
in Y
proof
assume
A1: z
in
[:
{x}, Y:];
then (z
`1 )
in
{x} by
Th4;
hence thesis by
A1,
Th4,
TARSKI:def 1;
end;
theorem ::
MCART_1:13
z
in
[:X,
{y}:] implies (z
`1 )
in X & (z
`2 )
= y
proof
assume
A1: z
in
[:X,
{y}:];
then (z
`2 )
in
{y} by
Th4;
hence thesis by
A1,
Th4,
TARSKI:def 1;
end;
theorem ::
MCART_1:14
z
in
[:
{x},
{y}:] implies (z
`1 )
= x & (z
`2 )
= y
proof
assume z
in
[:
{x},
{y}:];
then (z
`1 )
in
{x} & (z
`2 )
in
{y} by
Th4;
hence thesis by
TARSKI:def 1;
end;
theorem ::
MCART_1:15
z
in
[:
{x1, x2}, Y:] implies ((z
`1 )
= x1 or (z
`1 )
= x2) & (z
`2 )
in Y
proof
assume
A1: z
in
[:
{x1, x2}, Y:];
then (z
`1 )
in
{x1, x2} by
Th4;
hence thesis by
A1,
Th4,
TARSKI:def 2;
end;
theorem ::
MCART_1:16
z
in
[:X,
{y1, y2}:] implies (z
`1 )
in X & ((z
`2 )
= y1 or (z
`2 )
= y2)
proof
assume
A1: z
in
[:X,
{y1, y2}:];
then (z
`2 )
in
{y1, y2} by
Th4;
hence thesis by
A1,
Th4,
TARSKI:def 2;
end;
theorem ::
MCART_1:17
z
in
[:
{x1, x2},
{y}:] implies ((z
`1 )
= x1 or (z
`1 )
= x2) & (z
`2 )
= y
proof
assume z
in
[:
{x1, x2},
{y}:];
then (z
`1 )
in
{x1, x2} & (z
`2 )
in
{y} by
Th4;
hence thesis by
TARSKI:def 1,
TARSKI:def 2;
end;
theorem ::
MCART_1:18
z
in
[:
{x},
{y1, y2}:] implies (z
`1 )
= x & ((z
`2 )
= y1 or (z
`2 )
= y2)
proof
assume z
in
[:
{x},
{y1, y2}:];
then (z
`1 )
in
{x} & (z
`2 )
in
{y1, y2} by
Th4;
hence thesis by
TARSKI:def 1,
TARSKI:def 2;
end;
theorem ::
MCART_1:19
z
in
[:
{x1, x2},
{y1, y2}:] implies ((z
`1 )
= x1 or (z
`1 )
= x2) & ((z
`2 )
= y1 or (z
`2 )
= y2)
proof
assume z
in
[:
{x1, x2},
{y1, y2}:];
then (z
`1 )
in
{x1, x2} & (z
`2 )
in
{y1, y2} by
Th4;
hence thesis by
TARSKI:def 2;
end;
theorem ::
MCART_1:20
Th14: (ex y, z st x
=
[y, z]) implies x
<> (x
`1 ) & x
<> (x
`2 )
proof
given y, z such that
A1: x
=
[y, z];
now
assume y
= x;
then
{
{y, z},
{y}}
in
{y} by
A1,
TARSKI:def 1;
hence contradiction by
TARSKI:def 2;
end;
hence x
<> (x
`1 ) by
A1;
now
assume z
= x;
then
{
{y, z},
{y}}
in
{y, z} by
A1,
TARSKI:def 2;
hence contradiction by
TARSKI:def 2;
end;
hence thesis by
A1;
end;
reserve R for
Relation;
theorem ::
MCART_1:21
Th15: x
in R implies x
=
[(x
`1 ), (x
`2 )]
proof
assume x
in R;
then ex x1,x2 be
object st x
=
[x1, x2] by
RELAT_1:def 1;
hence thesis;
end;
Lm1: X1
<>
{} & X2
<>
{} implies for x be
Element of
[:X1, X2:] holds ex xx1 be
Element of X1, xx2 be
Element of X2 st x
=
[xx1, xx2]
proof
assume
A1: X1
<>
{} & X2
<>
{} ;
let x be
Element of
[:X1, X2:];
reconsider xx2 = (x
`2 ) as
Element of X2 by
A1,
Th4;
reconsider xx1 = (x
`1 ) as
Element of X1 by
A1,
Th4;
take xx1, xx2;
thus thesis by
A1,
Th15;
end;
registration
let X1,X2 be non
empty
set;
cluster ->
pair for
Element of
[:X1, X2:];
coherence
proof
let x be
Element of
[:X1, X2:];
ex xx1 be
Element of X1, xx2 be
Element of X2 st x
=
[xx1, xx2] by
Lm1;
hence thesis;
end;
end
theorem ::
MCART_1:22
X
<>
{} & Y
<>
{} implies for x be
Element of
[:X, Y:] holds x
=
[(x
`1 ), (x
`2 )] by
Th15;
theorem ::
MCART_1:23
Th17:
[:
{x1, x2},
{y1, y2}:]
=
{
[x1, y1],
[x1, y2],
[x2, y1],
[x2, y2]}
proof
thus
[:
{x1, x2},
{y1, y2}:]
= (
[:
{x1},
{y1, y2}:]
\/
[:
{x2},
{y1, y2}:]) by
ZFMISC_1: 109
.= (
{
[x1, y1],
[x1, y2]}
\/
[:
{x2},
{y1, y2}:]) by
ZFMISC_1: 30
.= (
{
[x1, y1],
[x1, y2]}
\/
{
[x2, y1],
[x2, y2]}) by
ZFMISC_1: 30
.=
{
[x1, y1],
[x1, y2],
[x2, y1],
[x2, y2]} by
ENUMSET1: 5;
end;
theorem ::
MCART_1:24
Th18: X
<>
{} & Y
<>
{} implies for x be
Element of
[:X, Y:] holds x
<> (x
`1 ) & x
<> (x
`2 )
proof
assume
A1: X
<>
{} & Y
<>
{} ;
let x be
Element of
[:X, Y:];
x
=
[(x
`1 ), (x
`2 )] by
A1,
Th15;
hence thesis by
Th14;
end;
::$Canceled
theorem ::
MCART_1:26
Th19: X
<>
{} implies ex v st v
in X & not ex x, y, z st (x
in X or y
in X) & v
=
[x, y, z]
proof
assume X
<>
{} ;
then
consider Y such that
A1: Y
in X and
A2: not ex Y1, Y2, Y3 st Y1
in Y2 & Y2
in Y3 & Y3
in Y & not Y1
misses X by
XREGULAR: 4;
take v = Y;
thus v
in X by
A1;
given x, y, z such that
A3: x
in X or y
in X and
A4: v
=
[x, y, z];
set Y1 =
{x, y}, Y2 =
{Y1,
{x}}, Y3 =
{Y2, z};
A5: x
in Y1 & y
in Y1 by
TARSKI:def 2;
A6: Y3
in Y by
A4,
TARSKI:def 2;
Y1
in Y2 & Y2
in Y3 by
TARSKI:def 2;
hence contradiction by
A2,
A5,
A6,
A3,
XBOOLE_0: 3;
end;
::$Canceled
theorem ::
MCART_1:30
Th20: X
<>
{} implies ex v st v
in X & not ex x1, x2, x3, x4 st (x1
in X or x2
in X) & v
=
[x1, x2, x3, x4]
proof
assume X
<>
{} ;
then
consider Y such that
A1: Y
in X and
A2: for Y1, Y2, Y3, Y4, Y5 st Y1
in Y2 & Y2
in Y3 & Y3
in Y4 & Y4
in Y5 & Y5
in Y holds Y1
misses X by
XREGULAR: 6;
take v = Y;
thus v
in X by
A1;
given x1, x2, x3, x4 such that
A3: x1
in X or x2
in X and
A4: v
=
[x1, x2, x3, x4];
set Y1 =
{x1, x2}, Y2 =
{Y1,
{x1}}, Y3 =
{Y2, x3}, Y4 =
{Y3,
{Y2}}, Y5 =
{Y4, x4};
A5: Y3
in Y4 & Y4
in Y5 by
TARSKI:def 2;
A6: Y5
in Y by
A4,
TARSKI:def 2;
A7: x1
in Y1 & x2
in Y1 by
TARSKI:def 2;
Y1
in Y2 & Y2
in Y3 by
TARSKI:def 2;
hence contradiction by
A2,
A7,
A5,
A6,
A3,
XBOOLE_0: 3;
end;
theorem ::
MCART_1:31
Th21: X1
<>
{} & X2
<>
{} & X3
<>
{} iff
[:X1, X2, X3:]
<>
{}
proof
A1: X1
<>
{} & X2
<>
{} iff
[:X1, X2:]
<>
{} by
ZFMISC_1: 90;
[:
[:X1, X2:], X3:]
=
[:X1, X2, X3:] by
ZFMISC_1:def 3;
hence thesis by
A1,
ZFMISC_1: 90;
end;
reserve xx1 for
Element of X1,
xx2 for
Element of X2,
xx3 for
Element of X3;
theorem ::
MCART_1:32
Th22: X1
<>
{} & X2
<>
{} & X3
<>
{} implies (
[:X1, X2, X3:]
=
[:Y1, Y2, Y3:] implies X1
= Y1 & X2
= Y2 & X3
= Y3)
proof
A1:
[:X1, X2, X3:]
=
[:
[:X1, X2:], X3:] by
ZFMISC_1:def 3;
assume
A2: X1
<>
{} & X2
<>
{} ;
assume
A3: X3
<>
{} ;
assume
[:X1, X2, X3:]
=
[:Y1, Y2, Y3:];
then
A4:
[:
[:X1, X2:], X3:]
=
[:
[:Y1, Y2:], Y3:] by
A1,
ZFMISC_1:def 3;
then
[:X1, X2:]
=
[:Y1, Y2:] by
A2,
A3,
ZFMISC_1: 110;
hence thesis by
A2,
A3,
A4,
ZFMISC_1: 110;
end;
theorem ::
MCART_1:33
[:X1, X2, X3:]
<>
{} &
[:X1, X2, X3:]
=
[:Y1, Y2, Y3:] implies X1
= Y1 & X2
= Y2 & X3
= Y3
proof
assume
A1:
[:X1, X2, X3:]
<>
{} ;
then
A2: X3
<>
{} by
Th21;
X1
<>
{} & X2
<>
{} by
A1,
Th21;
hence thesis by
A2,
Th22;
end;
theorem ::
MCART_1:34
[:X, X, X:]
=
[:Y, Y, Y:] implies X
= Y
proof
assume
[:X, X, X:]
=
[:Y, Y, Y:];
then X
<>
{} or Y
<>
{} implies thesis by
Th22;
hence thesis;
end;
Lm2: X1
<>
{} & X2
<>
{} & X3
<>
{} implies for x be
Element of
[:X1, X2, X3:] holds ex xx1, xx2, xx3 st x
=
[xx1, xx2, xx3]
proof
assume that
A1: X1
<>
{} & X2
<>
{} and
A2: X3
<>
{} ;
let x be
Element of
[:X1, X2, X3:];
reconsider x9 = x as
Element of
[:
[:X1, X2:], X3:] by
ZFMISC_1:def 3;
consider x12 be
Element of
[:X1, X2:], xx3 such that
A3: x9
=
[x12, xx3] by
A1,
A2,
Lm1;
consider xx1, xx2 such that
A4: x12
=
[xx1, xx2] by
A1,
Lm1;
take xx1, xx2, xx3;
thus thesis by
A3,
A4;
end;
theorem ::
MCART_1:35
Th25:
[:
{x1},
{x2},
{x3}:]
=
{
[x1, x2, x3]}
proof
thus
[:
{x1},
{x2},
{x3}:]
=
[:
[:
{x1},
{x2}:],
{x3}:] by
ZFMISC_1:def 3
.=
[:
{
[x1, x2]},
{x3}:] by
ZFMISC_1: 29
.=
{
[x1, x2, x3]} by
ZFMISC_1: 29;
end;
theorem ::
MCART_1:36
[:
{x1, y1},
{x2},
{x3}:]
=
{
[x1, x2, x3],
[y1, x2, x3]}
proof
thus
[:
{x1, y1},
{x2},
{x3}:]
=
[:
[:
{x1, y1},
{x2}:],
{x3}:] by
ZFMISC_1:def 3
.=
[:
{
[x1, x2],
[y1, x2]},
{x3}:] by
ZFMISC_1: 30
.=
{
[x1, x2, x3],
[y1, x2, x3]} by
ZFMISC_1: 30;
end;
theorem ::
MCART_1:37
[:
{x1},
{x2, y2},
{x3}:]
=
{
[x1, x2, x3],
[x1, y2, x3]}
proof
thus
[:
{x1},
{x2, y2},
{x3}:]
=
[:
[:
{x1},
{x2, y2}:],
{x3}:] by
ZFMISC_1:def 3
.=
[:
{
[x1, x2],
[x1, y2]},
{x3}:] by
ZFMISC_1: 30
.=
{
[x1, x2, x3],
[x1, y2, x3]} by
ZFMISC_1: 30;
end;
theorem ::
MCART_1:38
[:
{x1},
{x2},
{x3, y3}:]
=
{
[x1, x2, x3],
[x1, x2, y3]}
proof
thus
[:
{x1},
{x2},
{x3, y3}:]
=
[:
[:
{x1},
{x2}:],
{x3, y3}:] by
ZFMISC_1:def 3
.=
[:
{
[x1, x2]},
{x3, y3}:] by
ZFMISC_1: 29
.=
{
[x1, x2, x3],
[x1, x2, y3]} by
ZFMISC_1: 30;
end;
theorem ::
MCART_1:39
[:
{x1, y1},
{x2, y2},
{x3}:]
=
{
[x1, x2, x3],
[y1, x2, x3],
[x1, y2, x3],
[y1, y2, x3]}
proof
thus
[:
{x1, y1},
{x2, y2},
{x3}:]
=
[:
[:
{x1, y1},
{x2, y2}:],
{x3}:] by
ZFMISC_1:def 3
.=
[:
{
[x1, x2],
[x1, y2],
[y1, x2],
[y1, y2]},
{x3}:] by
Th17
.=
[:(
{
[x1, x2],
[x1, y2]}
\/
{
[y1, x2],
[y1, y2]}),
{x3}:] by
ENUMSET1: 5
.= (
[:
{
[x1, x2],
[x1, y2]},
{x3}:]
\/
[:
{
[y1, x2],
[y1, y2]},
{x3}:]) by
ZFMISC_1: 97
.= (
{
[
[x1, x2], x3],
[
[x1, y2], x3]}
\/
[:
{
[y1, x2],
[y1, y2]},
{x3}:]) by
ZFMISC_1: 30
.= (
{
[
[x1, x2], x3],
[
[x1, y2], x3]}
\/
{
[
[y1, x2], x3],
[
[y1, y2], x3]}) by
ZFMISC_1: 30
.=
{
[x1, x2, x3],
[x1, y2, x3],
[y1, x2, x3],
[
[y1, y2], x3]} by
ENUMSET1: 5
.=
{
[x1, x2, x3],
[y1, x2, x3],
[x1, y2, x3],
[y1, y2, x3]} by
ENUMSET1: 62;
end;
theorem ::
MCART_1:40
[:
{x1, y1},
{x2},
{x3, y3}:]
=
{
[x1, x2, x3],
[y1, x2, x3],
[x1, x2, y3],
[y1, x2, y3]}
proof
thus
[:
{x1, y1},
{x2},
{x3, y3}:]
=
[:
[:
{x1, y1},
{x2}:],
{x3, y3}:] by
ZFMISC_1:def 3
.=
[:
{
[x1, x2],
[y1, x2]},
{x3, y3}:] by
ZFMISC_1: 30
.=
{
[
[x1, x2], x3],
[
[x1, x2], y3],
[
[y1, x2], x3],
[
[y1, x2], y3]} by
Th17
.=
{
[x1, x2, x3],
[y1, x2, x3],
[x1, x2, y3],
[y1, x2, y3]} by
ENUMSET1: 62;
end;
theorem ::
MCART_1:41
[:
{x1},
{x2, y2},
{x3, y3}:]
=
{
[x1, x2, x3],
[x1, y2, x3],
[x1, x2, y3],
[x1, y2, y3]}
proof
thus
[:
{x1},
{x2, y2},
{x3, y3}:]
=
[:
[:
{x1},
{x2, y2}:],
{x3, y3}:] by
ZFMISC_1:def 3
.=
[:
{
[x1, x2],
[x1, y2]},
{x3, y3}:] by
ZFMISC_1: 30
.=
{
[
[x1, x2], x3],
[
[x1, x2], y3],
[
[x1, y2], x3],
[
[x1, y2], y3]} by
Th17
.=
{
[x1, x2, x3],
[x1, y2, x3],
[x1, x2, y3],
[x1, y2, y3]} by
ENUMSET1: 62;
end;
theorem ::
MCART_1:42
[:
{x1, y1},
{x2, y2},
{x3, y3}:]
=
{
[x1, x2, x3],
[x1, y2, x3],
[x1, x2, y3],
[x1, y2, y3],
[y1, x2, x3],
[y1, y2, x3],
[y1, x2, y3],
[y1, y2, y3]}
proof
A1:
[:
{
[x1, x2],
[x1, y2]},
{x3, y3}:]
=
{
[
[x1, x2], x3],
[
[x1, x2], y3],
[
[x1, y2], x3],
[
[x1, y2], y3]} by
Th17
.=
{
[x1, x2, x3],
[x1, y2, x3],
[x1, x2, y3],
[x1, y2, y3]} by
ENUMSET1: 62;
A2:
[:
{
[y1, x2],
[y1, y2]},
{x3, y3}:]
=
{
[
[y1, x2], x3],
[
[y1, x2], y3],
[
[y1, y2], x3],
[
[y1, y2], y3]} by
Th17
.=
{
[y1, x2, x3],
[y1, y2, x3],
[y1, x2, y3],
[y1, y2, y3]} by
ENUMSET1: 62;
thus
[:
{x1, y1},
{x2, y2},
{x3, y3}:]
=
[:
[:
{x1, y1},
{x2, y2}:],
{x3, y3}:] by
ZFMISC_1:def 3
.=
[:
{
[x1, x2],
[x1, y2],
[y1, x2],
[y1, y2]},
{x3, y3}:] by
Th17
.=
[:(
{
[x1, x2],
[x1, y2]}
\/
{
[y1, x2],
[y1, y2]}),
{x3, y3}:] by
ENUMSET1: 5
.= (
{
[x1, x2, x3],
[x1, y2, x3],
[x1, x2, y3],
[x1, y2, y3]}
\/
{
[y1, x2, x3],
[y1, y2, x3],
[y1, x2, y3],
[y1, y2, y3]}) by
A1,
A2,
ZFMISC_1: 97
.=
{
[x1, x2, x3],
[x1, y2, x3],
[x1, x2, y3],
[x1, y2, y3],
[y1, x2, x3],
[y1, y2, x3],
[y1, x2, y3],
[y1, y2, y3]} by
ENUMSET1: 25;
end;
registration
let X1,X2,X3 be non
empty
set;
cluster ->
triple for
Element of
[:X1, X2, X3:];
coherence
proof
let x be
Element of
[:X1, X2, X3:];
ex xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3 st x
=
[xx1, xx2, xx3] by
Lm2;
hence thesis;
end;
end
definition
::$Canceled
let X1,X2,X3 be non
empty
set;
let x be
Element of
[:X1, X2, X3:];
:: original:
`1_3
redefine
::
MCART_1:def5
func x
`1_3 ->
Element of X1 means x
=
[x1, x2, x3] implies it
= x1;
coherence
proof
consider xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3 such that
A1: x
=
[xx1, xx2, xx3] by
Lm2;
thus (x
`1_3 ) is
Element of X1 by
A1;
end;
compatibility
proof
let y be
Element of X1;
thus y
= (x
`1_3 ) implies for x1, x2, x3 holds x
=
[x1, x2, x3] implies y
= x1;
assume
A2: for x1, x2, x3 holds x
=
[x1, x2, x3] implies y
= x1;
consider xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3 such that
A3: x
=
[xx1, xx2, xx3] by
Lm2;
thus y
= (x
`1_3 ) by
A2,
A3;
end;
:: original:
`2_3
redefine
::
MCART_1:def6
func x
`2_3 ->
Element of X2 means x
=
[x1, x2, x3] implies it
= x2;
coherence
proof
consider xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3 such that
A4: x
=
[xx1, xx2, xx3] by
Lm2;
thus (x
`2_3 ) is
Element of X2 by
A4;
end;
compatibility
proof
let y be
Element of X2;
thus y
= (x
`2_3 ) implies for x1, x2, x3 holds x
=
[x1, x2, x3] implies y
= x2;
assume
A5: for x1, x2, x3 holds x
=
[x1, x2, x3] implies y
= x2;
consider xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3 such that
A6: x
=
[xx1, xx2, xx3] by
Lm2;
thus y
= (x
`2_3 ) by
A5,
A6;
end;
:: original:
`3_3
redefine
::
MCART_1:def7
func x
`3_3 ->
Element of X3 means x
=
[x1, x2, x3] implies it
= x3;
coherence
proof
consider xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3 such that
A7: x
=
[xx1, xx2, xx3] by
Lm2;
thus (x
`3_3 ) is
Element of X3 by
A7;
end;
compatibility
proof
let y be
Element of X3;
thus y
= (x
`3_3 ) implies for x1, x2, x3 holds x
=
[x1, x2, x3] implies y
= x3;
assume
A8: for x1, x2, x3 holds x
=
[x1, x2, x3] implies y
= x3;
consider xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3 such that
A9: x
=
[xx1, xx2, xx3] by
Lm2;
thus y
= (x
`3_3 ) by
A8,
A9;
end;
end
::$Canceled
theorem ::
MCART_1:45
Th34: X
c=
[:X, Y, Z:] or X
c=
[:Y, Z, X:] or X
c=
[:Z, X, Y:] implies X
=
{}
proof
assume that
A1: X
c=
[:X, Y, Z:] or X
c=
[:Y, Z, X:] or X
c=
[:Z, X, Y:] and
A2: X
<>
{} ;
[:X, Y, Z:]
<>
{} or
[:Y, Z, X:]
<>
{} or
[:Z, X, Y:]
<>
{} by
A1,
A2;
then
reconsider X, Y, Z as non
empty
set by
Th21;
per cases by
A1;
suppose
A3: X
c=
[:X, Y, Z:];
consider v such that
A4: v
in X and
A5: for x, y, z st x
in X or y
in X holds v
<>
[x, y, z] by
Th19;
reconsider v as
Element of
[:X, Y, Z:] by
A3,
A4;
v
=
[(v
`1_3 ), (v
`2_3 ), (v
`3_3 )];
hence contradiction by
A5;
end;
suppose X
c=
[:Y, Z, X:];
then X
c=
[:
[:Y, Z:], X:] by
ZFMISC_1:def 3;
hence thesis by
ZFMISC_1: 111;
end;
suppose
A6: X
c=
[:Z, X, Y:];
consider v such that
A7: v
in X and
A8: for z, x, y st z
in X or x
in X holds v
<>
[z, x, y] by
Th19;
reconsider v as
Element of
[:Z, X, Y:] by
A6,
A7;
v
=
[(v
`1_3 ), (v
`2_3 ), (v
`3_3 )];
hence thesis by
A8;
end;
end;
::$Canceled
theorem ::
MCART_1:47
Th35: for X1,X2,X3 be non
empty
set holds for x be
Element of
[:X1, X2, X3:] holds x
<> (x
`1_3 ) & x
<> (x
`2_3 ) & x
<> (x
`3_3 )
proof
let X1,X2,X3 be non
empty
set;
let x be
Element of
[:X1, X2, X3:];
set Y9 =
{(x
`1_3 ), (x
`2_3 )}, Y =
{Y9,
{(x
`1_3 )}}, X9 =
{Y, (x
`3_3 )}, X =
{X9,
{Y}};
A1: x
=
[(x
`1_3 ), (x
`2_3 ), (x
`3_3 )]
.=
[
[(x
`1_3 ), (x
`2_3 )], (x
`3_3 )];
then x
= (x
`1_3 ) or x
= (x
`2_3 ) implies X
in Y9 & Y9
in Y & Y
in X9 & X9
in X by
TARSKI:def 2;
hence x
<> (x
`1_3 ) & x
<> (x
`2_3 ) by
XREGULAR: 8;
thus thesis by
A1,
Th14;
end;
theorem ::
MCART_1:48
[:X1, X2, X3:]
meets
[:Y1, Y2, Y3:] implies X1
meets Y1 & X2
meets Y2 & X3
meets Y3
proof
assume
A1:
[:X1, X2, X3:]
meets
[:Y1, Y2, Y3:];
A2:
[:
[:X1, X2:], X3:]
=
[:X1, X2, X3:] &
[:
[:Y1, Y2:], Y3:]
=
[:Y1, Y2, Y3:] by
ZFMISC_1:def 3;
then
[:X1, X2:]
meets
[:Y1, Y2:] by
A1,
ZFMISC_1: 104;
hence thesis by
A2,
A1,
ZFMISC_1: 104;
end;
theorem ::
MCART_1:49
Th37:
[:X1, X2, X3, X4:]
=
[:
[:
[:X1, X2:], X3:], X4:]
proof
thus
[:X1, X2, X3, X4:]
=
[:
[:X1, X2, X3:], X4:] by
ZFMISC_1:def 4
.=
[:
[:
[:X1, X2:], X3:], X4:] by
ZFMISC_1:def 3;
end;
theorem ::
MCART_1:50
Th38:
[:
[:X1, X2:], X3, X4:]
=
[:X1, X2, X3, X4:]
proof
thus
[:
[:X1, X2:], X3, X4:]
=
[:
[:
[:X1, X2:], X3:], X4:] by
ZFMISC_1:def 3
.=
[:X1, X2, X3, X4:] by
Th37;
end;
theorem ::
MCART_1:51
Th39: X1
<>
{} & X2
<>
{} & X3
<>
{} & X4
<>
{} iff
[:X1, X2, X3, X4:]
<>
{}
proof
A1:
[:
[:X1, X2, X3:], X4:]
=
[:X1, X2, X3, X4:] by
ZFMISC_1:def 4;
X1
<>
{} & X2
<>
{} & X3
<>
{} iff
[:X1, X2, X3:]
<>
{} by
Th21;
hence thesis by
A1,
ZFMISC_1: 90;
end;
theorem ::
MCART_1:52
Th40: X1
<>
{} & X2
<>
{} & X3
<>
{} & X4
<>
{} &
[:X1, X2, X3, X4:]
=
[:Y1, Y2, Y3, Y4:] implies X1
= Y1 & X2
= Y2 & X3
= Y3 & X4
= Y4
proof
A1:
[:X1, X2, X3, X4:]
=
[:
[:X1, X2, X3:], X4:] by
ZFMISC_1:def 4;
assume
A2: X1
<>
{} & X2
<>
{} & X3
<>
{} ;
assume
A3: X4
<>
{} ;
assume
[:X1, X2, X3, X4:]
=
[:Y1, Y2, Y3, Y4:];
then
A4:
[:
[:X1, X2, X3:], X4:]
=
[:
[:Y1, Y2, Y3:], Y4:] by
A1,
ZFMISC_1:def 4;
[:X1, X2, X3:]
=
[:Y1, Y2, Y3:] by
A3,
A4,
A2,
ZFMISC_1: 110;
hence thesis by
A2,
A3,
A4,
Th22,
ZFMISC_1: 110;
end;
theorem ::
MCART_1:53
[:X1, X2, X3, X4:]
<>
{} &
[:X1, X2, X3, X4:]
=
[:Y1, Y2, Y3, Y4:] implies X1
= Y1 & X2
= Y2 & X3
= Y3 & X4
= Y4
proof
assume
A1:
[:X1, X2, X3, X4:]
<>
{} ;
then
A2: X3
<>
{} & X4
<>
{} by
Th39;
X1
<>
{} & X2
<>
{} by
A1,
Th39;
hence thesis by
A2,
Th40;
end;
theorem ::
MCART_1:54
[:X, X, X, X:]
=
[:Y, Y, Y, Y:] implies X
= Y
proof
assume
[:X, X, X, X:]
=
[:Y, Y, Y, Y:];
then X
<>
{} or Y
<>
{} implies thesis by
Th40;
hence thesis;
end;
reserve xx4 for
Element of X4;
Lm3: X1
<>
{} & X2
<>
{} & X3
<>
{} & X4
<>
{} implies for x be
Element of
[:X1, X2, X3, X4:] holds ex xx1, xx2, xx3, xx4 st x
=
[xx1, xx2, xx3, xx4]
proof
assume that
A1: X1
<>
{} & X2
<>
{} & X3
<>
{} and
A2: X4
<>
{} ;
let x be
Element of
[:X1, X2, X3, X4:];
reconsider x9 = x as
Element of
[:
[:X1, X2, X3:], X4:] by
ZFMISC_1:def 4;
consider x123 be
Element of
[:X1, X2, X3:], xx4 such that
A3: x9
=
[x123, xx4] by
A2,
Lm1,
A1;
consider xx1, xx2, xx3 such that
A4: x123
=
[xx1, xx2, xx3] by
A1,
Lm2;
take xx1, xx2, xx3, xx4;
thus thesis by
A3,
A4;
end;
registration
let X1,X2,X3,X4 be non
empty
set;
cluster ->
quadruple for
Element of
[:X1, X2, X3, X4:];
coherence
proof
let x be
Element of
[:X1, X2, X3, X4:];
ex xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3, xx4 be
Element of X4 st x
=
[xx1, xx2, xx3, xx4] by
Lm3;
hence thesis;
end;
end
definition
let X1,X2,X3,X4 be non
empty
set;
let x be
Element of
[:X1, X2, X3, X4:];
:: original:
`1_4
redefine
::
MCART_1:def8
func x
`1_4 ->
Element of X1 means x
=
[x1, x2, x3, x4] implies it
= x1;
coherence
proof
consider xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3, xx4 be
Element of X4 such that
A1: x
=
[xx1, xx2, xx3, xx4] by
Lm3;
thus (x
`1_4 ) is
Element of X1 by
A1;
end;
compatibility
proof
let y be
Element of X1;
thus y
= (x
`1_4 ) implies for x1, x2, x3, x4 holds x
=
[x1, x2, x3, x4] implies y
= x1;
assume
A2: for x1, x2, x3, x4 holds x
=
[x1, x2, x3, x4] implies y
= x1;
consider xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3, xx4 be
Element of X4 such that
A3: x
=
[xx1, xx2, xx3, xx4] by
Lm3;
thus y
= (x
`1_4 ) by
A2,
A3;
end;
:: original:
`2_4
redefine
::
MCART_1:def9
func x
`2_4 ->
Element of X2 means x
=
[x1, x2, x3, x4] implies it
= x2;
coherence
proof
consider xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3, xx4 be
Element of X4 such that
A4: x
=
[xx1, xx2, xx3, xx4] by
Lm3;
thus (x
`2_4 ) is
Element of X2 by
A4;
end;
compatibility
proof
let y be
Element of X2;
thus y
= (x
`2_4 ) implies for x1, x2, x3, x4 holds x
=
[x1, x2, x3, x4] implies y
= x2;
assume
A5: for x1, x2, x3, x4 holds x
=
[x1, x2, x3, x4] implies y
= x2;
consider xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3, xx4 be
Element of X4 such that
A6: x
=
[xx1, xx2, xx3, xx4] by
Lm3;
thus y
= (x
`2_4 ) by
A5,
A6;
end;
:: original:
`3_4
redefine
::
MCART_1:def10
func x
`3_4 ->
Element of X3 means x
=
[x1, x2, x3, x4] implies it
= x3;
coherence
proof
consider xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3, xx4 be
Element of X4 such that
A7: x
=
[xx1, xx2, xx3, xx4] by
Lm3;
thus (x
`3_4 ) is
Element of X3 by
A7;
end;
compatibility
proof
let y be
Element of X3;
thus y
= (x
`3_4 ) implies for x1, x2, x3, x4 holds x
=
[x1, x2, x3, x4] implies y
= x3;
assume
A8: for x1, x2, x3, x4 holds x
=
[x1, x2, x3, x4] implies y
= x3;
consider xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3, xx4 be
Element of X4 such that
A9: x
=
[xx1, xx2, xx3, xx4] by
Lm3;
thus y
= (x
`3_4 ) by
A8,
A9;
end;
:: original:
`4_4
redefine
::
MCART_1:def11
func x
`4_4 ->
Element of X4 means x
=
[x1, x2, x3, x4] implies it
= x4;
coherence
proof
consider xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3, xx4 be
Element of X4 such that
A10: x
=
[xx1, xx2, xx3, xx4] by
Lm3;
thus (x
`4_4 ) is
Element of X4 by
A10;
end;
compatibility
proof
let y be
Element of X4;
thus y
= (x
`4_4 ) implies for x1, x2, x3, x4 holds x
=
[x1, x2, x3, x4] implies y
= x4;
assume
A11: for x1, x2, x3, x4 holds x
=
[x1, x2, x3, x4] implies y
= x4;
consider xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3, xx4 be
Element of X4 such that
A12: x
=
[xx1, xx2, xx3, xx4] by
Lm3;
thus y
= (x
`4_4 ) by
A11,
A12;
end;
end
::$Canceled
theorem ::
MCART_1:58
for X1,X2,X3,X4 be non
empty
set holds for x be
Element of
[:X1, X2, X3, X4:] holds x
<> (x
`1_4 ) & x
<> (x
`2_4 ) & x
<> (x
`3_4 ) & x
<> (x
`4_4 )
proof
let X1,X2,X3,X4 be non
empty
set;
let x be
Element of
[:X1, X2, X3, X4:];
reconsider Y =
[:X1, X2:], X3, X4 as non
empty
set;
reconsider x9 = x as
Element of
[:Y, X3, X4:] by
Th38;
set Z9 =
{(x
`1_4 ), (x
`2_4 )}, Z =
{Z9,
{(x
`1_4 )}}, Y9 =
{Z, (x
`3_4 )}, Y =
{Y9,
{Z}}, X9 =
{Y, (x
`4_4 )}, X =
{X9,
{Y}};
x
=
[(x
`1_4 ), (x
`2_4 ), (x
`3_4 ), (x
`4_4 )]
.= X;
then x
= (x
`1_4 ) or x
= (x
`2_4 ) implies X
in Z9 & Z9
in Z & Z
in Y9 & Y9
in Y & Y
in X9 & X9
in X by
TARSKI:def 2;
hence x
<> (x
`1_4 ) & x
<> (x
`2_4 ) by
XREGULAR: 10;
(x
`3_4 )
= ((x qua
set
`1 )
`2 )
.= (x9
`2_3 );
hence thesis by
Th35;
end;
theorem ::
MCART_1:59
X1
c=
[:X1, X2, X3, X4:] or X1
c=
[:X2, X3, X4, X1:] or X1
c=
[:X3, X4, X1, X2:] or X1
c=
[:X4, X1, X2, X3:] implies X1
=
{}
proof
assume that
A1: X1
c=
[:X1, X2, X3, X4:] or X1
c=
[:X2, X3, X4, X1:] or X1
c=
[:X3, X4, X1, X2:] or X1
c=
[:X4, X1, X2, X3:] and
A2: X1
<>
{} ;
A3:
[:X1, X2, X3, X4:]
<>
{} or
[:X2, X3, X4, X1:]
<>
{} or
[:X3, X4, X1, X2:]
<>
{} or
[:X4, X1, X2, X3:]
<>
{} by
A1,
A2;
reconsider X1, X2, X3, X4 as non
empty
set by
A3,
Th39;
per cases by
A1;
suppose
A4: X1
c=
[:X1, X2, X3, X4:];
consider v such that
A5: v
in X1 and
A6: for x1, x2, x3, x4 st x1
in X1 or x2
in X1 holds v
<>
[x1, x2, x3, x4] by
Th20;
reconsider v as
Element of
[:X1, X2, X3, X4:] by
A4,
A5;
v
=
[(v
`1_4 ), (v
`2_4 ), (v
`3_4 ), (v
`4_4 )];
hence contradiction by
A6;
end;
suppose X1
c=
[:X2, X3, X4, X1:];
then X1
c=
[:
[:X2, X3:], X4, X1:] by
Th38;
hence thesis by
Th34;
end;
suppose X1
c=
[:X3, X4, X1, X2:];
then X1
c=
[:
[:X3, X4:], X1, X2:] by
Th38;
hence thesis by
Th34;
end;
suppose
A7: X1
c=
[:X4, X1, X2, X3:];
consider v such that
A8: v
in X1 and
A9: for x1, x2, x3, x4 st x1
in X1 or x2
in X1 holds v
<>
[x1, x2, x3, x4] by
Th20;
reconsider v as
Element of
[:X4, X1, X2, X3:] by
A7,
A8;
v
=
[(v
`1_4 ), (v
`2_4 ), (v
`3_4 ), (v
`4_4 )];
hence thesis by
A9;
end;
end;
theorem ::
MCART_1:60
[:X1, X2, X3, X4:]
meets
[:Y1, Y2, Y3, Y4:] implies X1
meets Y1 & X2
meets Y2 & X3
meets Y3 & X4
meets Y4
proof
assume
A1:
[:X1, X2, X3, X4:]
meets
[:Y1, Y2, Y3, Y4:];
A2:
[:
[:
[:X1, X2:], X3:], X4:]
=
[:X1, X2, X3, X4:] &
[:
[:
[:Y1, Y2:], Y3:], Y4:]
=
[:Y1, Y2, Y3, Y4:] by
Th37;
then
A3:
[:
[:X1, X2:], X3:]
meets
[:
[:Y1, Y2:], Y3:] by
A1,
ZFMISC_1: 104;
then
[:X1, X2:]
meets
[:Y1, Y2:] by
ZFMISC_1: 104;
hence thesis by
A2,
A1,
A3,
ZFMISC_1: 104;
end;
theorem ::
MCART_1:61
[:
{x1},
{x2},
{x3},
{x4}:]
=
{
[x1, x2, x3, x4]}
proof
thus
[:
{x1},
{x2},
{x3},
{x4}:]
=
[:
[:
{x1},
{x2}:],
{x3},
{x4}:] by
Th38
.=
[:
{
[x1, x2]},
{x3},
{x4}:] by
ZFMISC_1: 29
.=
{
[
[x1, x2], x3, x4]} by
Th25
.=
{
[x1, x2, x3, x4]};
end;
theorem ::
MCART_1:62
Th48:
[:X, Y:]
<>
{} implies for x be
Element of
[:X, Y:] holds x
<> (x
`1 ) & x
<> (x
`2 )
proof
assume
[:X, Y:]
<>
{} ;
then X
<>
{} & Y
<>
{} by
ZFMISC_1: 90;
hence thesis by
Th18;
end;
theorem ::
MCART_1:63
x
in
[:X, Y:] implies x
<> (x
`1 ) & x
<> (x
`2 ) by
Th48;
reserve A1 for
Subset of X1,
A2 for
Subset of X2,
A3 for
Subset of X3,
A4 for
Subset of X4;
reserve x for
Element of
[:X1, X2, X3:];
theorem ::
MCART_1:64
for X1,X2,X3 be non
empty
set holds for x be
Element of
[:X1, X2, X3:] holds for x1, x2, x3 st x
=
[x1, x2, x3] holds (x
`1_3 )
= x1 & (x
`2_3 )
= x2 & (x
`3_3 )
= x3;
theorem ::
MCART_1:65
for X1,X2,X3 be non
empty
set holds for x be
Element of
[:X1, X2, X3:] st for xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3 st x
=
[xx1, xx2, xx3] holds y1
= xx1 holds y1
= (x
`1_3 )
proof
let X1,X2,X3 be non
empty
set;
let x be
Element of
[:X1, X2, X3:];
assume that
A1: for xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3 st x
=
[xx1, xx2, xx3] holds y1
= xx1;
x
=
[(x
`1_3 ), (x
`2_3 ), (x
`3_3 )];
hence thesis by
A1;
end;
theorem ::
MCART_1:66
for X1,X2,X3 be non
empty
set holds for x be
Element of
[:X1, X2, X3:] st for xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3 st x
=
[xx1, xx2, xx3] holds y2
= xx2 holds y2
= (x
`2_3 )
proof
let X1,X2,X3 be non
empty
set;
let x be
Element of
[:X1, X2, X3:];
assume that
A1: for xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3 st x
=
[xx1, xx2, xx3] holds y2
= xx2;
x
=
[(x
`1_3 ), (x
`2_3 ), (x
`3_3 )];
hence thesis by
A1;
end;
theorem ::
MCART_1:67
for X1,X2,X3 be non
empty
set holds for x be
Element of
[:X1, X2, X3:] st for xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3 st x
=
[xx1, xx2, xx3] holds y3
= xx3 holds y3
= (x
`3_3 )
proof
let X1,X2,X3 be non
empty
set;
let x be
Element of
[:X1, X2, X3:];
assume that
A1: for xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3 st x
=
[xx1, xx2, xx3] holds y3
= xx3;
x
=
[(x
`1_3 ), (x
`2_3 ), (x
`3_3 )];
hence thesis by
A1;
end;
theorem ::
MCART_1:68
Th54: z
in
[:X1, X2, X3:] implies ex x1, x2, x3 st x1
in X1 & x2
in X2 & x3
in X3 & z
=
[x1, x2, x3]
proof
assume z
in
[:X1, X2, X3:];
then z
in
[:
[:X1, X2:], X3:] by
ZFMISC_1:def 3;
then
consider x12,x3 be
object such that
A1: x12
in
[:X1, X2:] and
A2: x3
in X3 and
A3: z
=
[x12, x3] by
ZFMISC_1:def 2;
consider x1,x2 be
object such that
A4: x1
in X1 & x2
in X2 and
A5: x12
=
[x1, x2] by
A1,
ZFMISC_1:def 2;
z
=
[x1, x2, x3] by
A3,
A5;
hence thesis by
A2,
A4;
end;
theorem ::
MCART_1:69
Th55:
[x1, x2, x3]
in
[:X1, X2, X3:] iff x1
in X1 & x2
in X2 & x3
in X3
proof
A1:
[x1, x2]
in
[:X1, X2:] iff x1
in X1 & x2
in X2 by
ZFMISC_1: 87;
[:X1, X2, X3:]
=
[:
[:X1, X2:], X3:] by
ZFMISC_1:def 3;
hence thesis by
A1,
ZFMISC_1: 87;
end;
theorem ::
MCART_1:70
(for z holds z
in Z iff ex x1, x2, x3 st x1
in X1 & x2
in X2 & x3
in X3 & z
=
[x1, x2, x3]) implies Z
=
[:X1, X2, X3:]
proof
assume
A1: for z holds z
in Z iff ex x1, x2, x3 st x1
in X1 & x2
in X2 & x3
in X3 & z
=
[x1, x2, x3];
now
let z be
object;
thus z
in Z implies z
in
[:
[:X1, X2:], X3:]
proof
assume z
in Z;
then
consider x1, x2, x3 such that
A2: x1
in X1 & x2
in X2 and
A3: x3
in X3 & z
=
[x1, x2, x3] by
A1;
[x1, x2]
in
[:X1, X2:] by
A2,
ZFMISC_1:def 2;
hence thesis by
A3,
ZFMISC_1:def 2;
end;
assume z
in
[:
[:X1, X2:], X3:];
then
consider x12,x3 be
object such that
A4: x12
in
[:X1, X2:] and
A5: x3
in X3 and
A6: z
=
[x12, x3] by
ZFMISC_1:def 2;
consider x1,x2 be
object such that
A7: x1
in X1 & x2
in X2 and
A8: x12
=
[x1, x2] by
A4,
ZFMISC_1:def 2;
z
=
[x1, x2, x3] by
A6,
A8;
hence z
in Z by
A1,
A5,
A7;
end;
then Z
=
[:
[:X1, X2:], X3:] by
TARSKI: 2;
hence thesis by
ZFMISC_1:def 3;
end;
::$Canceled
theorem ::
MCART_1:72
for X1,X2,X3 be non
empty
set holds for A1 be non
empty
Subset of X1, A2 be non
empty
Subset of X2, A3 be non
empty
Subset of X3 holds for x be
Element of
[:X1, X2, X3:] st x
in
[:A1, A2, A3:] holds (x
`1_3 )
in A1 & (x
`2_3 )
in A2 & (x
`3_3 )
in A3
proof
let X1,X2,X3 be non
empty
set;
let A1 be non
empty
Subset of X1, A2 be non
empty
Subset of X2, A3 be non
empty
Subset of X3;
let x be
Element of
[:X1, X2, X3:];
assume x
in
[:A1, A2, A3:];
then
reconsider y = x as
Element of
[:A1, A2, A3:];
A1: (y
`2_3 )
in A2;
A2: (y
`3_3 )
in A3;
(y
`1_3 )
in A1;
hence thesis by
A1,
A2;
end;
theorem ::
MCART_1:73
Th58: X1
c= Y1 & X2
c= Y2 & X3
c= Y3 implies
[:X1, X2, X3:]
c=
[:Y1, Y2, Y3:]
proof
A1:
[:X1, X2, X3:]
=
[:
[:X1, X2:], X3:] &
[:Y1, Y2, Y3:]
=
[:
[:Y1, Y2:], Y3:] by
ZFMISC_1:def 3;
assume X1
c= Y1 & X2
c= Y2;
then
A2:
[:X1, X2:]
c=
[:Y1, Y2:] by
ZFMISC_1: 96;
assume X3
c= Y3;
hence thesis by
A2,
A1,
ZFMISC_1: 96;
end;
reserve x for
Element of
[:X1, X2, X3, X4:];
theorem ::
MCART_1:74
for X1,X2,X3,X4 be non
empty
set holds for x be
Element of
[:X1, X2, X3, X4:] holds for x1,x2,x3,x4 be
set st x
=
[x1, x2, x3, x4] holds (x
`1_4 )
= x1 & (x
`2_4 )
= x2 & (x
`3_4 )
= x3 & (x
`4_4 )
= x4;
theorem ::
MCART_1:75
for X1,X2,X3,X4 be non
empty
set holds for x be
Element of
[:X1, X2, X3, X4:] st for xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3, xx4 be
Element of X4 st x
=
[xx1, xx2, xx3, xx4] holds y1
= xx1 holds y1
= (x
`1_4 )
proof
let X1,X2,X3,X4 be non
empty
set;
let x be
Element of
[:X1, X2, X3, X4:];
assume that
A1: for xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3, xx4 be
Element of X4 st x
=
[xx1, xx2, xx3, xx4] holds y1
= xx1;
x
=
[(x
`1_4 ), (x
`2_4 ), (x
`3_4 ), (x
`4_4 )];
hence thesis by
A1;
end;
theorem ::
MCART_1:76
for X1,X2,X3,X4 be non
empty
set holds for x be
Element of
[:X1, X2, X3, X4:] st for xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3, xx4 be
Element of X4 st x
=
[xx1, xx2, xx3, xx4] holds y2
= xx2 holds y2
= (x
`2_4 )
proof
let X1,X2,X3,X4 be non
empty
set;
let x be
Element of
[:X1, X2, X3, X4:];
assume that
A1: for xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3, xx4 be
Element of X4 st x
=
[xx1, xx2, xx3, xx4] holds y2
= xx2;
x
=
[(x
`1_4 ), (x
`2_4 ), (x
`3_4 ), (x
`4_4 )];
hence thesis by
A1;
end;
theorem ::
MCART_1:77
for X1,X2,X3,X4 be non
empty
set holds for x be
Element of
[:X1, X2, X3, X4:] st for xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3, xx4 be
Element of X4 st x
=
[xx1, xx2, xx3, xx4] holds y3
= xx3 holds y3
= (x
`3_4 )
proof
let X1,X2,X3,X4 be non
empty
set;
let x be
Element of
[:X1, X2, X3, X4:];
assume that
A1: for xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3, xx4 be
Element of X4 st x
=
[xx1, xx2, xx3, xx4] holds y3
= xx3;
x
=
[(x
`1_4 ), (x
`2_4 ), (x
`3_4 ), (x
`4_4 )];
hence thesis by
A1;
end;
theorem ::
MCART_1:78
for X1,X2,X3,X4 be non
empty
set holds for x be
Element of
[:X1, X2, X3, X4:] st for xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3, xx4 be
Element of X4 st x
=
[xx1, xx2, xx3, xx4] holds y4
= xx4 holds y4
= (x
`4_4 )
proof
let X1,X2,X3,X4 be non
empty
set;
let x be
Element of
[:X1, X2, X3, X4:];
assume that
A1: for xx1 be
Element of X1, xx2 be
Element of X2, xx3 be
Element of X3, xx4 be
Element of X4 st x
=
[xx1, xx2, xx3, xx4] holds y4
= xx4;
x
=
[(x
`1_4 ), (x
`2_4 ), (x
`3_4 ), (x
`4_4 )];
hence thesis by
A1;
end;
theorem ::
MCART_1:79
z
in
[:X1, X2, X3, X4:] implies ex x1, x2, x3, x4 st x1
in X1 & x2
in X2 & x3
in X3 & x4
in X4 & z
=
[x1, x2, x3, x4]
proof
assume z
in
[:X1, X2, X3, X4:];
then z
in
[:
[:X1, X2, X3:], X4:] by
ZFMISC_1:def 4;
then
consider x123,x4 be
object such that
A1: x123
in
[:X1, X2, X3:] and
A2: x4
in X4 and
A3: z
=
[x123, x4] by
ZFMISC_1:def 2;
consider x1, x2, x3 such that
A4: x1
in X1 & x2
in X2 & x3
in X3 and
A5: x123
=
[x1, x2, x3] by
A1,
Th54;
z
=
[x1, x2, x3, x4] by
A3,
A5;
hence thesis by
A2,
A4;
end;
theorem ::
MCART_1:80
[x1, x2, x3, x4]
in
[:X1, X2, X3, X4:] iff x1
in X1 & x2
in X2 & x3
in X3 & x4
in X4
proof
A1:
[x1, x2]
in
[:X1, X2:] iff x1
in X1 & x2
in X2 by
ZFMISC_1: 87;
[:X1, X2, X3, X4:]
=
[:
[:X1, X2:], X3, X4:] &
[x1, x2, x3, x4]
=
[
[x1, x2], x3, x4] by
Th38;
hence thesis by
A1,
Th55;
end;
theorem ::
MCART_1:81
(for z holds z
in Z iff ex x1, x2, x3, x4 st x1
in X1 & x2
in X2 & x3
in X3 & x4
in X4 & z
=
[x1, x2, x3, x4]) implies Z
=
[:X1, X2, X3, X4:]
proof
assume
A1: for z holds z
in Z iff ex x1, x2, x3, x4 st x1
in X1 & x2
in X2 & x3
in X3 & x4
in X4 & z
=
[x1, x2, x3, x4];
now
let z be
object;
thus z
in Z implies z
in
[:
[:X1, X2, X3:], X4:]
proof
assume z
in Z;
then
consider x1, x2, x3, x4 such that
A2: x1
in X1 & x2
in X2 & x3
in X3 and
A3: x4
in X4 & z
=
[x1, x2, x3, x4] by
A1;
[x1, x2, x3]
in
[:X1, X2, X3:] by
A2,
Th55;
hence thesis by
A3,
ZFMISC_1:def 2;
end;
assume z
in
[:
[:X1, X2, X3:], X4:];
then
consider x123,x4 be
object such that
A4: x123
in
[:X1, X2, X3:] and
A5: x4
in X4 and
A6: z
=
[x123, x4] by
ZFMISC_1:def 2;
consider x1, x2, x3 such that
A7: x1
in X1 & x2
in X2 & x3
in X3 and
A8: x123
=
[x1, x2, x3] by
A4,
Th54;
z
=
[x1, x2, x3, x4] by
A6,
A8;
hence z
in Z by
A1,
A5,
A7;
end;
then Z
=
[:
[:X1, X2, X3:], X4:] by
TARSKI: 2;
hence thesis by
ZFMISC_1:def 4;
end;
::$Canceled
theorem ::
MCART_1:83
for X1,X2,X3,X4 be non
empty
set, A1 be non
empty
Subset of X1, A2 be non
empty
Subset of X2, A3 be non
empty
Subset of X3, A4 be non
empty
Subset of X4 holds for x be
Element of
[:X1, X2, X3, X4:] st x
in
[:A1, A2, A3, A4:] holds (x
`1_4 )
in A1 & (x
`2_4 )
in A2 & (x
`3_4 )
in A3 & (x
`4_4 )
in A4
proof
let X1,X2,X3,X4 be non
empty
set, A1 be non
empty
Subset of X1, A2 be non
empty
Subset of X2, A3 be non
empty
Subset of X3, A4 be non
empty
Subset of X4;
let x be
Element of
[:X1, X2, X3, X4:];
assume x
in
[:A1, A2, A3, A4:];
then
reconsider y = x as
Element of
[:A1, A2, A3, A4:];
A1: (y
`2_4 )
in A2;
A2: (y
`4_4 )
in A4;
A3: (y
`3_4 )
in A3;
(y
`1_4 )
in A1;
hence thesis by
A1,
A3,
A2;
end;
theorem ::
MCART_1:84
Th68: X1
c= Y1 & X2
c= Y2 & X3
c= Y3 & X4
c= Y4 implies
[:X1, X2, X3, X4:]
c=
[:Y1, Y2, Y3, Y4:]
proof
A1:
[:X1, X2, X3, X4:]
=
[:
[:X1, X2, X3:], X4:] &
[:Y1, Y2, Y3, Y4:]
=
[:
[:Y1, Y2, Y3:], Y4:] by
ZFMISC_1:def 4;
assume X1
c= Y1 & X2
c= Y2 & X3
c= Y3;
then
A2:
[:X1, X2, X3:]
c=
[:Y1, Y2, Y3:] by
Th58;
assume X4
c= Y4;
hence thesis by
A2,
A1,
ZFMISC_1: 96;
end;
definition
let X1, X2, A1, A2;
:: original:
[:
redefine
func
[:A1,A2:] ->
Subset of
[:X1, X2:] ;
coherence by
ZFMISC_1: 96;
end
definition
let X1, X2, X3, A1, A2, A3;
:: original:
[:
redefine
func
[:A1,A2,A3:] ->
Subset of
[:X1, X2, X3:] ;
coherence by
Th58;
end
definition
let X1, X2, X3, X4, A1, A2, A3, A4;
:: original:
[:
redefine
func
[:A1,A2,A3,A4:] ->
Subset of
[:X1, X2, X3, X4:] ;
coherence by
Th68;
end
begin
definition
let f be
Function;
::
MCART_1:def12
func
pr1 f ->
Function means (
dom it )
= (
dom f) & for x be
object st x
in (
dom f) holds (it
. x)
= ((f
. x)
`1 );
existence
proof
deffunc
F(
object) = ((f
. $1)
`1 );
ex g be
Function st (
dom g)
= (
dom f) & for x be
object st x
in (
dom f) holds (g
. x)
=
F(x) from
FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let p1,p2 be
Function such that
A1: (
dom p1)
= (
dom f) and
A2: for x be
object st x
in (
dom f) holds (p1
. x)
= ((f
. x)
`1 ) and
A3: (
dom p2)
= (
dom f) and
A4: for x be
object st x
in (
dom f) holds (p2
. x)
= ((f
. x)
`1 );
now
let x be
object;
assume
A5: x
in (
dom f);
then (p1
. x)
= ((f
. x)
`1 ) by
A2;
hence (p1
. x)
= (p2
. x) by
A4,
A5;
end;
hence thesis by
A1,
A3,
FUNCT_1: 2;
end;
::
MCART_1:def13
func
pr2 f ->
Function means (
dom it )
= (
dom f) & for x be
object st x
in (
dom f) holds (it
. x)
= ((f
. x)
`2 );
existence
proof
deffunc
F(
object) = ((f
. $1)
`2 );
ex g be
Function st (
dom g)
= (
dom f) & for x be
object st x
in (
dom f) holds (g
. x)
=
F(x) from
FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let p1,p2 be
Function such that
A6: (
dom p1)
= (
dom f) and
A7: for x be
object st x
in (
dom f) holds (p1
. x)
= ((f
. x)
`2 ) and
A8: (
dom p2)
= (
dom f) and
A9: for x be
object st x
in (
dom f) holds (p2
. x)
= ((f
. x)
`2 );
now
let x be
object;
assume
A10: x
in (
dom f);
then (p1
. x)
= ((f
. x)
`2 ) by
A7;
hence (p1
. x)
= (p2
. x) by
A9,
A10;
end;
hence thesis by
A6,
A8,
FUNCT_1: 2;
end;
end
definition
let x be
object;
::
MCART_1:def14
func x
`11 ->
set equals ((x
`1 )
`1 );
coherence by
TARSKI: 1;
::
MCART_1:def15
func x
`12 ->
set equals ((x
`1 )
`2 );
coherence by
TARSKI: 1;
::
MCART_1:def16
func x
`21 ->
set equals ((x
`2 )
`1 );
coherence by
TARSKI: 1;
::
MCART_1:def17
func x
`22 ->
set equals ((x
`2 )
`2 );
coherence by
TARSKI: 1;
end
reserve x for
object;
theorem ::
MCART_1:85
(
[
[x1, x2], y]
`11 )
= x1 & (
[
[x1, x2], y]
`12 )
= x2 & (
[x,
[y1, y2]]
`21 )
= y1 & (
[x,
[y1, y2]]
`22 )
= y2;
theorem ::
MCART_1:86
x
in R implies (x
`1 )
in (
dom R) & (x
`2 )
in (
rng R)
proof
assume
A1: x
in R;
then x
=
[(x
`1 ), (x
`2 )] by
Th15;
hence thesis by
A1,
XTUPLE_0:def 12,
XTUPLE_0:def 13;
end;
theorem ::
MCART_1:87
Th71: for R be non
empty
Relation, x be
object holds (
Im (R,x))
= { (I
`2 ) where I be
Element of R : (I
`1 )
= x }
proof
let R be non
empty
Relation, x be
object;
set X = { (I
`2 ) where I be
Element of R : (I
`1 )
= x };
thus (
Im (R,x))
c= X
proof
let z be
object;
assume z
in (
Im (R,x));
then
consider y be
object such that
A1:
[y, z]
in R and
A2: y
in
{x} by
RELAT_1:def 13;
A3: y
= x by
A2,
TARSKI:def 1;
y
= (
[y, z]
`1 ) & z
= (
[y, z]
`2 );
hence z
in X by
A1,
A3;
end;
let z be
object;
assume z
in X;
then
consider I be
Element of R such that
A4: z
= (I
`2 ) and
A5: (I
`1 )
= x;
A6: I
=
[(I
`1 ), (I
`2 )] by
Th15;
x
in
{x} by
TARSKI:def 1;
hence z
in (
Im (R,x)) by
A4,
A5,
A6,
RELAT_1:def 13;
end;
theorem ::
MCART_1:88
x
in R implies (x
`2 )
in (
Im (R,(x
`1 )))
proof
assume
A1: x
in R;
then (x
`2 )
in { (I
`2 ) where I be
Element of R : (I
`1 )
= (x
`1 ) };
hence thesis by
A1,
Th71;
end;
theorem ::
MCART_1:89
Th73: x
in R & y
in R & (x
`1 )
= (y
`1 ) & (x
`2 )
= (y
`2 ) implies x
= y
proof
assume x
in R & y
in R;
then x
=
[(x
`1 ), (x
`2 )] & y
=
[(y
`1 ), (y
`2 )] by
Th15;
hence thesis;
end;
theorem ::
MCART_1:90
for R be non
empty
Relation, x,y be
Element of R st (x
`1 )
= (y
`1 ) & (x
`2 )
= (y
`2 ) holds x
= y by
Th73;
theorem ::
MCART_1:91
(
proj1 (
proj1
{
[x1, x2, x3],
[y1, y2, y3]}))
=
{x1, y1}
proof
thus (
proj1 (
proj1
{
[x1, x2, x3],
[y1, y2, y3]}))
= (
proj1
{
[x1, x2],
[y1, y2]}) by
RELAT_1: 10
.=
{x1, y1} by
RELAT_1: 10;
end;
theorem ::
MCART_1:92
(
proj1 (
proj1
{
[x1, x2, x3]}))
=
{x1}
proof
thus (
proj1 (
proj1
{
[x1, x2, x3]}))
= (
proj1
{
[x1, x2]}) by
RELAT_1: 9
.=
{x1} by
RELAT_1: 9;
end;
scheme ::
MCART_1:sch1
BiFuncEx { A() ->
set , B() ->
set , C() ->
set , P[
object,
object,
object] } :
ex f,g be
Function st (
dom f)
= A() & (
dom g)
= A() & for x st x
in A() holds P[x, (f
. x), (g
. x)]
provided
A1: x
in A() implies ex y, z st y
in B() & z
in C() & P[x, y, z];
defpred
H[
object,
object] means for y, z st ($2
`1 )
= y & ($2
`2 )
= z holds P[$1, y, z];
A2: for x be
object st x
in A() holds ex p be
object st p
in
[:B(), C():] &
H[x, p]
proof
let x be
object;
assume x
in A();
then
consider y, z such that
A3: y
in B() & z
in C() and
A4: P[x, y, z] by
A1;
reconsider p =
[y, z] as
set;
take p;
thus p
in
[:B(), C():] by
A3,
ZFMISC_1: 87;
thus for y, z st (p
`1 )
= y & (p
`2 )
= z holds P[x, y, z] by
A4;
end;
consider h be
Function such that (
dom h)
= A() & (
rng h)
c=
[:B(), C():] and
A5: for x be
object st x
in A() holds
H[x, (h
. x)] from
FUNCT_1:sch 6(
A2);
deffunc
g(
object) = ((h
. $1)
`2 );
deffunc
f(
object) = ((h
. $1)
`1 );
consider f be
Function such that
A6: (
dom f)
= A() and
A7: for x be
object st x
in A() holds (f
. x)
=
f(x) from
FUNCT_1:sch 3;
consider g be
Function such that
A8: (
dom g)
= A() and
A9: for x be
object st x
in A() holds (g
. x)
=
g(x) from
FUNCT_1:sch 3;
take f, g;
thus (
dom f)
= A() & (
dom g)
= A() by
A6,
A8;
thus for x st x
in A() holds P[x, (f
. x), (g
. x)]
proof
let x;
assume
A10: x
in A();
then (f
. x)
= ((h
. x)
`1 ) & (g
. x)
= ((h
. x)
`2 ) by
A7,
A9;
hence thesis by
A5,
A10;
end;
end;
theorem ::
MCART_1:93
[
[x1, x2],
[x3, x4]]
=
[
[y1, y2],
[y3, y4]] implies x1
= y1 & x2
= y2 & x3
= y3 & x4
= y4
proof
assume
[
[x1, x2],
[x3, x4]]
=
[
[y1, y2],
[y3, y4]];
then
[x1, x2]
=
[y1, y2] &
[x3, x4]
=
[y3, y4] by
XTUPLE_0: 1;
hence x1
= y1 & x2
= y2 & x3
= y3 & x4
= y4 by
XTUPLE_0: 1;
end;