Metamath Proof Explorer

Theorem frrlem3

Description: Lemma for 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 )