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.

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$

Statement

Let $R$ be a relation and let $A$ and $B$ be sets. Then

(i) $R \subseteq dom R \times ran R$ ;
(ii) $R \subseteq A \times B$ if and only if $dom R \subseteq A$ and $ran R \subseteq B$ .

Facts & Assumptions

Given: a relation $R$ and sets $A$ , $B$ .

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

$(a, b) = (c, d)$ if and only if $a = c$ and $b = d$ ( $(a, b) = (c, d)$ if and only if $a = c$ and $b = d$ ).

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

Proof

technique · direct

1.1L1L2L3L5

Claim (i): let $z \in R$ . Since $R$ is a relation, $z = (a, b)$ for some sets $a$ and $b$ ; then $a \in dom R$ and $b \in ran R$ by the defining conditions, so $z \in dom R \times ran R$ .

1.2L2L3L4L5

Claim (ii), from left to right: assume $R \subseteq A \times B$ . If $a \in dom R$ then $(a, b) \in R$ for some $b$ , so $(a, b) \in A \times B$ , so $(a, b) = (a^{'}, b^{'})$ with $a^{'} \in A$ and $b^{'} \in B$ , and the characterising property gives $a = a^{'} \in A$ . The argument for $ran R \subseteq B$ is the same on the second coordinate.

1.3L1L2L3L5

Claim (ii), from right to left: assume $dom R \subseteq A$ and $ran R \subseteq B$ , and let $z \in R$ . Then $z = (a, b)$ with $a \in dom R \subseteq A$ and $b \in ran R \subseteq B$ , so $z \in A \times 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$

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

Every relation RR satisfies R⊆dom⁡R×ran⁡RR⊆domR×ranR, and RR is a relation from AA to BB if and only if dom⁡R⊆AdomR⊆A and ran⁡R⊆BranR⊆B

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

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$