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

Theorem wfrlem4 25473
Description: Lemma for well-founded recursion. Properties of the restriction of an acceptable function to the domain of another one. (Contributed by Scott Fenton, 21-Apr-2011.)
Hypotheses
Ref Expression
wfrlem4.1  |-  R  We  A
wfrlem4.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 )  =  ( G `  ( f  |`  Pred ( R ,  A ,  y )
) ) ) }
Assertion
Ref Expression
wfrlem4  |-  ( ( g  e.  B  /\  h  e.  B )  ->  ( ( g  |`  ( dom  g  i^i  dom  h ) )  Fn  ( dom  g  i^i 
dom  h )  /\  A. a  e.  ( dom  g  i^i  dom  h
) ( ( g  |`  ( dom  g  i^i 
dom  h ) ) `
 a )  =  ( G `  (
( g  |`  ( dom  g  i^i  dom  h
) )  |`  Pred ( R ,  ( dom  g  i^i  dom  h ) ,  a ) ) ) ) )
Distinct variable groups:    A, a,
f, g, h, x, y    B, a    G, a, f, g, h, x, y    R, a, f, g, h, x, y
Allowed substitution hints:    B( x, y, f, g, h)

Proof of Theorem wfrlem4
Dummy variables  b 
c are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wfrlem4.2 . . . . . 6  |-  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 )  =  ( G `  ( f  |`  Pred ( R ,  A ,  y )
) ) ) }
21wfrlem2 25471 . . . . 5  |-  ( g  e.  B  ->  Fun  g )
3 funfn 5441 . . . . 5  |-  ( Fun  g  <->  g  Fn  dom  g )
42, 3sylib 189 . . . 4  |-  ( g  e.  B  ->  g  Fn  dom  g )
5 fnresin1 5518 . . . 4  |-  ( g  Fn  dom  g  -> 
( g  |`  ( dom  g  i^i  dom  h
) )  Fn  ( dom  g  i^i  dom  h
) )
64, 5syl 16 . . 3  |-  ( g  e.  B  ->  (
g  |`  ( dom  g  i^i  dom  h ) )  Fn  ( dom  g  i^i  dom  h ) )
76adantr 452 . 2  |-  ( ( g  e.  B  /\  h  e.  B )  ->  ( g  |`  ( dom  g  i^i  dom  h
) )  Fn  ( dom  g  i^i  dom  h
) )
8 inss1 3521 . . . . . . . 8  |-  ( dom  g  i^i  dom  h
)  C_  dom  g
98sseli 3304 . . . . . . 7  |-  ( a  e.  ( dom  g  i^i  dom  h )  -> 
a  e.  dom  g
)
101wfrlem1 25470 . . . . . . . . 9  |-  B  =  { g  |  E. b ( g  Fn  b  /\  ( b 
C_  A  /\  A. a  e.  b  Pred ( R ,  A , 
a )  C_  b
)  /\  A. a  e.  b  ( g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A ,  a )
) ) ) }
1110abeq2i 2511 . . . . . . . 8  |-  ( g  e.  B  <->  E. b
( g  Fn  b  /\  ( b  C_  A  /\  A. a  e.  b 
Pred ( R ,  A ,  a )  C_  b )  /\  A. a  e.  b  (
g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A , 
a ) ) ) ) )
12 fndm 5503 . . . . . . . . . . . . 13  |-  ( g  Fn  b  ->  dom  g  =  b )
1312raleqdv 2870 . . . . . . . . . . . 12  |-  ( g  Fn  b  ->  ( A. a  e.  dom  g ( g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A ,  a )
) )  <->  A. a  e.  b  ( g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A ,  a )
) ) ) )
1413biimpar 472 . . . . . . . . . . 11  |-  ( ( g  Fn  b  /\  A. a  e.  b  ( g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A , 
a ) ) ) )  ->  A. a  e.  dom  g ( g `
 a )  =  ( G `  (
g  |`  Pred ( R ,  A ,  a )
) ) )
15 rsp 2726 . . . . . . . . . . 11  |-  ( A. a  e.  dom  g ( g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A , 
a ) ) )  ->  ( a  e. 
dom  g  ->  (
g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A , 
a ) ) ) ) )
1614, 15syl 16 . . . . . . . . . 10  |-  ( ( g  Fn  b  /\  A. a  e.  b  ( g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A , 
a ) ) ) )  ->  ( a  e.  dom  g  ->  (
g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A , 
a ) ) ) ) )
17163adant2 976 . . . . . . . . 9  |-  ( ( g  Fn  b  /\  ( b  C_  A  /\  A. a  e.  b 
Pred ( R ,  A ,  a )  C_  b )  /\  A. a  e.  b  (
g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A , 
a ) ) ) )  ->  ( a  e.  dom  g  ->  (
g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A , 
a ) ) ) ) )
1817exlimiv 1641 . . . . . . . 8  |-  ( E. b ( g  Fn  b  /\  ( b 
C_  A  /\  A. a  e.  b  Pred ( R ,  A , 
a )  C_  b
)  /\  A. a  e.  b  ( g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A ,  a )
) ) )  -> 
( a  e.  dom  g  ->  ( g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A ,  a )
) ) ) )
1911, 18sylbi 188 . . . . . . 7  |-  ( g  e.  B  ->  (
a  e.  dom  g  ->  ( g `  a
)  =  ( G `
 ( g  |`  Pred ( R ,  A ,  a ) ) ) ) )
209, 19syl5 30 . . . . . 6  |-  ( g  e.  B  ->  (
a  e.  ( dom  g  i^i  dom  h
)  ->  ( g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A ,  a )
) ) ) )
2120imp 419 . . . . 5  |-  ( ( g  e.  B  /\  a  e.  ( dom  g  i^i  dom  h )
)  ->  ( g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A ,  a )
) ) )
2221adantlr 696 . . . 4  |-  ( ( ( g  e.  B  /\  h  e.  B
)  /\  a  e.  ( dom  g  i^i  dom  h ) )  -> 
( g `  a
)  =  ( G `
 ( g  |`  Pred ( R ,  A ,  a ) ) ) )
23 fvres 5704 . . . . 5  |-  ( a  e.  ( dom  g  i^i  dom  h )  -> 
( ( g  |`  ( dom  g  i^i  dom  h ) ) `  a )  =  ( g `  a ) )
2423adantl 453 . . . 4  |-  ( ( ( g  e.  B  /\  h  e.  B
)  /\  a  e.  ( dom  g  i^i  dom  h ) )  -> 
( ( g  |`  ( dom  g  i^i  dom  h ) ) `  a )  =  ( g `  a ) )
25 resres 5118 . . . . . 6  |-  ( ( g  |`  ( dom  g  i^i  dom  h )
)  |`  Pred ( R , 
( dom  g  i^i  dom  h ) ,  a ) )  =  ( g  |`  ( ( dom  g  i^i  dom  h
)  i^i  Pred ( R ,  ( dom  g  i^i  dom  h ) ,  a ) ) )
26 predss 25387 . . . . . . . . 9  |-  Pred ( R ,  ( dom  g  i^i  dom  h ) ,  a )  C_  ( dom  g  i^i  dom  h )
27 sseqin2 3520 . . . . . . . . 9  |-  ( Pred ( R ,  ( dom  g  i^i  dom  h ) ,  a )  C_  ( dom  g  i^i  dom  h )  <->  ( ( dom  g  i^i 
dom  h )  i^i 
Pred ( R , 
( dom  g  i^i  dom  h ) ,  a ) )  =  Pred ( R ,  ( dom  g  i^i  dom  h
) ,  a ) )
2826, 27mpbi 200 . . . . . . . 8  |-  ( ( dom  g  i^i  dom  h )  i^i  Pred ( R ,  ( dom  g  i^i  dom  h
) ,  a ) )  =  Pred ( R ,  ( dom  g  i^i  dom  h ) ,  a )
291wfrlem1 25470 . . . . . . . . . . . 12  |-  B  =  { h  |  E. c ( h  Fn  c  /\  ( c 
C_  A  /\  A. a  e.  c  Pred ( R ,  A , 
a )  C_  c
)  /\  A. a  e.  c  ( h `  a )  =  ( G `  ( h  |`  Pred ( R ,  A ,  a )
) ) ) }
3029abeq2i 2511 . . . . . . . . . . 11  |-  ( h  e.  B  <->  E. c
( h  Fn  c  /\  ( c  C_  A  /\  A. a  e.  c 
Pred ( R ,  A ,  a )  C_  c )  /\  A. a  e.  c  (
h `  a )  =  ( G `  ( h  |`  Pred ( R ,  A , 
a ) ) ) ) )
31 3an6 1264 . . . . . . . . . . . . . 14  |-  ( ( ( g  Fn  b  /\  h  Fn  c
)  /\  ( (
b  C_  A  /\  A. a  e.  b  Pred ( R ,  A , 
a )  C_  b
)  /\  ( c  C_  A  /\  A. a  e.  c  Pred ( R ,  A ,  a )  C_  c )
)  /\  ( A. a  e.  b  (
g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A , 
a ) ) )  /\  A. a  e.  c  ( h `  a )  =  ( G `  ( h  |`  Pred ( R ,  A ,  a )
) ) ) )  <-> 
( ( g  Fn  b  /\  ( b 
C_  A  /\  A. a  e.  b  Pred ( R ,  A , 
a )  C_  b
)  /\  A. a  e.  b  ( g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A ,  a )
) ) )  /\  ( h  Fn  c  /\  ( c  C_  A  /\  A. a  e.  c 
Pred ( R ,  A ,  a )  C_  c )  /\  A. a  e.  c  (
h `  a )  =  ( G `  ( h  |`  Pred ( R ,  A , 
a ) ) ) ) ) )
32312exbii 1590 . . . . . . . . . . . . 13  |-  ( E. b E. c ( ( g  Fn  b  /\  h  Fn  c
)  /\  ( (
b  C_  A  /\  A. a  e.  b  Pred ( R ,  A , 
a )  C_  b
)  /\  ( c  C_  A  /\  A. a  e.  c  Pred ( R ,  A ,  a )  C_  c )
)  /\  ( A. a  e.  b  (
g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A , 
a ) ) )  /\  A. a  e.  c  ( h `  a )  =  ( G `  ( h  |`  Pred ( R ,  A ,  a )
) ) ) )  <->  E. b E. c ( ( g  Fn  b  /\  ( b  C_  A  /\  A. a  e.  b 
Pred ( R ,  A ,  a )  C_  b )  /\  A. a  e.  b  (
g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A , 
a ) ) ) )  /\  ( h  Fn  c  /\  (
c  C_  A  /\  A. a  e.  c  Pred ( R ,  A , 
a )  C_  c
)  /\  A. a  e.  c  ( h `  a )  =  ( G `  ( h  |`  Pred ( R ,  A ,  a )
) ) ) ) )
33 eeanv 1933 . . . . . . . . . . . . 13  |-  ( E. b E. c ( ( g  Fn  b  /\  ( b  C_  A  /\  A. a  e.  b 
Pred ( R ,  A ,  a )  C_  b )  /\  A. a  e.  b  (
g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A , 
a ) ) ) )  /\  ( h  Fn  c  /\  (
c  C_  A  /\  A. a  e.  c  Pred ( R ,  A , 
a )  C_  c
)  /\  A. a  e.  c  ( h `  a )  =  ( G `  ( h  |`  Pred ( R ,  A ,  a )
) ) ) )  <-> 
( E. b ( g  Fn  b  /\  ( b  C_  A  /\  A. a  e.  b 
Pred ( R ,  A ,  a )  C_  b )  /\  A. a  e.  b  (
g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A , 
a ) ) ) )  /\  E. c
( h  Fn  c  /\  ( c  C_  A  /\  A. a  e.  c 
Pred ( R ,  A ,  a )  C_  c )  /\  A. a  e.  c  (
h `  a )  =  ( G `  ( h  |`  Pred ( R ,  A , 
a ) ) ) ) ) )
3432, 33bitri 241 . . . . . . . . . . . 12  |-  ( E. b E. c ( ( g  Fn  b  /\  h  Fn  c
)  /\  ( (
b  C_  A  /\  A. a  e.  b  Pred ( R ,  A , 
a )  C_  b
)  /\  ( c  C_  A  /\  A. a  e.  c  Pred ( R ,  A ,  a )  C_  c )
)  /\  ( A. a  e.  b  (
g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A , 
a ) ) )  /\  A. a  e.  c  ( h `  a )  =  ( G `  ( h  |`  Pred ( R ,  A ,  a )
) ) ) )  <-> 
( E. b ( g  Fn  b  /\  ( b  C_  A  /\  A. a  e.  b 
Pred ( R ,  A ,  a )  C_  b )  /\  A. a  e.  b  (
g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A , 
a ) ) ) )  /\  E. c
( h  Fn  c  /\  ( c  C_  A  /\  A. a  e.  c 
Pred ( R ,  A ,  a )  C_  c )  /\  A. a  e.  c  (
h `  a )  =  ( G `  ( h  |`  Pred ( R ,  A , 
a ) ) ) ) ) )
35 ssinss1 3529 . . . . . . . . . . . . . . . . . 18  |-  ( b 
C_  A  ->  (
b  i^i  c )  C_  A )
3635ad2antrr 707 . . . . . . . . . . . . . . . . 17  |-  ( ( ( b  C_  A  /\  A. a  e.  b 
Pred ( R ,  A ,  a )  C_  b )  /\  (
c  C_  A  /\  A. a  e.  c  Pred ( R ,  A , 
a )  C_  c
) )  ->  (
b  i^i  c )  C_  A )
37 nfra1 2716 . . . . . . . . . . . . . . . . . . . 20  |-  F/ a A. a  e.  b 
Pred ( R ,  A ,  a )  C_  b
38 nfra1 2716 . . . . . . . . . . . . . . . . . . . 20  |-  F/ a A. a  e.  c 
Pred ( R ,  A ,  a )  C_  c
3937, 38nfan 1842 . . . . . . . . . . . . . . . . . . 19  |-  F/ a ( A. a  e.  b  Pred ( R ,  A ,  a )  C_  b  /\  A. a  e.  c  Pred ( R ,  A ,  a )  C_  c )
40 inss1 3521 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( b  i^i  c )  C_  b
4140sseli 3304 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  e.  ( b  i^i  c )  ->  a  e.  b )
42 rsp 2726 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A. a  e.  b  Pred ( R ,  A , 
a )  C_  b  ->  ( a  e.  b  ->  Pred ( R ,  A ,  a )  C_  b ) )
4341, 42syl5com 28 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  ( b  i^i  c )  ->  ( A. a  e.  b  Pred ( R ,  A ,  a )  C_  b  ->  Pred ( R ,  A ,  a )  C_  b ) )
44 inss2 3522 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( b  i^i  c )  C_  c
4544sseli 3304 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  e.  ( b  i^i  c )  ->  a  e.  c )
46 rsp 2726 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A. a  e.  c  Pred ( R ,  A , 
a )  C_  c  ->  ( a  e.  c  ->  Pred ( R ,  A ,  a )  C_  c ) )
4745, 46syl5com 28 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  ( b  i^i  c )  ->  ( A. a  e.  c  Pred ( R ,  A ,  a )  C_  c  ->  Pred ( R ,  A ,  a )  C_  c ) )
4843, 47anim12d 547 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  e.  ( b  i^i  c )  ->  (
( A. a  e.  b  Pred ( R ,  A ,  a )  C_  b  /\  A. a  e.  c  Pred ( R ,  A ,  a )  C_  c )  ->  ( Pred ( R ,  A ,  a )  C_  b  /\  Pred ( R ,  A ,  a )  C_  c ) ) )
49 ssin 3523 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
Pred ( R ,  A ,  a )  C_  b  /\  Pred ( R ,  A , 
a )  C_  c
)  <->  Pred ( R ,  A ,  a )  C_  ( b  i^i  c
) )
5049biimpi 187 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
Pred ( R ,  A ,  a )  C_  b  /\  Pred ( R ,  A , 
a )  C_  c
)  ->  Pred ( R ,  A ,  a )  C_  ( b  i^i  c ) )
5148, 50syl6com 33 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A. a  e.  b 
Pred ( R ,  A ,  a )  C_  b  /\  A. a  e.  c  Pred ( R ,  A ,  a )  C_  c )  ->  ( a  e.  ( b  i^i  c )  ->  Pred ( R ,  A ,  a )  C_  ( b  i^i  c
) ) )
5239, 51ralrimi 2747 . . . . . . . . . . . . . . . . . 18  |-  ( ( A. a  e.  b 
Pred ( R ,  A ,  a )  C_  b  /\  A. a  e.  c  Pred ( R ,  A ,  a )  C_  c )  ->  A. a  e.  ( b  i^i  c )
Pred ( R ,  A ,  a )  C_  ( b  i^i  c
) )
5352ad2ant2l 727 . . . . . . . . . . . . . . . . 17  |-  ( ( ( b  C_  A  /\  A. a  e.  b 
Pred ( R ,  A ,  a )  C_  b )  /\  (
c  C_  A  /\  A. a  e.  c  Pred ( R ,  A , 
a )  C_  c
) )  ->  A. a  e.  ( b  i^i  c
) Pred ( R ,  A ,  a )  C_  ( b  i^i  c
) )
5436, 53jca 519 . . . . . . . . . . . . . . . 16  |-  ( ( ( b  C_  A  /\  A. a  e.  b 
Pred ( R ,  A ,  a )  C_  b )  /\  (
c  C_  A  /\  A. a  e.  c  Pred ( R ,  A , 
a )  C_  c
) )  ->  (
( b  i^i  c
)  C_  A  /\  A. a  e.  ( b  i^i  c ) Pred ( R ,  A ,  a )  C_  ( b  i^i  c
) ) )
55 fndm 5503 . . . . . . . . . . . . . . . . . 18  |-  ( h  Fn  c  ->  dom  h  =  c )
5612, 55ineqan12d 3504 . . . . . . . . . . . . . . . . 17  |-  ( ( g  Fn  b  /\  h  Fn  c )  ->  ( dom  g  i^i 
dom  h )  =  ( b  i^i  c
) )
57 sseq1 3329 . . . . . . . . . . . . . . . . . . 19  |-  ( ( dom  g  i^i  dom  h )  =  ( b  i^i  c )  ->  ( ( dom  g  i^i  dom  h
)  C_  A  <->  ( b  i^i  c )  C_  A
) )
58 sseq2 3330 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( dom  g  i^i  dom  h )  =  ( b  i^i  c )  ->  ( Pred ( R ,  A , 
a )  C_  ( dom  g  i^i  dom  h
)  <->  Pred ( R ,  A ,  a )  C_  ( b  i^i  c
) ) )
5958raleqbi1dv 2872 . . . . . . . . . . . . . . . . . . 19  |-  ( ( dom  g  i^i  dom  h )  =  ( b  i^i  c )  ->  ( A. a  e.  ( dom  g  i^i 
dom  h ) Pred ( R ,  A ,  a )  C_  ( dom  g  i^i  dom  h )  <->  A. a  e.  ( b  i^i  c
) Pred ( R ,  A ,  a )  C_  ( b  i^i  c
) ) )
6057, 59anbi12d 692 . . . . . . . . . . . . . . . . . 18  |-  ( ( dom  g  i^i  dom  h )  =  ( b  i^i  c )  ->  ( ( ( dom  g  i^i  dom  h )  C_  A  /\  A. a  e.  ( dom  g  i^i  dom  h ) Pred ( R ,  A , 
a )  C_  ( dom  g  i^i  dom  h
) )  <->  ( (
b  i^i  c )  C_  A  /\  A. a  e.  ( b  i^i  c
) Pred ( R ,  A ,  a )  C_  ( b  i^i  c
) ) ) )
6160imbi2d 308 . . . . . . . . . . . . . . . . 17  |-  ( ( dom  g  i^i  dom  h )  =  ( b  i^i  c )  ->  ( ( ( ( b  C_  A  /\  A. a  e.  b 
Pred ( R ,  A ,  a )  C_  b )  /\  (
c  C_  A  /\  A. a  e.  c  Pred ( R ,  A , 
a )  C_  c
) )  ->  (
( dom  g  i^i  dom  h )  C_  A  /\  A. a  e.  ( dom  g  i^i  dom  h ) Pred ( R ,  A , 
a )  C_  ( dom  g  i^i  dom  h
) ) )  <->  ( (
( b  C_  A  /\  A. a  e.  b 
Pred ( R ,  A ,  a )  C_  b )  /\  (
c  C_  A  /\  A. a  e.  c  Pred ( R ,  A , 
a )  C_  c
) )  ->  (
( b  i^i  c
)  C_  A  /\  A. a  e.  ( b  i^i  c ) Pred ( R ,  A ,  a )  C_  ( b  i^i  c
) ) ) ) )
6256, 61syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( g  Fn  b  /\  h  Fn  c )  ->  ( ( ( ( b  C_  A  /\  A. a  e.  b  Pred ( R ,  A , 
a )  C_  b
)  /\  ( c  C_  A  /\  A. a  e.  c  Pred ( R ,  A ,  a )  C_  c )
)  ->  ( ( dom  g  i^i  dom  h
)  C_  A  /\  A. a  e.  ( dom  g  i^i  dom  h
) Pred ( R ,  A ,  a )  C_  ( dom  g  i^i 
dom  h ) ) )  <->  ( ( ( b  C_  A  /\  A. a  e.  b  Pred ( R ,  A , 
a )  C_  b
)  /\  ( c  C_  A  /\  A. a  e.  c  Pred ( R ,  A ,  a )  C_  c )
)  ->  ( (
b  i^i  c )  C_  A  /\  A. a  e.  ( b  i^i  c
) Pred ( R ,  A ,  a )  C_  ( b  i^i  c
) ) ) ) )
6354, 62mpbiri 225 . . . . . . . . . . . . . . 15  |-  ( ( g  Fn  b  /\  h  Fn  c )  ->  ( ( ( b 
C_  A  /\  A. a  e.  b  Pred ( R ,  A , 
a )  C_  b
)  /\  ( c  C_  A  /\  A. a  e.  c  Pred ( R ,  A ,  a )  C_  c )
)  ->  ( ( dom  g  i^i  dom  h
)  C_  A  /\  A. a  e.  ( dom  g  i^i  dom  h
) Pred ( R ,  A ,  a )  C_  ( dom  g  i^i 
dom  h ) ) ) )
6463imp 419 . . . . . . . . . . . . . 14  |-  ( ( ( g  Fn  b  /\  h  Fn  c
)  /\  ( (
b  C_  A  /\  A. a  e.  b  Pred ( R ,  A , 
a )  C_  b
)  /\  ( c  C_  A  /\  A. a  e.  c  Pred ( R ,  A ,  a )  C_  c )
) )  ->  (
( dom  g  i^i  dom  h )  C_  A  /\  A. a  e.  ( dom  g  i^i  dom  h ) Pred ( R ,  A , 
a )  C_  ( dom  g  i^i  dom  h
) ) )
65643adant3 977 . . . . . . . . . . . . 13  |-  ( ( ( g  Fn  b  /\  h  Fn  c
)  /\  ( (
b  C_  A  /\  A. a  e.  b  Pred ( R ,  A , 
a )  C_  b
)  /\  ( c  C_  A  /\  A. a  e.  c  Pred ( R ,  A ,  a )  C_  c )
)  /\  ( A. a  e.  b  (
g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A , 
a ) ) )  /\  A. a  e.  c  ( h `  a )  =  ( G `  ( h  |`  Pred ( R ,  A ,  a )
) ) ) )  ->  ( ( dom  g  i^i  dom  h
)  C_  A  /\  A. a  e.  ( dom  g  i^i  dom  h
) Pred ( R ,  A ,  a )  C_  ( dom  g  i^i 
dom  h ) ) )
6665exlimivv 1642 . . . . . . . . . . . 12  |-  ( E. b E. c ( ( g  Fn  b  /\  h  Fn  c
)  /\  ( (
b  C_  A  /\  A. a  e.  b  Pred ( R ,  A , 
a )  C_  b
)  /\  ( c  C_  A  /\  A. a  e.  c  Pred ( R ,  A ,  a )  C_  c )
)  /\  ( A. a  e.  b  (
g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A , 
a ) ) )  /\  A. a  e.  c  ( h `  a )  =  ( G `  ( h  |`  Pred ( R ,  A ,  a )
) ) ) )  ->  ( ( dom  g  i^i  dom  h
)  C_  A  /\  A. a  e.  ( dom  g  i^i  dom  h
) Pred ( R ,  A ,  a )  C_  ( dom  g  i^i 
dom  h ) ) )
6734, 66sylbir 205 . . . . . . . . . . 11  |-  ( ( E. b ( g  Fn  b  /\  (
b  C_  A  /\  A. a  e.  b  Pred ( R ,  A , 
a )  C_  b
)  /\  A. a  e.  b  ( g `  a )  =  ( G `  ( g  |`  Pred ( R ,  A ,  a )
) ) )  /\  E. c ( h  Fn  c  /\  ( c 
C_  A  /\  A. a  e.  c  Pred ( R ,  A , 
a )  C_  c
)  /\  A. a  e.  c  ( h `  a )  =  ( G `  ( h  |`  Pred ( R ,  A ,  a )
) ) ) )  ->  ( ( dom  g  i^i  dom  h
)  C_  A  /\  A. a  e.  ( dom  g  i^i  dom  h
) Pred ( R ,  A ,  a )  C_  ( dom  g  i^i 
dom  h ) ) )
6811, 30, 67syl2anb 466 . . . . . . . . . 10  |-  ( ( g  e.  B  /\  h  e.  B )  ->  ( ( dom  g  i^i  dom  h )  C_  A  /\  A. a  e.  ( dom  g  i^i 
dom  h ) Pred ( R ,  A ,  a )  C_  ( dom  g  i^i  dom  h ) ) )
6968adantr 452 . . . . . . . . 9  |-  ( ( ( g  e.  B  /\  h  e.  B
)  /\  a  e.  ( dom  g  i^i  dom  h ) )  -> 
( ( dom  g  i^i  dom  h )  C_  A  /\  A. a  e.  ( dom  g  i^i 
dom  h ) Pred ( R ,  A ,  a )  C_  ( dom  g  i^i  dom  h ) ) )
70 simpr 448 . . . . . . . . 9  |-  ( ( ( g  e.  B  /\  h  e.  B
)  /\  a  e.  ( dom  g  i^i  dom  h ) )  -> 
a  e.  ( dom  g  i^i  dom  h
) )
71 preddowncl 25410 . . . . . . . . 9  |-  ( ( ( dom  g  i^i 
dom  h )  C_  A  /\  A. a  e.  ( dom  g  i^i 
dom  h ) Pred ( R ,  A ,  a )  C_  ( dom  g  i^i  dom  h ) )  -> 
( a  e.  ( dom  g  i^i  dom  h )  ->  Pred ( R ,  ( dom  g  i^i  dom  h ) ,  a )  = 
Pred ( R ,  A ,  a )
) )
7269, 70, 71sylc 58 . . . . . . . 8  |-  ( ( ( g  e.  B  /\  h  e.  B
)  /\  a  e.  ( dom  g  i^i  dom  h ) )  ->  Pred ( R ,  ( dom  g  i^i  dom  h ) ,  a )  =  Pred ( R ,  A , 
a ) )
7328, 72syl5eq 2448 . . . . . . 7  |-  ( ( ( g  e.  B  /\  h  e.  B
)  /\  a  e.  ( dom  g  i^i  dom  h ) )  -> 
( ( dom  g  i^i  dom  h )  i^i 
Pred ( R , 
( dom  g  i^i  dom  h ) ,  a ) )  =  Pred ( R ,  A , 
a ) )
7473reseq2d 5105 . . . . . 6  |-  ( ( ( g  e.  B  /\  h  e.  B
)  /\  a  e.  ( dom  g  i^i  dom  h ) )  -> 
( g  |`  (
( dom  g  i^i  dom  h )  i^i  Pred ( R ,  ( dom  g  i^i  dom  h
) ,  a ) ) )  =  ( g  |`  Pred ( R ,  A ,  a ) ) )
7525, 74syl5eq 2448 . . . . 5  |-  ( ( ( g  e.  B  /\  h  e.  B
)  /\  a  e.  ( dom  g  i^i  dom  h ) )  -> 
( ( g  |`  ( dom  g  i^i  dom  h ) )  |`  Pred ( R ,  ( dom  g  i^i  dom  h ) ,  a ) )  =  ( g  |`  Pred ( R ,  A ,  a ) ) )
7675fveq2d 5691 . . . 4  |-  ( ( ( g  e.  B  /\  h  e.  B
)  /\  a  e.  ( dom  g  i^i  dom  h ) )  -> 
( G `  (
( g  |`  ( dom  g  i^i  dom  h
) )  |`  Pred ( R ,  ( dom  g  i^i  dom  h ) ,  a ) ) )  =  ( G `
 ( g  |`  Pred ( R ,  A ,  a ) ) ) )
7722, 24, 763eqtr4d 2446 . . 3  |-  ( ( ( g  e.  B  /\  h  e.  B
)  /\  a  e.  ( dom  g  i^i  dom  h ) )  -> 
( ( g  |`  ( dom  g  i^i  dom  h ) ) `  a )  =  ( G `  ( ( g  |`  ( dom  g  i^i  dom  h )
)  |`  Pred ( R , 
( dom  g  i^i  dom  h ) ,  a ) ) ) )
7877ralrimiva 2749 . 2  |-  ( ( g  e.  B  /\  h  e.  B )  ->  A. a  e.  ( dom  g  i^i  dom  h ) ( ( g  |`  ( dom  g  i^i  dom  h )
) `  a )  =  ( G `  ( ( g  |`  ( dom  g  i^i  dom  h ) )  |`  Pred ( R ,  ( dom  g  i^i  dom  h ) ,  a ) ) ) )
797, 78jca 519 1  |-  ( ( g  e.  B  /\  h  e.  B )  ->  ( ( g  |`  ( dom  g  i^i  dom  h ) )  Fn  ( dom  g  i^i 
dom  h )  /\  A. a  e.  ( dom  g  i^i  dom  h
) ( ( g  |`  ( dom  g  i^i 
dom  h ) ) `
 a )  =  ( G `  (
( g  |`  ( dom  g  i^i  dom  h
) )  |`  Pred ( R ,  ( dom  g  i^i  dom  h ) ,  a ) ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    /\ w3a 936   E.wex 1547    = wceq 1649    e. wcel 1721   {cab 2390   A.wral 2666    i^i cin 3279    C_ wss 3280    We wwe 4500   dom cdm 4837    |` cres 4839   Fun wfun 5407    Fn wfn 5408   ` cfv 5413   Predcpred 25381
This theorem is referenced by:  wfrlem5  25474
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 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363
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-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-fv 5421  df-pred 25382
  Copyright terms: Public domain W3C validator