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 >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. m e. n ( f ` m ) R ( f ` suc m ) ) }
2 1 relopabi 
 |-  Rel t++ R