PropositionStatement: 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.

$R [A \cup B] = R [A] \cup R [B]$ , $R [A \cap B] \subseteq R [A] \cap R [B]$ , $R [A] ∖ R [B] \subseteq R [A ∖ B]$ , $A \subseteq B$ implies $R [A] \subseteq R [B]$ , and $(S \circ R) [A] = S [R [A]]$

Statement

Let $R$ and $S$ be relations and $A$ , $B$ sets. Then

(i) $R [A \cup B] = R [A] \cup R [B]$ ;
(ii) $R [A \cap B] \subseteq R [A] \cap R [B]$ ;
(iii) $R [A] ∖ R [B] \subseteq R [A ∖ B]$ ;
(iv) if $A \subseteq B$ then $R [A] \subseteq R [B]$ ;
(v) $(S \circ R) [A] = S [R [A]]$ .

Facts & Assumptions

Given: relations $R$ and $S$ and sets $A$ , $B$ .

[L1]

$b \in R [A]$ holds if and only if $(a, b) \in R$ for some $a \in A$ (The image $R [A]$ and the preimage $R^{- 1} [B]$ of a set under a relation).

[L2]

$(a, c) \in S \circ R$ holds if and only if $(a, b) \in R$ and $(b, c) \in S$ for some $b$ (The inverse relation $R^{- 1}$ , the composite $S \circ R$ , and the restriction $R ↾ A$ ).

[L3]

$z \in a \cup b$ holds if and only if $z \in a$ or $z \in b$ ( $⋃ \emptyset = \emptyset$ , $⋃ {a} = a$ , $⋃ {a, b} = a \cup b$ , $⋂ {a} = a$ , and $⋂ {a, b} = a \cap b$ ).

[L4]

$z \in a \cap b$ holds if and only if $z \in a$ and $z \in b$ ( $⋃ \emptyset = \emptyset$ , $⋃ {a} = a$ , $⋃ {a, b} = a \cup b$ , $⋂ {a} = a$ , and $⋂ {a, b} = a \cap b$ ).

[L5]

$z \in a ∖ b$ holds exactly when $z \in a$ and $z \notin b$ (The difference $a ∖ b$ , the symmetric difference $a △ b$ , and the complement $X ∖ a$ relative to a set $X$ ).

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

If every $z$ satisfies $z \in x$ if and only if $z \in y$ , then $x = y$ (The Axiom of Extensionality: $\forall x \forall y (\forall z (z \in x \leftrightarrow z \in y) \to x = y)$ ).

[L8]

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

Proof

technique · direct

1.1

Claim (i): $c \in R [A \cup B]$ exactly when $(a, c) \in R$ for some $a$ with $a \in A$ or $a \in B$ ; that is exactly when $(a, c) \in R$ for some $a \in A$ , or $(a, c) \in R$ for some $a \in B$ , which is $c \in R [A] \cup R [B]$ .

L1L3L7

1.2

Claim (ii): if $c \in R [A \cap B]$ then $(a, c) \in R$ for some $a$ lying in both $A$ and $B$ ; that same $a$ witnesses $c \in R [A]$ and $c \in R [B]$ .

L1L4L6

1.3

Claim (iii): if $c \in R [A] ∖ R [B]$ then $(a, c) \in R$ for some $a \in A$ , and no element of $B$ is related to $c$ ; in particular that $a$ is not in $B$ , so $a \in A ∖ B$ and $c \in R [A ∖ B]$ .

L1L5L6

1.4

Claim (iv): if $A \subseteq B$ and $c \in R [A]$ then $(a, c) \in R$ for some $a \in A$ , and that $a$ lies in $B$ .

L1L6

1.5

Claim (v): $c \in (S \circ R) [A]$ exactly when $(a, c) \in S \circ R$ for some $a \in A$ , that is, exactly when there are $a \in A$ and $b$ with $(a, b) \in R$ and $(b, c) \in S$ ; and that says exactly that $(b, c) \in S$ for some $b \in R [A]$ , which is $c \in S [R [A]]$ .

L1L2L7L8

2.1

Claims (i) to (v) are established, which is the statement.

step 1.1step 1.2step 1.3step 1.4step 1.5∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

17 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

B. Kaya, MATH 320 Set Theory (METU), Def. 7 and Lemma 2 (standard reference, not scraped)
Image (mathematics) (Wikipedia) (standard reference, not scraped)
Composition of relations (Wikipedia) (standard reference, not scraped)

R[A∪B]=R[A]∪R[B]R[A∪B]=R[A]∪R[B], R[A∩B]⊆R[A]∩R[B]R[A∩B]⊆R[A]∩R[B], R[A]∖R[B]⊆R[A∖B]R[A]∖R[B]⊆R[A∖B], A⊆BA⊆B implies R[A]⊆R[B]R[A]⊆R[B], and (S∘R)[A]=S[R[A]](S∘R)[A]=S[R[A]]