Transitive Closure of Set-Like Relation is Set-Like

Theorem

Let $A$ be a class.

Let $\RR$ be a set-like endorelation on $A$.

Let $\RR^+$ be the transitive closure of $\RR$.

Then $\RR^+$ is also a set-like relation.

Proof

Let $x \in A$.

Let $A'$ be the class of all subsets of $A$.

For each $s \in A'$, $\RR^{-1}$ is a subset of $A$.

Hence by Inverse Image of Set under Set-Like Relation is Set and the definition of endorelation:

$\RR^{-1} \in A'$

Define a mapping $G: A' \to A'$ as:

$\forall s \in A': \map G s = \map {\RR^{-1} } s$

Recursively define a mapping $f: \N \to A'$ as follows:

$\map f n = \begin {cases} \set x & : n = 0 \\ \map G {\map f {n - 1} } & : n > 0 \end {cases}$

By the Axiom of Infinity and the Axiom of Replacement:

$\map f \N$ is a set.

Thus by the Axiom of Unions:

$\ds \bigcup \map f \N$ is a set.

Let $y \in \map {\paren {\RR^+}^{-1} } x$.

By the definition of transitive closure:

for some $n \in \N_{>0}$ there are $a_0, a_1, \dots, a_n$ such that $y = a_0 \mathrel \RR a_1 \mathrel \RR \cdots \mathrel \RR a_n = x$.

This article, or a section of it, needs explaining. In particular: it's a finite sort of induction, and a simple and common pattern. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Explain}} from the code.

Then by induction (working from $n$ to $0$), $\ds a_n, a_{n - 1}, \dots, a_0 \in \bigcup \map f \N$.

As this holds for all such $y$:

$\ds \map {\paren {\RR^+}^{-1} } x \subseteq \bigcup \map f \N$

By the Axiom of Specification:

$\map {\paren {\RR^+}^{-1} } x$ is a set.

As this holds for all $x \in A$:

$\RR^+$ is a set-like relation.

$\blacksquare$