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

definition

let x be object ;

attr x is pair means :Def1: :: XTUPLE_0:def 1
ex x1, x2 being object st x = [x1,x2];

end;

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

registration

let x1, x2 be object ;

cluster [x1,x2] -> pair ;

coherence
[x1,x2] is pair ;

end;

Lm1: for x, y1, y2 being object st {x} = {y1,y2} holds
x = y1

proof end;

Lm2: for x, y1, y2 being object st {x} = {y1,y2} holds
y1 = y2

proof end;

Lm3: for x1, x2, y1, y2 being object 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 object st [x1,x2] = [y1,y2] holds
( x1 = y1 & x2 = y2 )

proof end;

definition

let x be object ;
assume x is pair ;
then consider x1, x2 being object such that
A1: x = [x1,x2] ;

func x `1 -> object means :Def2: :: XTUPLE_0:def 2
for y1, y2 being object st x = [y1,y2] holds
it = y1;

existence
ex b₁ being object st
for y1, y2 being object st x = [y1,y2] holds
b₁ = y1

proof end;

uniqueness
for b₁, b₂ being object st ( for y1, y2 being object st x = [y1,y2] holds
b₁ = y1 ) & ( for y1, y2 being object st x = [y1,y2] holds
b₂ = y1 ) holds
b₁ = b₂

proof end;

func x `2 -> object means :Def3: :: XTUPLE_0:def 3
for y1, y2 being object st x = [y1,y2] holds
it = y2;

existence
ex b₁ being object st
for y1, y2 being object st x = [y1,y2] holds
b₁ = y2

proof end;

uniqueness
for b₁, b₂ being object st ( for y1, y2 being object st x = [y1,y2] holds
b₁ = y2 ) & ( for y1, y2 being object st x = [y1,y2] holds
b₂ = y2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines `1 XTUPLE_0:def 2 :
for x being object st x is pair holds
for b<sub>2</sub> being object holds
( b<sub>2</sub> = x `1 iff for y1, y2 being object st x = [y1,y2] holds
b₂ = y1 );

:: deftheorem Def3 defines `2 XTUPLE_0:def 3 :
for x being object st x is pair holds
for b<sub>2</sub> being object holds
( b<sub>2</sub> = x `2 iff for y1, y2 being object st x = [y1,y2] holds
b₂ = y2 );

registration

let x1, x2 be object ;

reduce [x1,x2] `1 to x1;

reducibility
[x1,x2] `1 = x1 by Def2;

reduce [x1,x2] `2 to x2;

reducibility
[x1,x2] `2 = x2 by Def3;

end;

registration

cluster pair for object ;

existence
ex b₁ being object st b₁ is pair

proof end;

end;

registration

let x be pair object ;

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 object st a `1 = b `1 & a `2 = b `2 holds
a = b

proof end;

definition

let x1, x2, x3 be object ;

func [x1,x2,x3] -> object equals :: XTUPLE_0:def 4
[[x1,x2],x3];

coherence
[[x1,x2],x3] is object ;

end;

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

definition

let x be object ;

attr x is triple means :Def5: :: XTUPLE_0:def 5
ex x1, x2, x3 being object st x = [x1,x2,x3];

end;

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

registration

let x1, x2, x3 be object ;

cluster [x1,x2,x3] -> triple ;

coherence
[x1,x2,x3] is triple ;

end;

theorem Th3: :: XTUPLE_0:3

for x1, x2, x3, y1, y2, y3 being object st [x1,x2,x3] = [y1,y2,y3] holds
( x1 = y1 & x2 = y2 & x3 = y3 )

proof end;

registration

cluster triple for object ;

existence
ex b₁ being object st b₁ is triple

proof end;

cluster triple -> pair for object ;

coherence
for b₁ being object st b₁ is triple holds
b₁ is pair ;

end;

definition

let x be object ;

