This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem relttrcl

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

Ref Expression
Assertion relttrcl ⊢ Rel ⁡ t++ R

Proof

Step Hyp Ref Expression
1 df-ttrcl ⊢ t++ R = x y | ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = x ∧ f ⁡ n = y ∧ ∀ m ∈ n f ⁡ m R f ⁡ suc ⁡ m
2 1 relopabi ⊢ Rel ⁡ t++ R