LemmaStatement: AI-adaptedProof: 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 relations $R$ and $S$ and a set $A$ , the collections ${(b, a) : (a, b) \in R}$ , ${(a, c) : \exists b ((a, b) \in R \land (b, c) \in S)}$ and ${(a, b) \in R : a \in A}$ are sets

Statement

Let $R$ and $S$ be relations and $A$ a set. Then each of

${(b, a) : (a, b) \in R}, {(a, c) : \exists b ((a, b) \in R \land (b, c) \in S)}, {(a, b) \in R : a \in A}$

is a set; the first is included in $ran R \times dom R$ , the second in $dom R \times ran S$ , and the third in $R$ .

Facts & Assumptions

Given: relations $R$ and $S$ and a set $A$ .

[L1]

A relation is a set $R$ every element of which is an ordered pair (Relation, $dom R$ , $ran R$ , $fld R$ , and the specialisations "relation from $A$ to $B$ " and "relation on $A$ ").

[L2]

$dom R : = {a : \exists b (a, b) \in R}, ran R : = {b : \exists a (a, b) \in R}$ (Relation, $dom R$ , $ran R$ , $fld R$ , and the specialisations "relation from $A$ to $B$ " and "relation on $A$ ").

[L3]

$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)}$ ).

[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]

$R \subseteq dom R \times ran R$ (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$ ).

[L6]

$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)}$ ).

[L7]

$(a, b) : = {{a}, {a, b}}$ (The Kuratowski ordered pair $(a, b) : = {{a}, {a, b}}$ ).

Proof

technique · direct

1.1L2L3L4L6L7

If $(a, b) \in R$ then $a \in dom R$ and $b \in ran R$ , so $(b, a) \in ran R \times dom R$ ; separating inside that product with the formula $\exists a \exists b (z = (b, a) \land (a, b) \in R)$ and the parameter $R$ therefore yields exactly the first collection.

1.2L2L3L4L6L7

If $(a, b) \in R$ and $(b, c) \in S$ then $a \in dom R$ and $c \in ran S$ , so $(a, c) \in dom R \times ran S$ ; separating inside that product with the formula $\exists a \exists c (z = (a, c) \land \exists b ((a, b) \in R \land (b, c) \in S))$ and the parameters $R$ and $S$ yields exactly the second collection.

1.3L1L4L5L6L7

The third collection consists of elements of $R$ , and separating inside $R$ with the formula $\exists a \exists b (z = (a, b) \land a \in A)$ and the parameters $A$ and $R$ yields exactly it; every element of $R$ is an ordered pair, so the formula selects the intended pairs.

For relations $R$ and $S$ and a set $A$ , the collections ${(b, a) : (a, b) \in R}$ , ${(a, c) : \exists b ((a, b) \in R \land (b, c) \in S)}$ and ${(a, b) \in R : a \in A}$ are sets

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

For relations RR and SS and a set AA, the collections { (b,a):(a,b)∈R }{(b,a):(a,b)∈R}, { (a,c):∃b ((a,b)∈R∧(b,c)∈S) }{(a,c):∃b ((a,b)∈R∧(b,c)∈S)} and { (a,b)∈R:a∈A }{(a,b)∈R:a∈A} are sets

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

For relations $R$ and $S$ and a set $A$ , the collections ${(b, a) : (a, b) \in R}$ , ${(a, c) : \exists b ((a, b) \in R \land (b, c) \in S)}$ and ${(a, b) \in R : a \in A}$ are sets