Theorem tfrlem6

Description: Lemma for transfinite recursion. The union of all acceptable functions is a relation. (Contributed by NM, 8-Aug-1994) (Revised by Mario Carneiro, 9-May-2015) Avoid ax-10 , ax-nul , ax-pr , ax-sep and ax-un . (Revised by Umit Teoman Dogan, 10-Jun-2026)

	Ref	Expression
Hypothesis	tfrlem.1	|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
Assertion	tfrlem6	|- Rel recs ( F )

Proof

Step	Hyp	Ref	Expression
1		tfrlem.1	|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
2		df-recs	|- recs ( F ) = wrecs ( _E , On , F )
3	2	wfrrel	|- Rel recs ( F )