Theorem frrlem3

Description: Lemma for well-founded recursion. An acceptable function's domain is a subset of A . (Contributed by Paul Chapman, 21-Apr-2012)

	Ref	Expression
Hypothesis	frrlem1.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 ) ) ) ) }
Assertion	frrlem3	|- ( g e. B -> dom g C_ A )

Proof

Step	Hyp	Ref	Expression
1		frrlem1.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	1	frrlem1	|- B = { g | E. z ( g Fn z /\ ( z C_ A /\ A. w e. z Pred ( R , A , w ) C_ z ) /\ A. w e. z ( g ` w ) = ( w G ( g |` Pred ( R , A , w ) ) ) ) }
3	2	abeq2i	|- ( g e. B <-> E. z ( g Fn z /\ ( z C_ A /\ A. w e. z Pred ( R , A , w ) C_ z ) /\ A. w e. z ( g ` w ) = ( w G ( g |` Pred ( R , A , w ) ) ) ) )
4		fndm	|- ( g Fn z -> dom g = z )
5	4	sseq1d	|- ( g Fn z -> ( dom g C_ A <-> z C_ A ) )
6	5	biimpar	|- ( ( g Fn z /\ z C_ A ) -> dom g C_ A )
7	6	adantrr	|- ( ( g Fn z /\ ( z C_ A /\ A. w e. z Pred ( R , A , w ) C_ z ) ) -> dom g C_ A )
8	7	3adant3	|- ( ( g Fn z /\ ( z C_ A /\ A. w e. z Pred ( R , A , w ) C_ z ) /\ A. w e. z ( g ` w ) = ( w G ( g |` Pred ( R , A , w ) ) ) ) -> dom g C_ A )
9	8	exlimiv	|- ( E. z ( g Fn z /\ ( z C_ A /\ A. w e. z Pred ( R , A , w ) C_ z ) /\ A. w e. z ( g ` w ) = ( w G ( g |` Pred ( R , A , w ) ) ) ) -> dom g C_ A )
10	3 9	sylbi	|- ( g e. B -> dom g C_ A )