CARTESIAN PRODUCT, RELATION AND FUNCTION

Definition S.C.1
Let x,y be sets. 
We define that (x,y) = {{x},{x,y}}.
We call (x,y) an ordered pair.

(x,y) is a set by Axiom ZF3. 

Theorem S.C.2
If x,y,a,b are sets then (x,y) = (a,b) <=> x = a and y = b.

Proof
It is obvious that if x = a and y = b then (x,y) = (a,b). 
We have to prove that if (x,y) = (a,b) then x = a and y = b. 
Assume that (x,y) = (a,b). 
Then (*) {{x},{x,y}} = {{a},{a,b}}. 
We will prove that x = a at first. 
Assume to the contrary that x != a. 
By Axiom ZF1 {x} != {a}. 
By (*) and Axiom ZF1 {x} = {a,b}. 
Thus by the Axiom ZF1 x = a. 
Contradiction. 
We have proved that x = a.
So we have (**) {{x},{x,y}} = {{x},{x,b}}.  
Now, we will prove that {x,b} = {x,y}. 
Assume to the contrary that {x,b} != {x,y}. 
Then by Axiom ZF1 applying to (**) 
we have {x,y} = {x} and {x,b} = {x}. 
Thus {x,b} = {x,y}. 
Contradiction.
We have proved that (***) {x,y} = {x,b}. 
Now, we will prove that y = b. 
Assume to the contrary that y != b. 
Then by Axiom ZF1 applying to (***)
we have y = x and b = x. 
Thus y = b. Contradiction. 
We heve proved that y = b.  

Definition S.C.3 - Power Set
Let x be a set.
We define that P(x) = z if and only if /\(y) (y:-z <=> y c x).

P(x) is a set by Axiom ZF6.

This definition is correct because z is unique by Axiom ZF1.

Theorem S.C.4
If A,B are sets and a:-A, b:-B then (a,b):-P(P(AuB)).

Proof
Notice that (a,b) = {{a},{a,b}}.
By Definition S.I.6 {a} c AuB and {a,b} c AuB.
Thus by Definition S.C.3 {a}:-P(AuB) and {a,b}:-P(AuB).
Now, by Definition S.I.6 
{{a},{a,b}} c P(AuB) and
by  Definition S.C.3 {{a},{a,b}}:-P(P(AuB)).
Thus (a,b):-P(P(AuB)).

Definition S.C.5 - Cartesian Product
Let A,B be sets.
We define that
AxB = {y:-P(P(AuB)) | \/(a:-A}\/(b:-B) y = (a,b)}

We call AxB the Cartesian product of A and B.

Theorem S.C.6
If A,B are sets
(a,b):-AxB <=> a:-A and b:-B.

Proof
(=>)
Assume that (a,b):-AxB.
Let y = (a,b). We have y:-AxB.
By Definition S.C.5 y:-P(P(AuB)) and 
\/(x:-A)\/(z:-B) y = (x,z). Thus y = (x,z) = (a,b).
By Theorem S.C.2 x = a and z = b.
Thus a:-A and b:-B.
(<=)
Assume that a:-A and b:-B.
Let y = (a,b);
By Theorem S.C.4 y = (a,b) = {{a},{a,b}}:-P(P(AuB)).
By Definition S.C.6 y:-AxB.
Thus (a,b):-AxB.

Definition S.C.7 - Relation
Let A,B be sets.
R is a relation if and only if R c AxB.

Sometimes we shorten (x,y):-R to xRy.

Definition S.C.8 - Equivalence Relation
Let A be a set.
We define that
R is an equivalence relation if and only if
R c AxA and

(1) /\(x:-A) xRx,
(2) /\(x,y:-A) xRy <=> yRx,
(3) /\(x,y,z:-A) xRy and yRz => xRz.

Definition S.C.9 - Function
Let X,Y be sets and f c XxY.

We define that f is a function if and only if 
/\(x:-X)/\(y1,y2:-Y) ( (x,y1):-f and (x,y2):-f => y1 = y2 ).

