Theorem

Let A and B be objects. Let f(a) be a member of B depending on a member a of A. Then we have {⟨a,b⟩∈A×B|f(a)=b} is a function from A to B.

Background

The following background is necessary to understand this theorem.

(.) Let A and x be objects. Then x∈A is a proposition.

(.) Let x and y be objects. Then x=y is a proposition.

(.) Let A and B be objects. Let φ(a,b) be a proposition depending on a member a of A and a member b of B. Then "{⟨a,b⟩∈A×B|φ(a,b)}" is an object.

(.) Let A, B and f be objects. Then "f is a function from A to B" is a proposition.

Background for Proof

The following background is necessary for the proof.

(.) Let φ and ψ be propositions. Then φ∧ψ is a proposition.

(.) Let A be an object. Let φ(a) be a proposition depending on a member a of A. Then "∀a∈A⋅φ(a)" is a proposition.

(.) Let φ and ψ be propositions. Assume φ and ψ. Then we know φ∧ψ.

(.) Let x be an object. Then we know x=x.

(.) Let x and y be objects. Assume x=y. Then we know y=x.

(.) Let A be an object. Let φ(a) be a proposition depending on a member a of A. Assume for all a ∈ A φ(a). Then we know ∀a∈A⋅φ(a).

(.) Let x and y be objects. Then "⟨x,y⟩" is an object.

(.) Let A be an object. Let φ(a) be a proposition depending on a member a of A. Then "∃!a∈A⋅φ(a)" is a proposition.

(.) Let A be an object. Let φ(a) be a proposition depending on a member a of A. Let a be a member of A. Assume φ(a) and for all b ∈ A φ(b) implies b=a. Then we know ∃!a∈A⋅φ(a).

(.) Let A, B and R be objects. Then "R is a binary relation on A and B" is a proposition.

(.) Let A, B and f be objects. Then f is a function from A to B is the proposition given by "f is a binary relation on A and B"∧∀a∈A⋅∃!b∈B⋅⟨a,b⟩∈f.

(.) Let A and B be objects. Let φ(a,b) be a proposition depending on a member a of A and a member b of B. Let a be a member of A. Let b be a member of B. Assume φ(a,b). Then we know ⟨a,b⟩∈{⟨a,b⟩∈A×B|φ(a,b)}.

(.) Let A and B be objects. Let φ(a,b) be a proposition depending on a member a of A and a member b of B. Then we know {⟨a,b⟩∈A×B|φ(a,b)} is a binary relation on A and B.

(.) Let A and B be objects. Let φ(a,b) be a proposition depending on a member a of A and a member b of B. Let a be a member of A. Let b be a member of B. Assume ⟨a,b⟩∈{⟨a,b⟩∈A×B|φ(a,b)}. Then we know φ(a,b).

Proof

We will show "{⟨a,b⟩∈A×B|f(a)=b} is a binary relation on A and B"∧∀a∈A⋅∃!b∈B⋅⟨a,b⟩∈{⟨a,b⟩∈A×B|f(a)=b}. We have {⟨a,b⟩∈A×B|f(a)=b} is a binary relation on A and B. Using this, it is enough to show ∀a∈A⋅∃!b∈B⋅⟨a,b⟩∈{⟨a,b⟩∈A×B|f(a)=b}. Let a be a member of B. We know ⟨a,f(a)⟩∈{⟨a,b⟩∈A×B|f(a)=b}. Clearly, for all b ∈ B ⟨a,b⟩∈{⟨a,b⟩∈A×B|f(a)=b} implies b=f(a). Using this and ⟨a,f(a)⟩∈{⟨a,b⟩∈A×B|f(a)=b}, we conclude ∃!b∈B⋅⟨a,b⟩∈{⟨a,b⟩∈A×B|f(a)=b}.

Click here to modify variable names (JavaScript Must Be Enabled).

Hide Background.

Test yourself on this item.