Definition S.C.1Let 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.2If x,y,a,b are sets then (x,y) = (a,b) <=> x = a and y = b.ProofIt 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 SetLet 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.4If A,B are sets and a:-A, b:-B then (a,b):-P(P(AuB)).ProofNotice 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 ProductLet 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.6If 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 - RelationLet 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 RelationLet 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 - FunctionLet 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.10Let 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.11Let 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 FunctionLet 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" FunctionLet 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.14If 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.ProofTake 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.15Let 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.16Let 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.16If X,Y,Z are sets, g:X->Y and f:Y->Z then fog:X->Z and /\(x:-X) fog(x) = f(g(x)).ProofFirst 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.17Let X,Y are sets and fcXxY. We define that f^(-1) = {(y,x):-YxX | (x,y):-f }.Theorem S.C.18If 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.ProofDirectly by Definition S.C.17.Theorem S.C.19If 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.ProofDirectly by Theorem S.C.18 and Theorem S.C.16.