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++ 𝑅

Proof

Step	Hyp	Ref	Expression
1		df-ttrcl	⊢ t++ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ) }
2	1	relopabi	⊢ Rel t++ 𝑅