func x `1_3 -> object equals :: XTUPLE_0:def 6
(x `1) `1 ;

coherence
(x `1) `1 is object ;

func x `2_3 -> object equals :: XTUPLE_0:def 7
(x `1) `2 ;

coherence
(x `1) `2 is object ;

end;

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

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

notation

let x be object ;
synonym x `3_3 for x `2 ;

end;

registration

let x1, x2, x3 be object ;

reduce [x1,x2,x3] `1_3 to x1;

reducibility
[x1,x2,x3] `1_3 = x1 ;

reduce [x1,x2,x3] `2_3 to x2;

reducibility
[x1,x2,x3] `2_3 = x2 ;

reduce [x1,x2,x3] `3_3 to x3;

reducibility
[x1,x2,x3] `3_3 = x3 ;

end;

registration

let x be triple object ;

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 object st a `1_3 = b `1_3 & a `2_3 = b `2_3 & a `3_3 = b `3_3 holds
a = b

proof end;

definition

let x1, x2, x3, x4 be object ;

func [x1,x2,x3,x4] -> object equals :: XTUPLE_0:def 8
[[x1,x2,x3],x4];

coherence
[[x1,x2,x3],x4] is object ;

end;

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

definition

let x be object ;

attr x is quadruple means :Def9: :: XTUPLE_0:def 9
ex x1, x2, x3, x4 being object st x = [x1,x2,x3,x4];

end;

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

registration

let x1, x2, x3, x4 be object ;

cluster [x1,x2,x3,x4] -> quadruple ;

coherence
[x1,x2,x3,x4] is quadruple ;

end;

theorem :: XTUPLE_0:5

for x1, x2, x3, x4, y1, y2, y3, y4 being object st [x1,x2,x3,x4] = [y1,y2,y3,y4] holds
( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 )

proof end;

registration

cluster quadruple for object ;

existence
ex b₁ being object st b₁ is quadruple

proof end;

cluster quadruple -> triple for object ;

coherence
for b₁ being object st b₁ is quadruple holds
b₁ is triple

proof end;

end;

definition

let x be object ;

func x `1_4 -> object equals :: XTUPLE_0:def 10
((x `1) `1) `1 ;

coherence
((x `1) `1) `1 is object ;

func x `2_4 -> object equals :: XTUPLE_0:def 11
((x `1) `1) `2 ;

coherence
((x `1) `1) `2 is object ;

end;

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

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

notation

let x be object ;
synonym x `3_4 for x `2_3 ;
synonym x `4_4 for x `2 ;

end;

registration

let x1, x2, x3, x4 be object ;

reduce [x1,x2,x3,x4] `1_4 to x1;

reducibility
[x1,x2,x3,x4] `1_4 = x1 ;

reduce [x1,x2,x3,x4] `2_4 to x2;

reducibility
[x1,x2,x3,x4] `2_4 = x2 ;

reduce [x1,x2,x3,x4] `3_4 to x3;

reducibility
[x1,x2,x3,x4] `3_4 = x3 ;

reduce [x1,x2,x3,x4] `4_4 to x4;

reducibility
[x1,x2,x3,x4] `4_4 = x4 ;

end;

registration

let x be quadruple object ;

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 Th6: :: XTUPLE_0:6

for x, y being object
for X being set st [x,y] in X holds
x in union (union X)

proof end;

theorem Th7: :: XTUPLE_0:7

for x, y being object
for X being set st [x,y] in X holds
y in union (union X)

proof end;

:: Projections

definition

let X be set ;

func proj1 X -> set means :Def12: :: XTUPLE_0:def 12
for x being object holds
( x in it iff ex y being object st [x,y] in X );

existence
ex b₁ being set st
for x being object holds
( x in b₁ iff ex y being object st [x,y] in X )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff ex y being object st [x,y] in X ) ) & ( for x being object holds
( x in b₂ iff ex y being object st [x,y] in X ) ) holds
b₁ = b₂

