Theorem frrlem6

Description: Lemma for well-founded recursion. The well-founded recursion generator is a relationship. (Contributed by Scott Fenton, 27-Aug-2022)

	Ref	Expression
Hypotheses	frrlem5.1	|- B = { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) }
	frrlem5.2	|- F = frecs ( R , A , G )
Assertion	frrlem6	|- Rel F

Proof

Step	Hyp	Ref	Expression
1		frrlem5.1	|- B = { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) }
2		frrlem5.2	|- F = frecs ( R , A , G )
3	1 2	frrlem5	|- F = U. B
4	3	releqi	|- ( Rel F <-> Rel U. B )
5		reluni	|- ( Rel U. B <-> A. g e. B Rel g )
6	4 5	bitri	|- ( Rel F <-> A. g e. B Rel g )
7	1	frrlem2	|- ( g e. B -> Fun g )
8		funrel	|- ( Fun g -> Rel g )
9	7 8	syl	|- ( g e. B -> Rel g )
10	6 9	mprgbir	|- Rel F