Theorem frrlem7

Description: Lemma for well-founded recursion. The well-founded recursion generator's domain is a subclass of A . (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	frrlem7	|- dom F C_ A

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	dmeqi	|- dom F = dom U. B
5		dmuni	|- dom U. B = U_ g e. B dom g
6	4 5	eqtri	|- dom F = U_ g e. B dom g
7	6	sseq1i	|- ( dom F C_ A <-> U_ g e. B dom g C_ A )
8		iunss	|- ( U_ g e. B dom g C_ A <-> A. g e. B dom g C_ A )
9	7 8	bitri	|- ( dom F C_ A <-> A. g e. B dom g C_ A )
10	1	frrlem3	|- ( g e. B -> dom g C_ A )
11	9 10	mprgbir	|- dom F C_ A