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)

	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		reluni	|- ( Rel U. A <-> A. g e. A Rel g )
3	1	tfrlem4	|- ( g e. A -> Fun g )
4		funrel	|- ( Fun g -> Rel g )
5	3 4	syl	|- ( g e. A -> Rel g )
6	2 5	mprgbir	|- Rel U. A
7	1	recsfval	|- recs ( F ) = U. A
8	7	releqi	|- ( Rel recs ( F ) <-> Rel U. A )
9	6 8	mpbir	|- Rel recs ( F )