Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  frrlem1 Structured version   Unicode version

Theorem frrlem1 25575
Description: Lemma for founded recursion. The final item we are interested in is the union of acceptable functions  B. This lemma just changes bound variables for later use. (Contributed by Paul Chapman, 21-Apr-2012.)
Hypothesis
Ref Expression
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
Ref Expression
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 ) ) ) ) ) }
Distinct variable groups:    A, f,
g, w, x, y, z    f, G, g, w, x, y, z    R, f, g, w, x, y, z
Allowed substitution hints:    B( x, y, z, w, f, g)

Proof of Theorem frrlem1
StepHypRef Expression
1 frrlem1.1 . 2  |-  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 fneq1 5527 . . . . . 6  |-  ( f  =  g  ->  (
f  Fn  x  <->  g  Fn  x ) )
3 fveq1 5720 . . . . . . . . 9  |-  ( f  =  g  ->  (
f `  y )  =  ( g `  y ) )
4 reseq1 5133 . . . . . . . . . 10  |-  ( f  =  g  ->  (
f  |`  Pred ( R ,  A ,  y )
)  =  ( g  |`  Pred ( R ,  A ,  y )
) )
54oveq2d 6090 . . . . . . . . 9  |-  ( f  =  g  ->  (
y G ( f  |`  Pred ( R ,  A ,  y )
) )  =  ( y G ( g  |`  Pred ( R ,  A ,  y )
) ) )
63, 5eqeq12d 2450 . . . . . . . 8  |-  ( f  =  g  ->  (
( f `  y
)  =  ( y G ( f  |`  Pred ( R ,  A ,  y ) ) )  <->  ( g `  y )  =  ( y G ( g  |`  Pred ( R ,  A ,  y )
) ) ) )
76ralbidv 2718 . . . . . . 7  |-  ( f  =  g  ->  ( A. y  e.  x  ( f `  y
)  =  ( y G ( f  |`  Pred ( R ,  A ,  y ) ) )  <->  A. y  e.  x  ( g `  y
)  =  ( y G ( g  |`  Pred ( R ,  A ,  y ) ) ) ) )
873anbi3d 1260 . . . . . 6  |-  ( f  =  g  ->  (
( 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 )
) ) )  <->  ( x  C_  A  /\  A. y  e.  x  Pred ( R ,  A ,  y )  C_  x  /\  A. y  e.  x  ( g `  y )  =  ( y G ( g  |`  Pred ( R ,  A , 
y ) ) ) ) ) )
92, 8anbi12d 692 . . . . 5  |-  ( f  =  g  ->  (
( 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 )
) ) ) )  <-> 
( g  Fn  x  /\  ( x  C_  A  /\  A. y  e.  x  Pred ( R ,  A ,  y )  C_  x  /\  A. y  e.  x  ( g `  y )  =  ( y G ( g  |`  Pred ( R ,  A ,  y )
) ) ) ) ) )
109exbidv 1636 . . . 4  |-  ( f  =  g  ->  ( 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 ) ) ) ) )  <->  E. x
( g  Fn  x  /\  ( x  C_  A  /\  A. y  e.  x  Pred ( R ,  A ,  y )  C_  x  /\  A. y  e.  x  ( g `  y )  =  ( y G ( g  |`  Pred ( R ,  A ,  y )
) ) ) ) ) )
11 fneq2 5528 . . . . . 6  |-  ( x  =  z  ->  (
g  Fn  x  <->  g  Fn  z ) )
12 sseq1 3362 . . . . . . 7  |-  ( x  =  z  ->  (
x  C_  A  <->  z  C_  A ) )
13 sseq2 3363 . . . . . . . . 9  |-  ( x  =  z  ->  ( Pred ( R ,  A ,  y )  C_  x 
<-> 
Pred ( R ,  A ,  y )  C_  z ) )
1413raleqbi1dv 2905 . . . . . . . 8  |-  ( x  =  z  ->  ( A. y  e.  x  Pred ( R ,  A ,  y )  C_  x 
<-> 
A. y  e.  z 
Pred ( R ,  A ,  y )  C_  z ) )
15 predeq3 25436 . . . . . . . . . 10  |-  ( y  =  w  ->  Pred ( R ,  A , 
y )  =  Pred ( R ,  A ,  w ) )
1615sseq1d 3368 . . . . . . . . 9  |-  ( y  =  w  ->  ( Pred ( R ,  A ,  y )  C_  z 
<-> 
Pred ( R ,  A ,  w )  C_  z ) )
1716cbvralv 2925 . . . . . . . 8  |-  ( A. y  e.  z  Pred ( R ,  A , 
y )  C_  z  <->  A. w  e.  z  Pred ( R ,  A ,  w )  C_  z
)
1814, 17syl6bb 253 . . . . . . 7  |-  ( x  =  z  ->  ( A. y  e.  x  Pred ( R ,  A ,  y )  C_  x 
<-> 
A. w  e.  z 
Pred ( R ,  A ,  w )  C_  z ) )
19 raleq 2897 . . . . . . . 8  |-  ( x  =  z  ->  ( A. y  e.  x  ( g `  y
)  =  ( y G ( g  |`  Pred ( R ,  A ,  y ) ) )  <->  A. y  e.  z  ( g `  y
)  =  ( y G ( g  |`  Pred ( R ,  A ,  y ) ) ) ) )
20 fveq2 5721 . . . . . . . . . 10  |-  ( y  =  w  ->  (
g `  y )  =  ( g `  w ) )
21 id 20 . . . . . . . . . . 11  |-  ( y  =  w  ->  y  =  w )
2215reseq2d 5139 . . . . . . . . . . 11  |-  ( y  =  w  ->  (
g  |`  Pred ( R ,  A ,  y )
)  =  ( g  |`  Pred ( R ,  A ,  w )
) )
2321, 22oveq12d 6092 . . . . . . . . . 10  |-  ( y  =  w  ->  (
y G ( g  |`  Pred ( R ,  A ,  y )
) )  =  ( w G ( g  |`  Pred ( R ,  A ,  w )
) ) )
2420, 23eqeq12d 2450 . . . . . . . . 9  |-  ( y  =  w  ->  (
( g `  y
)  =  ( y G ( g  |`  Pred ( R ,  A ,  y ) ) )  <->  ( g `  w )  =  ( w G ( g  |`  Pred ( R ,  A ,  w )
) ) ) )
2524cbvralv 2925 . . . . . . . 8  |-  ( A. y  e.  z  (
g `  y )  =  ( y G ( g  |`  Pred ( R ,  A , 
y ) ) )  <->  A. w  e.  z 
( g `  w
)  =  ( w G ( g  |`  Pred ( R ,  A ,  w ) ) ) )
2619, 25syl6bb 253 . . . . . . 7  |-  ( x  =  z  ->  ( A. y  e.  x  ( g `  y
)  =  ( y G ( g  |`  Pred ( R ,  A ,  y ) ) )  <->  A. w  e.  z  ( g `  w
)  =  ( w G ( g  |`  Pred ( R ,  A ,  w ) ) ) ) )
2712, 18, 263anbi123d 1254 . . . . . 6  |-  ( x  =  z  ->  (
( x  C_  A  /\  A. y  e.  x  Pred ( R ,  A ,  y )  C_  x  /\  A. y  e.  x  ( g `  y )  =  ( y G ( g  |`  Pred ( R ,  A ,  y )
) ) )  <->  ( 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 ) ) ) ) ) )
2811, 27anbi12d 692 . . . . 5  |-  ( x  =  z  ->  (
( g  Fn  x  /\  ( x  C_  A  /\  A. y  e.  x  Pred ( R ,  A ,  y )  C_  x  /\  A. y  e.  x  ( g `  y )  =  ( y G ( g  |`  Pred ( R ,  A ,  y )
) ) ) )  <-> 
( 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 )
) ) ) ) ) )
2928cbvexv 1985 . . . 4  |-  ( E. x ( g  Fn  x  /\  ( x 
C_  A  /\  A. y  e.  x  Pred ( R ,  A , 
y )  C_  x  /\  A. y  e.  x  ( g `  y
)  =  ( y G ( g  |`  Pred ( R ,  A ,  y ) ) ) ) )  <->  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 )
) ) ) ) )
3010, 29syl6bb 253 . . 3  |-  ( f  =  g  ->  ( 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 ) ) ) ) )  <->  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 )
) ) ) ) ) )
3130cbvabv 2555 . 2  |-  { 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 ) ) ) ) ) }  =  { 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 ) ) ) ) ) }
321, 31eqtri 2456 1  |-  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 ) ) ) ) ) }
Colors of variables: wff set class
Syntax hints:    /\ wa 359    /\ w3a 936   E.wex 1550    = wceq 1652   {cab 2422   A.wral 2698    C_ wss 3313    |` cres 4873    Fn wfn 5442   ` cfv 5447  (class class class)co 6074   Predcpred 25431
This theorem is referenced by:  frrlem2  25576  frrlem3  25577  frrlem4  25578  frrlem5e  25583
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ral 2703  df-rex 2704  df-rab 2707  df-v 2951  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-nul 3622  df-if 3733  df-sn 3813  df-pr 3814  df-op 3816  df-uni 4009  df-br 4206  df-opab 4260  df-xp 4877  df-rel 4878  df-cnv 4879  df-co 4880  df-dm 4881  df-rn 4882  df-res 4883  df-ima 4884  df-iota 5411  df-fun 5449  df-fn 5450  df-fv 5455  df-ov 6077  df-pred 25432
  Copyright terms: Public domain W3C validator