:: Kuratowski Pairs. {T}uples and Projections
:: by Grzegorz Bancerek, Artur Korni\l owicz and Andrzej Trybulec
::
:: Copyright (c) 2011-2012 Association of Mizar Users

begin

definition
let x be set ;
attr x is pair means :Dfx: :: XTUPLE_0:def 1
ex x1, x2 being set st x = [x1,x2];
end;

:: deftheorem Dfx defines pair XTUPLE_0:def 1 :
for x being set holds
( x is pair iff ex x1, x2 being set st x = [x1,x2] );

registration
let x1, x2 be set ;
cluster [x1,x2] -> pair ;
coherence
[x1,x2] is pair
by Dfx;
end;

Lx4: for x, y1, y2 being set st {x} = {y1,y2} holds
x = y1

proof end;

Lx5: for x, y1, y2 being set st {x} = {y1,y2} holds
y1 = y2

proof end;

Lx6: for x1, x2, y1, y2 being set holds
( not {x1,x2} = {y1,y2} or x1 = y1 or x1 = y2 )

proof end;

theorem Th1: :: XTUPLE_0:1
for x1, x2, y1, y2 being set st [x1,x2] = [y1,y2] holds
( x1 = y1 & x2 = y2 )
proof end;

definition
let x be set ;
assume x is pair ;
then consider x1, x2 being set such that
A1: x = [x1,x2] by Dfx;
func x 1 -> set means :Def1: :: XTUPLE_0:def 2
for y1, y2 being set st x = [y1,y2] holds
it = y1;
existence
ex b1 being set st
for y1, y2 being set st x = [y1,y2] holds
b1 = y1
proof end;
uniqueness
for b1, b2 being set st ( for y1, y2 being set st x = [y1,y2] holds
b1 = y1 ) & ( for y1, y2 being set st x = [y1,y2] holds
b2 = y1 ) holds
b1 = b2
proof end;
func x 2 -> set means :Def2: :: XTUPLE_0:def 3
for y1, y2 being set st x = [y1,y2] holds
it = y2;
existence
ex b1 being set st
for y1, y2 being set st x = [y1,y2] holds
b1 = y2
proof end;
uniqueness
for b1, b2 being set st ( for y1, y2 being set st x = [y1,y2] holds
b1 = y2 ) & ( for y1, y2 being set st x = [y1,y2] holds
b2 = y2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines 1 XTUPLE_0:def 2 :
for x being set st x is pair holds
for b2 being set holds
( b2 = x 1 iff for y1, y2 being set st x = [y1,y2] holds
b2 = y1 );

:: deftheorem Def2 defines 2 XTUPLE_0:def 3 :
for x being set st x is pair holds
for b2 being set holds
( b2 = x 2 iff for y1, y2 being set st x = [y1,y2] holds
b2 = y2 );

registration
let x1, x2 be set ;
reduce [x1,x2] 1 to x1;
reducibility
[x1,x2] 1 = x1
by Def1;
reduce [x1,x2] 2 to x2;
reducibility
[x1,x2] 2 = x2
by Def2;
end;

registration
cluster pair for set ;
existence
ex b1 being set st b1 is pair
proof end;
end;

registration
let x be pair set ;
reduce [(x 1),(x 2)] to x;
reducibility
[(x 1),(x 2)] = x
proof end;
end;

theorem :: XTUPLE_0:2
for a, b being pair set st a 1 = b 1 & a 2 = b 2 holds
a = b
proof end;

begin

definition
let x1, x2, x3 be set ;
func [x1,x2,x3] -> set equals :: XTUPLE_0:def 4
[[x1,x2],x3];
coherence
[[x1,x2],x3] is set
;
end;

:: deftheorem defines [ XTUPLE_0:def 4 :
for x1, x2, x3 being set holds [x1,x2,x3] = [[x1,x2],x3];

definition
let x be set ;
attr x is triple means :Dfy: :: XTUPLE_0:def 5
ex x1, x2, x3 being set st x = [x1,x2,x3];
end;

:: deftheorem Dfy defines triple XTUPLE_0:def 5 :
for x being set holds
( x is triple iff ex x1, x2, x3 being set st x = [x1,x2,x3] );

registration
let x1, x2, x3 be set ;
cluster [x1,x2,x3] -> triple ;
coherence
[x1,x2,x3] is triple
by Dfy;
end;

theorem Th3: :: XTUPLE_0:3
for x1, x2, x3, y1, y2, y3 being set st [x1,x2,x3] = [y1,y2,y3] holds
( x1 = y1 & x2 = y2 & x3 = y3 )
proof end;

registration
cluster triple for set ;
existence
ex b1 being set st b1 is triple
proof end;
cluster triple -> pair for set ;
coherence
for b1 being set st b1 is triple holds
b1 is pair
proof end;
end;

definition
let x be set ;
func x 1_3 -> set equals :: XTUPLE_0:def 6
(x 1) 1 ;
coherence
(x 1) 1 is set
;
func x 2_3 -> set equals :: XTUPLE_0:def 7
(x 1) 2 ;
coherence
(x 1) 2 is set
;
end;

:: deftheorem defines 1_3 XTUPLE_0:def 6 :
for x being set holds x 1_3 = (x 1) 1 ;

:: deftheorem defines 2_3 XTUPLE_0:def 7 :
for x being set holds x 2_3 = (x 1) 2 ;

notation
let x be set ;
synonym x 3_3 for x 2 ;
end;

registration
let x1, x2, x3 be set ;
reduce [x1,x2,x3] 1_3 to x1;
reducibility
[x1,x2,x3] 1_3 = x1
proof end;
reduce [x1,x2,x3] 2_3 to x2;
reducibility
[x1,x2,x3] 2_3 = x2
proof end;
reduce [x1,x2,x3] 3_3 to x3;
reducibility
[x1,x2,x3] 3_3 = x3
proof end;
end;

registration
let x be triple set ;
reduce [(x 1_3),(x 2_3),(x 3_3)] to x;
reducibility
[(x 1_3),(x 2_3),(x 3_3)] = x
proof end;
end;

theorem :: XTUPLE_0:4
for a, b being triple set st a 1_3 = b 1_3 & a 2_3 = b 2_3 & a 3_3 = b 3_3 holds
a = b
proof end;

begin

definition
let x1, x2, x3, x4 be set ;
func [x1,x2,x3,x4] -> set equals :: XTUPLE_0:def 8
[[x1,x2,x3],x4];
coherence
[[x1,x2,x3],x4] is set
;
end;

:: deftheorem defines [ XTUPLE_0:def 8 :
for x1, x2, x3, x4 being set holds [x1,x2,x3,x4] = [[x1,x2,x3],x4];

definition
let x be set ;
attr x is quadruple means :Dfz: :: XTUPLE_0:def 9
ex x1, x2, x3, x4 being set st x = [x1,x2,x3,x4];
end;

:: deftheorem Dfz defines quadruple XTUPLE_0:def 9 :
for x being set holds
( x is quadruple iff ex x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] );

registration
let x1, x2, x3, x4 be set ;
coherence
by Dfz;
end;

theorem :: XTUPLE_0:5
for x1, x2, x3, x4, y1, y2, y3, y4 being set st [x1,x2,x3,x4] = [y1,y2,y3,y4] holds
( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 )
proof end;

registration
existence
ex b1 being set st b1 is quadruple
proof end;
coherence
for b1 being set st b1 is quadruple holds
b1 is triple
proof end;
end;

definition
let x be set ;
func x 1_4 -> set equals :: XTUPLE_0:def 10
((x 1) 1) 1 ;
coherence
((x 1) 1) 1 is set
;
func x 2_4 -> set equals :: XTUPLE_0:def 11
((x 1) 1) 2 ;
coherence
((x 1) 1) 2 is set
;
end;

:: deftheorem defines 1_4 XTUPLE_0:def 10 :
for x being set holds x 1_4 = ((x 1) 1) 1 ;

:: deftheorem defines 2_4 XTUPLE_0:def 11 :
for x being set holds x 2_4 = ((x 1) 1) 2 ;

notation
let x be set ;
synonym x 3_4 for x 2_3 ;
synonym x 4_4 for x 2 ;
end;

registration
let x1, x2, x3, x4 be set ;
reduce [x1,x2,x3,x4] 1_4 to x1;
reducibility
[x1,x2,x3,x4] 1_4 = x1
proof end;
reduce [x1,x2,x3,x4] 2_4 to x2;
reducibility
[x1,x2,x3,x4] 2_4 = x2
proof end;
reduce [x1,x2,x3,x4] 3_4 to x3;
reducibility
[x1,x2,x3,x4] 3_4 = x3
proof end;
reduce [x1,x2,x3,x4] 4_4 to x4;
reducibility
[x1,x2,x3,x4] 4_4 = x4
proof end;
end;

registration
let x be quadruple set ;
reduce [(x 1_4),(x 2_4),(x 3_4),(x 4_4)] to x;
reducibility
[(x 1_4),(x 2_4),(x 3_4),(x 4_4)] = x
proof end;
end;

:: Preliminaries
theorem Pre1: :: XTUPLE_0:6
for x, y, X being set st [x,y] in X holds
x in union ()
proof end;

theorem Pre2: :: XTUPLE_0:7
for x, y, X being set st [x,y] in X holds
y in union ()
proof end;

:: Projections
definition
let X be set ;
func proj1 X -> set means :Def4: :: XTUPLE_0:def 12
for x being set holds
( x in it iff ex y being set st [x,y] in X );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex y being set st [x,y] in X )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex y being set st [x,y] in X ) ) & ( for x being set holds
( x in b2 iff ex y being set st [x,y] in X ) ) holds
b1 = b2
proof end;
func proj2 X -> set means :Def5: :: XTUPLE_0:def 13
for x being set holds
( x in it iff ex y being set st [y,x] in X );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex y being set st [y,x] in X )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex y being set st [y,x] in X ) ) & ( for x being set holds
( x in b2 iff ex y being set st [y,x] in X ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines proj1 XTUPLE_0:def 12 :
for X, b2 being set holds
( b2 = proj1 X iff for x being set holds
( x in b2 iff ex y being set st [x,y] in X ) );

:: deftheorem Def5 defines proj2 XTUPLE_0:def 13 :
for X, b2 being set holds
( b2 = proj2 X iff for x being set holds
( x in b2 iff ex y being set st [y,x] in X ) );

theorem Th10: :: XTUPLE_0:8
for X, Y being set st X c= Y holds
proj1 X c= proj1 Y
proof end;

theorem Th11: :: XTUPLE_0:9
for X, Y being set st X c= Y holds
proj2 X c= proj2 Y
proof end;

definition
let X be set ;
func proj1_3 X -> set equals :: XTUPLE_0:def 14
proj1 ();
coherence
proj1 () is set
;
func proj2_3 X -> set equals :: XTUPLE_0:def 15
proj2 ();
coherence
proj2 () is set
;
end;

:: deftheorem defines proj1_3 XTUPLE_0:def 14 :
for X being set holds proj1_3 X = proj1 ();

:: deftheorem defines proj2_3 XTUPLE_0:def 15 :
for X being set holds proj2_3 X = proj2 ();

notation
let X be set ;
synonym proj3_3 X for proj2 X;
end;

theorem Th12: :: XTUPLE_0:10
for X, Y being set st X c= Y holds
proj1_3 X c= proj1_3 Y
proof end;

theorem Th13: :: XTUPLE_0:11
for X, Y being set st X c= Y holds
proj2_3 X c= proj2_3 Y
proof end;

theorem Th14: :: XTUPLE_0:12
for x, X being set st x in proj1_3 X holds
ex y, z being set st [x,y,z] in X
proof end;

theorem Th14a: :: XTUPLE_0:13
for x, y, z, X being set st [x,y,z] in X holds
x in proj1_3 X
proof end;

theorem Th15: :: XTUPLE_0:14
for x, X being set st x in proj2_3 X holds
ex y, z being set st [y,x,z] in X
proof end;

theorem Th15a: :: XTUPLE_0:15
for x, y, z, X being set st [x,y,z] in X holds
y in proj2_3 X
proof end;

definition
let X be set ;
func proj1_4 X -> set equals :: XTUPLE_0:def 16
proj1 ();
coherence
proj1 () is set
;
func proj2_4 X -> set equals :: XTUPLE_0:def 17
proj2 ();
coherence
proj2 () is set
;
end;

:: deftheorem defines proj1_4 XTUPLE_0:def 16 :
for X being set holds proj1_4 X = proj1 ();

:: deftheorem defines proj2_4 XTUPLE_0:def 17 :
for X being set holds proj2_4 X = proj2 ();

notation
let X be set ;
synonym proj3_4 X for proj2_3 X;
synonym proj4_4 X for proj2 X;
end;

theorem Th17: :: XTUPLE_0:16
for X, Y being set st X c= Y holds
proj1_4 X c= proj1_4 Y
proof end;

theorem Th18: :: XTUPLE_0:17
for X, Y being set st X c= Y holds
proj2_4 X c= proj2_4 Y
proof end;

theorem Th19: :: XTUPLE_0:18
for x, X being set st x in proj1_4 X holds
ex x1, x2, x3 being set st [x,x1,x2,x3] in X
proof end;

theorem Th19a: :: XTUPLE_0:19
for x, x1, x2, x3, X being set st [x,x1,x2,x3] in X holds
x in proj1_4 X
proof end;

theorem Th20: :: XTUPLE_0:20
for x, X being set st x in proj2_4 X holds
ex x1, x2, x3 being set st [x1,x,x2,x3] in X
proof end;

theorem Th20a: :: XTUPLE_0:21
for x1, x, x2, x3, X being set st [x1,x,x2,x3] in X holds
x in proj2_4 X
proof end;

theorem :: XTUPLE_0:22
for a, b being quadruple set st a 1_4 = b 1_4 & a 2_4 = b 2_4 & a 3_4 = b 3_4 & a 4_4 = b 4_4 holds
a = b
proof end;

begin

registration
let X be empty set ;
coherence
proj1 X is empty
proof end;
end;

registration
let X be empty set ;
coherence
proj2 X is empty
proof end;
end;

registration
let X be empty set ;
coherence
proj1_3 X is empty
;
end;

registration
let X be empty set ;
coherence
proj2_3 X is empty
;
end;

registration
let X be empty set ;
coherence
proj1_4 X is empty
;
end;

registration
let X be empty set ;
coherence
proj2_4 X is empty
;
end;

theorem Th22: :: XTUPLE_0:23
for X, Y being set holds proj1 (X \/ Y) = () \/ ()
proof end;

theorem :: XTUPLE_0:24
for X, Y being set holds proj1 (X /\ Y) c= () /\ ()
proof end;

theorem Th24: :: XTUPLE_0:25
for X, Y being set holds () \ () c= proj1 (X \ Y)
proof end;

theorem :: XTUPLE_0:26
for X, Y being set holds () \+\ () c= proj1 (X \+\ Y)
proof end;

theorem Th26: :: XTUPLE_0:27
for X, Y being set holds proj2 (X \/ Y) = () \/ ()
proof end;

theorem :: XTUPLE_0:28
for X, Y being set holds proj2 (X /\ Y) c= () /\ ()
proof end;

theorem Th28: :: XTUPLE_0:29
for X, Y being set holds () \ () c= proj2 (X \ Y)
proof end;

theorem :: XTUPLE_0:30
for X, Y being set holds () \+\ () c= proj2 (X \+\ Y)
proof end;

theorem Th30: :: XTUPLE_0:31
for X, Y being set holds proj1_3 (X \/ Y) = () \/ ()
proof end;

theorem :: XTUPLE_0:32
for X, Y being set holds proj1_3 (X /\ Y) c= () /\ ()
proof end;

theorem Th32: :: XTUPLE_0:33
for X, Y being set holds () \ () c= proj1_3 (X \ Y)
proof end;

theorem :: XTUPLE_0:34
for X, Y being set holds () \+\ () c= proj1_3 (X \+\ Y)
proof end;

theorem Th34: :: XTUPLE_0:35
for X, Y being set holds proj2_3 (X \/ Y) = () \/ ()
proof end;

theorem :: XTUPLE_0:36
for X, Y being set holds proj2_3 (X /\ Y) c= () /\ ()
proof end;

theorem Th36: :: XTUPLE_0:37
for X, Y being set holds () \ () c= proj2_3 (X \ Y)
proof end;

theorem :: XTUPLE_0:38
for X, Y being set holds () \+\ () c= proj2_3 (X \+\ Y)
proof end;

theorem Th38: :: XTUPLE_0:39
for X, Y being set holds proj1_4 (X \/ Y) = () \/ ()
proof end;

theorem :: XTUPLE_0:40
for X, Y being set holds proj1_4 (X /\ Y) c= () /\ ()
proof end;

theorem Th32: :: XTUPLE_0:41
for X, Y being set holds () \ () c= proj1_4 (X \ Y)
proof end;

theorem :: XTUPLE_0:42
for X, Y being set holds () \+\ () c= proj1_4 (X \+\ Y)
proof end;

theorem Th34: :: XTUPLE_0:43
for X, Y being set holds proj2_4 (X \/ Y) = () \/ ()
proof end;

theorem :: XTUPLE_0:44
for X, Y being set holds proj2_4 (X /\ Y) c= () /\ ()
proof end;

theorem Th36: :: XTUPLE_0:45
for X, Y being set holds () \ () c= proj2_4 (X \ Y)
proof end;

theorem :: XTUPLE_0:46
for X, Y being set holds () \+\ () c= proj2_4 (X \+\ Y)
proof end;