Let A,B be sets.
We define that f:A->B if and only if 
f c AxB, f is a function, and /\(x:-A) \/(y:-B) (x,y):-f.

A is called the domain of function f.

Definition S.C.10
Let A,B be sets, let f:A->B and x:-A.
We define that 
y = f(x) if and only if (x,y):-f

This definition is correct because y is unique by Definition S.C.9.

Remark: We will sometimes write f[x] instead of f(x).

Definition S.C.11
Let A,B be sets, let f:A->B and DcA.
We define that
f(D) = {y:-B | \/(x:-D) f(x)=y}.

We use Definition S.C.11 when there is no confusion 
with Definition S.C.10.

Definition S.C.12 - 1-1 Function
Let X,Y be sets, let fcXxY, 
and let f be a function.
We define that f is 1-1 if and only if
/\(x1,x2:-X) (\/(y:-Y) (x1,y):-f and (x2,y):-f) => x1 = x2.

Let A,B be sets and let f:A->B.
We define that
f:A-1-1->B if and only if
/\(x1,x2:-A) f(x1) = f(x2) => x1 = x2.

Definition S.C.13 - "onto" Function
Let A,B be sets and let f:A->B.
f maps A onto B if and only if /\(y:-B)\/(x:-A) f(x) = y.

Remark: We will sometimes write f:A-onto->B.

Remark: f:A-1-1-onto->B denotes that 
f:A->B and is both 1-1 and "onto" 

Theorem S.C.14
If X,Y are sets and L c P(P(XxY)) such that
(1) /\(f:-L) f is a function,
(2) /\(f,g:-L) f c g or g c f,
then u(L) is a function.

Proof
Take any x:-X and y1,y2:-Y such that 
(x,y1),(x,y2):-u(L).
We have f,g:-L such that 
(x,y1):-f and (x,y2):-g.
We have (f c g) or (g c f).
Thus f = f u g or g = f u g.
So f u g is a function and 
(x,y1):-fug and (x,y2):-fug.
Thus y1 = y2.
We have proved that u(L) is a function.   

Definition S.C.15
Let X,Y be sets, let A c X.
Let f:X->Y.
We define that
{f(x) | x:-A} = {y:-Y | \/(x:-A) f(x) = y }.

Definition S.C.16
Let A,B,X,Y be sets.
Let f c AxB, g c XxY.
fog = {(x,y):-AxY | \/(z:-BnX) (x,z):-f and (z,y):-g}.

Theorem S.C.16
If X,Y,Z are sets, g:X->Y and f:Y->Z
then fog:X->Z and /\(x:-X) fog(x) = f(g(x)).

Proof
First we prove that fog is a function.
Take any x:-X and z1,z2:-Z 
such that (x,z1):-fog and (x,z2):-fog.
By Definition S.C.16 we have y1,y2:-Y such that
(x,y1):-g and (y1,z1):-g 
and (x,y2):-f and (y1,z2):-f.
Since g is a function, y1 = y2.
Now since f is a function, z1 = z2.
Thus fog is a function.

We will show that fog:X->Z.
Take any x:-X.
Since g:X->Y, there exists y:-Y
such that (x,y):-g.
Since f:Y->Z, there exist z:-Z
such that (z,y):-f.
Thus (x,z):-fog.
Now it is also obvious that f(g(x)) = fog(x).

Definition S.C.17
Let X,Y are sets and fcXxY.
We define that 
f^(-1) = {(y,x):-YxX | (x,y):-f }.

Theorem S.C.18
If X,Y are sets and f:X-1-1-onto->Y
then f^(-1):Y-1-1-onto->X 
and /\(x:-X) f^(-1)(y) = x <=> f(x) = y.

Proof
Directly by Definition S.C.17.

Theorem S.C.19
If X,Y are sets and f:X-1-1-onto->Y,
/\(x:-X) (f^(-1))o(f)(x) = x,
and /\(y:-Y) (f)o(f^(-1))(y) = y.

Proof
Directly by Theorem S.C.18 and Theorem S.C.16.