LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-06 (claude-opus-5)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

For sets $A$ and $B$ the collection of all functions $A \to B$ is a set, being a subset of $P (A \times B)$

Statement

Let $A$ and $B$ be sets. Then there is a set whose elements are exactly the functions $f : A \to B$ , and it is a subset of $P (A \times B)$ .

Facts & Assumptions

Given: sets $A$ and $B$ .

[L1]

We write $f : A \to B$ , and say $f$ is a function from $A$ to $B$ , when $f$ is a function with $dom f = A$ and $ran f \subseteq B$ (A function is a relation $f$ with $(a, b) \in f$ and $(a, c) \in f$ implying $b = c$ ; $f : A \to B$ , the value $f (a)$ , domain and codomain).

[L2]

For a relation $R$ , $R \subseteq A \times B$ if and only if $dom R \subseteq A$ and $ran R \subseteq B$ (Every relation $R$ satisfies $R \subseteq dom R \times ran R$ , and $R$ is a relation from $A$ to $B$ if and only if $dom R \subseteq A$ and $ran R \subseteq B$ ).

[L3]

$z \in P (x)$ holds if and only if $z \subseteq x$ (The power set $P (x) = {z : z \subseteq x}$ ).

[L4]

For any parameters $\overset{ˉ}{p}$ and any set $x$ , there is a set $y$ whose elements are exactly the elements $z$ of $x$ for which $φ (z, \overset{ˉ}{p})$ holds (The Axiom Schema of Separation: for each formula $φ$ , $\forall \overset{ˉ}{p} \forall x \exists y \forall z (z \in y \leftrightarrow (z \in x \land φ (z, \overset{ˉ}{p})))$ ).

[L5]

$x \subseteq y$ means that every element of $x$ is an element of $y$ (Subset $x \subseteq y$ , proper subset $x ⊊ y$ , and the separation notation ${z \in x : φ (z)}$ ).

[L6]

$z \in A \times B$ holds if and only if $z = (a, b)$ for some $a \in A$ and some $b \in B$ (The Cartesian product $A \times B : = {z \in P (P (A \cup B)) : \exists a \in A \exists b \in B z = (a, b)}$ ).

Proof

technique · direct

1.1L1L2L3L5L6

A function $f : A \to B$ is a relation with $dom f = A$ and $ran f \subseteq B$ , so $f \subseteq A \times B$ and therefore $f \in P (A \times B)$ .

2.1L1L3L4L5step 1.1∎

Separating inside $P (A \times B)$ with the formula saying that $z$ is a function and $dom z = A$ , with parameters $A$ and $B$ , gives a set whose elements are exactly those elements of $P (A \times B)$ that are functions $A \to B$ ; by step 1.1 every function $A \to B$ is such an element, so that set has exactly the intended elements and is included in $P (A \times B)$ .

For sets $A$ and $B$ the collection of all functions $A \to B$ is a set, being a subset of $P (A \times B)$

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

For sets AA and BB the collection of all functions A→BA→B is a set, being a subset of P(A×B)P(A×B)

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

For sets $A$ and $B$ the collection of all functions $A \to B$ is a set, being a subset of $P (A \times B)$