Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

T∘(S∘R)=(T∘S)∘RT \circ (S \circ R) = (T \circ S) \circ R, (S∘R)−1=R−1∘S−1(S \circ R)^{-1} = R^{-1} \circ S^{-1}, (R−1)−1=R(R^{-1})^{-1} = R, dom⁡(R−1)=ran⁡R\operatorname{dom}(R^{-1}) = \operatorname{ran} R, and ΔB∘R=R=R∘ΔA\Delta_B \circ R = R = R \circ \Delta_A for a relation RR from AA to BB

Statement

Let RR, SS, TT be relations and let AA, BB be sets. Then

  • (i) T∘(S∘R)=(T∘S)∘RT \circ (S \circ R) = (T \circ S) \circ R;
  • (ii) (S∘R)−1=R−1∘S−1(S \circ R)^{-1} = R^{-1} \circ S^{-1};
  • (iii) (R−1)−1=R(R^{-1})^{-1} = R;
  • (iv) dom⁡(R−1)=ran⁡R\operatorname{dom}(R^{-1}) = \operatorname{ran} R and ran⁡(R−1)=dom⁡R\operatorname{ran}(R^{-1}) = \operatorname{dom} R;
  • (v) if RR is a relation from AA to BB, then ΔB∘R=R\Delta_B \circ R = R and R∘ΔA=RR \circ \Delta_A = R.

Facts & Assumptions

Given: relations RR, SS, TT and sets AA, BB.

[L1]

(b,a)∈R−1(b,a) \in R^{-1} holds if and only if (a,b)∈R(a,b) \in R; (a,c)∈S∘R(a,c) \in S \circ R holds if and only if (a,b)∈R(a,b) \in R and (b,c)∈S(b,c) \in S for some bb (The inverse relation R−1R^{-1}, the composite S∘RS \circ R, and the restriction R↾AR \restriction A).

[L2]

A relation is a set RR every element of which is an ordered pair (Relation, dom⁡R\operatorname{dom} R, ran⁡R\operatorname{ran} R, fld⁡R\operatorname{fld} R, and the specialisations "relation from AA to BB" and "relation on AA").

[L3]

dom⁡R:={ a:∃b (a,b)∈R },ran⁡R:={ b:∃a (a,b)∈R }\operatorname{dom} R := \{\, a : \exists b\ (a,b) \in R \,\}, \qquad \operatorname{ran} R := \{\, b : \exists a\ (a,b) \in R \,\} (Relation, dom⁡R\operatorname{dom} R, ran⁡R\operatorname{ran} R, fld⁡R\operatorname{fld} R, and the specialisations "relation from AA to BB" and "relation on AA").

[L4]

(a,b)∈ΔA(a,b) \in \Delta_A holds if and only if a=ba = b and a∈Aa \in A (The identity relation ΔA={ (a,b)∈A×A:a=b }\Delta_A = \{\,(a,b) \in A \times A : a = b\,\} and the membership relation ∈A ={ (a,b)∈A×A:a∈b }\in_A\, = \{\,(a,b) \in A \times A : a \in b\,\}).

[L5]

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

[L6]

If every zz satisfies z∈xz \in x if and only if z∈yz \in y, then x=yx = y (The Axiom of Extensionality: ∀x ∀y (∀z (z∈x↔z∈y)→x=y)\forall x\,\forall y\,(\forall z\,(z \in x \leftrightarrow z \in y) \to x = y)).

[L7]

R⊆A×BR \subseteq A \times B if and only if dom⁡R⊆A\operatorname{dom} R \subseteq A and ran⁡R⊆B\operatorname{ran} R \subseteq B (Every relation RR satisfies R⊆dom⁡R×ran⁡RR \subseteq \operatorname{dom} R \times \operatorname{ran} R, and RR is a relation from AA to BB if and only if dom⁡R⊆A\operatorname{dom} R \subseteq A and ran⁡R⊆B\operatorname{ran} R \subseteq B).

[L8]

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

Proof

technique · direct
1.1

Claim (i): every element of either side is an ordered pair, and (a,d)(a,d) lies in T∘(S∘R)T \circ (S \circ R) exactly when there is cc with (a,c)∈S∘R(a,c) \in S \circ R and (c,d)∈T(c,d) \in T, that is, exactly when there are bb and cc with (a,b)∈R(a,b) \in R, (b,c)∈S(b,c) \in S and (c,d)∈T(c,d) \in T. Reading the same condition with the middle pair grouped the other way gives membership in (T∘S)∘R(T \circ S) \circ R.

L1L2L5L6L8
1.2

Claim (ii): (c,a)∈(S∘R)−1(c,a) \in (S \circ R)^{-1} exactly when (a,c)∈S∘R(a,c) \in S \circ R, that is, exactly when there is bb with (a,b)∈R(a,b) \in R and (b,c)∈S(b,c) \in S; and that says exactly that (c,b)∈S−1(c,b) \in S^{-1} and (b,a)∈R−1(b,a) \in R^{-1} for some bb, which is (c,a)∈R−1∘S−1(c,a) \in R^{-1} \circ S^{-1}.

L1L2L5L6L8
1.3

Claim (iii): every element of RR is an ordered pair (a,b)(a,b), and (a,b)∈(R−1)−1(a,b) \in (R^{-1})^{-1} exactly when (b,a)∈R−1(b,a) \in R^{-1}, exactly when (a,b)∈R(a,b) \in R; both sides consist of ordered pairs, so they are equal.

L1L2L5L6L8
1.4

Claim (iv): a∈dom⁡(R−1)a \in \operatorname{dom}(R^{-1}) exactly when (a,b)∈R−1(a,b) \in R^{-1} for some bb, exactly when (b,a)∈R(b,a) \in R for some bb, exactly when a∈ran⁡Ra \in \operatorname{ran} R; the second identity is the same argument with the coordinates exchanged.

L1L3L6
2.1

Claim (v): let RR be a relation from AA to BB, so dom⁡R⊆A\operatorname{dom} R \subseteq A and ran⁡R⊆B\operatorname{ran} R \subseteq B. Then (a,c)∈ΔB∘R(a,c) \in \Delta_B \circ R exactly when there is bb with (a,b)∈R(a,b) \in R and b=c∈Bb = c \in B, that is, exactly when (a,c)∈R(a,c) \in R and c∈Bc \in B; and (a,c)∈R(a,c) \in R already forces c∈ran⁡R⊆Bc \in \operatorname{ran} R \subseteq B, so the two sets are equal. Symmetrically (a,c)∈R∘ΔA(a,c) \in R \circ \Delta_A exactly when a∈Aa \in A and (a,c)∈R(a,c) \in R, and (a,c)∈R(a,c) \in R forces a∈dom⁡R⊆Aa \in \operatorname{dom} R \subseteq A.

L1L3L4L6L7step 1.4
3.1

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

step 1.1step 1.2step 1.3step 1.4step 2.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 20 results over 10 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources