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

Theorem frrlem1 25298
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 5467 . . . . . 6  |-  ( f  =  g  ->  (
f  Fn  x  <->  g  Fn  x ) )
3 fveq1 5660 . . . . . . . . 9  |-  ( f  =  g  ->  (
f `  y )  =  ( g `  y ) )
4 reseq1 5073 . . . . . . . . . 10  |-  ( f  =  g  ->  (
f  |`  Pred ( R ,  A ,  y )
)  =  ( g  |`  Pred ( R ,  A ,  y )
) )
54oveq2d 6029 . . . . . . . . 9  |-  ( f  =  g  ->  (
y G ( f  |`  Pred ( R ,  A ,  y )
) )  =  ( y G ( g  |`  Pred ( R ,  A ,  y )
) ) )
63, 5eqeq12d 2394 . . . . . . . 8  |-  ( f  =  g  ->  (
( f `  y
)  =  ( y G ( f  |`  Pred ( R ,  A ,  y ) ) )  <->  ( g `  y )  =  ( y G ( g  |`  Pred ( R ,  A ,  y )
) ) ) )
76ralbidv 2662 . . . . . . 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 1633 . . . 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 5468 . . . . . 6  |-  ( x  =  z  ->  (
g  Fn  x  <->  g  Fn  z ) )
12 sseq1 3305 . . . . . . 7  |-  ( x  =  z  ->  (
x  C_  A  <->  z  C_  A ) )
13 sseq2 3306 . . . . . . . . 9  |-  ( x  =  z  ->  ( Pred ( R ,  A ,  y )  C_  x 
<-> 
Pred ( R ,  A ,  y )  C_  z ) )
1413raleqbi1dv 2848 . . . . . . . 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 25188 . . . . . . . . . 10  |-  ( y  =  w  ->  Pred ( R ,  A , 
y )  =  Pred ( R ,  A ,  w ) )
1615sseq1d 3311 . . . . . . . . 9  |-  ( y  =  w  ->  ( Pred ( R ,  A ,  y )  C_  z 
<-> 
Pred ( R ,  A ,  w )  C_  z ) )
1716cbvralv 2868 . . . . . . . 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 2840 . . . . . . . 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 5661 . . . . . . . . . 10  |-  ( y  =  w  ->  (
g `  y )  =  ( g `  w ) )
21 id 20 . . . . . . . . . . 11  |-  ( y  =  w  ->  y  =  w )
2215reseq2d 5079 . . . . . . . . . . 11  |-  ( y  =  w  ->  (
g  |`  Pred ( R ,  A ,  y )
)  =  ( g  |`  Pred ( R ,  A ,  w )
) )
2321, 22oveq12d 6031 . . . . . . . . . 10  |-  ( y  =  w  ->  (
y G ( g  |`  Pred ( R ,  A ,  y )
) )  =  ( w G ( g  |`  Pred ( R ,  A ,  w )
) ) )
2420, 23eqeq12d 2394 . . . . . . . . 9  |-  ( y  =  w  ->  (
( g `  y
)  =  ( y G ( g  |`  Pred ( R ,  A ,  y ) ) )  <->  ( g `  w )  =  ( w G ( g  |`  Pred ( R ,  A ,  w )
) ) ) )
2524cbvralv 2868 . . . . . . . 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 2029 . . . 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 2499 . 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 2400 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 1547    = wceq 1649   {cab 2366   A.wral 2642    C_ wss 3256    |` cres 4813    Fn wfn 5382   ` cfv 5387  (class class class)co 6013   Predcpred 25184
This theorem is referenced by:  frrlem2  25299  frrlem3  25300  frrlem4  25301  frrlem5e  25306
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ral 2647  df-rex 2648  df-rab 2651  df-v 2894  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-nul 3565  df-if 3676  df-sn 3756  df-pr 3757  df-op 3759  df-uni 3951  df-br 4147  df-opab 4201  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5351  df-fun 5389  df-fn 5390  df-fv 5395  df-ov 6016  df-pred 25185
  Copyright terms: Public domain W3C validator