proof end;

func proj2 X -> set means :Def13: :: XTUPLE_0:def 13
for x being object holds
( x in it iff ex y being object st [y,x] in X );

existence
ex b₁ being set st
for x being object holds
( x in b₁ iff ex y being object st [y,x] in X )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff ex y being object st [y,x] in X ) ) & ( for x being object holds
( x in b₂ iff ex y being object st [y,x] in X ) ) holds
b₁ = b₂

proof end;

end;

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

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

theorem Th8: :: XTUPLE_0:8

for X, Y being set st X c= Y holds
proj1 X c= proj1 Y

proof end;

theorem Th9: :: 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 (proj1 X);

coherence
proj1 (proj1 X) is set ;

func proj2_3 X -> set equals :: XTUPLE_0:def 15
proj2 (proj1 X);

coherence
proj2 (proj1 X) is set ;

end;

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

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

notation

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

end;

theorem Th10: :: XTUPLE_0:10

for X, Y being set st X c= Y holds
proj1_3 X c= proj1_3 Y

proof end;

theorem Th11: :: XTUPLE_0:11

for X, Y being set st X c= Y holds
proj2_3 X c= proj2_3 Y

proof end;

theorem Th12: :: XTUPLE_0:12

for x being object
for X being set st x in proj1_3 X holds
ex y, z being object st [x,y,z] in X

proof end;

theorem Th13: :: XTUPLE_0:13

for x, y, z being object
for X being set st [x,y,z] in X holds
x in proj1_3 X

proof end;

theorem Th14: :: XTUPLE_0:14

for x being object
for X being set st x in proj2_3 X holds
ex y, z being object st [y,x,z] in X

proof end;

theorem Th15: :: XTUPLE_0:15

for x, y, z being object
for 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 (proj1_3 X);

coherence
proj1 (proj1_3 X) is set ;

func proj2_4 X -> set equals :: XTUPLE_0:def 17
proj2 (proj1_3 X);

coherence
proj2 (proj1_3 X) is set ;

end;

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

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

notation

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

end;

theorem Th16: :: XTUPLE_0:16

for X, Y being set st X c= Y holds
proj1_4 X c= proj1_4 Y

proof end;

theorem Th17: :: XTUPLE_0:17

for X, Y being set st X c= Y holds
proj2_4 X c= proj2_4 Y

proof end;

theorem Th18: :: XTUPLE_0:18

for x being object
for X being set st x in proj1_4 X holds
ex x1, x2, x3 being object st [x,x1,x2,x3] in X

proof end;

theorem Th19: :: XTUPLE_0:19

for x, x1, x2, x3 being object
for 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 being object
for X being set st x in proj2_4 X holds
ex x1, x2, x3 being object st [x1,x,x2,x3] in X

proof end;

theorem Th21: :: XTUPLE_0:21

for x, x1, x2, x3 being object
for 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 object 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;

registration

let X be empty set ;

cluster proj1 X -> empty ;

coherence
proj1 X is empty

proof end;

end;

registration

let X be empty set ;

cluster proj2 X -> empty ;

coherence
proj2 X is empty

proof end;

end;

registration

let X be empty set ;

cluster proj1_3 X -> empty ;

coherence
proj1_3 X is empty ;

end;

registration

let X be empty set ;

cluster proj2_3 X -> empty ;

coherence
proj2_3 X is empty ;

end;

registration

let X be empty set ;

cluster proj1_4 X -> empty ;

coherence
proj1_4 X is empty ;

end;

registration

let X be empty set ;

cluster proj2_4 X -> empty ;

coherence
proj2_4 X is empty ;

end;

theorem Th23: :: XTUPLE_0:23

for X, Y being set holds proj1 (X \/ Y) = (proj1 X) \/ (proj1 Y)

proof end;

theorem :: XTUPLE_0:24

for X, Y being set holds proj1 (X /\ Y) c= (proj1 X) /\ (proj1 Y)

