Theorem relttrcl

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

	Ref	Expression
Assertion	relttrcl	Could not format assertion : No typesetting found for |- Rel t++ R with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-ttrcl	Could not format 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 ) ) } : No typesetting found for |- 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 ) ) } with typecode |-
2	1	relopabi	Could not format Rel t++ R : No typesetting found for |- Rel t++ R with typecode |-