Cartesian Product, Relation and Function (original) (raw)
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.