proof end;

theorem Th25: :: XTUPLE_0:25

for X, Y being set holds (proj1 X) \ (proj1 Y) c= proj1 (X \ Y)

proof end;

theorem :: XTUPLE_0:26

for X, Y being set holds (proj1 X) \+\ (proj1 Y) c= proj1 (X \+\ Y)

proof end;

theorem Th27: :: XTUPLE_0:27

for X, Y being set holds proj2 (X \/ Y) = (proj2 X) \/ (proj2 Y)

proof end;

theorem :: XTUPLE_0:28

for X, Y being set holds proj2 (X /\ Y) c= (proj2 X) /\ (proj2 Y)

proof end;

theorem Th29: :: XTUPLE_0:29

for X, Y being set holds (proj2 X) \ (proj2 Y) c= proj2 (X \ Y)

proof end;

theorem :: XTUPLE_0:30

for X, Y being set holds (proj2 X) \+\ (proj2 Y) c= proj2 (X \+\ Y)

proof end;

theorem Th31: :: XTUPLE_0:31

for X, Y being set holds proj1_3 (X \/ Y) = (proj1_3 X) \/ (proj1_3 Y)

proof end;

theorem :: XTUPLE_0:32

for X, Y being set holds proj1_3 (X /\ Y) c= (proj1_3 X) /\ (proj1_3 Y)

proof end;

theorem Th33: :: XTUPLE_0:33

for X, Y being set holds (proj1_3 X) \ (proj1_3 Y) c= proj1_3 (X \ Y)

proof end;

theorem :: XTUPLE_0:34

for X, Y being set holds (proj1_3 X) \+\ (proj1_3 Y) c= proj1_3 (X \+\ Y)

proof end;

theorem Th35: :: XTUPLE_0:35

for X, Y being set holds proj2_3 (X \/ Y) = (proj2_3 X) \/ (proj2_3 Y)

proof end;

theorem :: XTUPLE_0:36

for X, Y being set holds proj2_3 (X /\ Y) c= (proj2_3 X) /\ (proj2_3 Y)

proof end;

theorem Th37: :: XTUPLE_0:37

for X, Y being set holds (proj2_3 X) \ (proj2_3 Y) c= proj2_3 (X \ Y)

proof end;

theorem :: XTUPLE_0:38

for X, Y being set holds (proj2_3 X) \+\ (proj2_3 Y) c= proj2_3 (X \+\ Y)

proof end;

theorem Th39: :: XTUPLE_0:39

for X, Y being set holds proj1_4 (X \/ Y) = (proj1_4 X) \/ (proj1_4 Y)

proof end;

theorem :: XTUPLE_0:40

for X, Y being set holds proj1_4 (X /\ Y) c= (proj1_4 X) /\ (proj1_4 Y)

proof end;

theorem Th41: :: XTUPLE_0:41

for X, Y being set holds (proj1_4 X) \ (proj1_4 Y) c= proj1_4 (X \ Y)

proof end;

theorem :: XTUPLE_0:42

for X, Y being set holds (proj1_4 X) \+\ (proj1_4 Y) c= proj1_4 (X \+\ Y)

proof end;

theorem Th43: :: XTUPLE_0:43

for X, Y being set holds proj2_4 (X \/ Y) = (proj2_4 X) \/ (proj2_4 Y)

proof end;

theorem :: XTUPLE_0:44

for X, Y being set holds proj2_4 (X /\ Y) c= (proj2_4 X) /\ (proj2_4 Y)

proof end;

theorem Th45: :: XTUPLE_0:45

for X, Y being set holds (proj2_4 X) \ (proj2_4 Y) c= proj2_4 (X \ Y)

proof end;

theorem :: XTUPLE_0:46

for X, Y being set holds (proj2_4 X) \+\ (proj2_4 Y) c= proj2_4 (X \+\ Y)

proof end;