Theorem relttrcl

Description: The transitive closure of a class is a relation. (Contributed by Scott Fenton, 17-Oct-2024)

	Ref	Expression
Assertion	relttrcl	$$⊢\mathrm{Rel}\mathrm{t++}R$$

Proof

Step	Hyp	Ref	Expression
1		df-ttrcl	$$⊢\mathrm{t++}R=\left\{⟨x,y⟩|\exists n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall m\in nf\left(m\right)Rf\left(\mathrm{suc}m\right)\right)\right\}$$
2	1	relopabi	$$⊢\mathrm{Rel}\mathrm{t++}R$$