Metamath Proof Explorer

Theorem frrlem4

Description: Lemma for well-founded recursion. Properties of the restriction of an acceptable function to the domain of another acceptable function. (Contributed by Paul Chapman, 21-Apr-2012)

Ref Expression
Hypothesis frrlem4.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 frrlem4 
|- ( ( 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 ) = ( a G ( ( g |` ( dom g i^i dom h ) ) |` Pred ( R , ( dom g i^i dom h ) , a ) ) ) ) )

Proof

Step Hyp Ref Expression
1 frrlem4.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 frrlem2 
 |-  ( g e. B -> Fun g )
3 2 funfnd 
 |-  ( g e. B -> g Fn dom g )
4 fnresin1 
 |-  ( g Fn dom g -> ( g |` ( dom g i^i dom h ) ) Fn ( dom g i^i dom h ) )
5 3 4 syl 
 |-  ( g e. B -> ( g |` ( dom g i^i dom h ) ) Fn ( dom g i^i dom h ) )
6 5 adantr 
 |-  ( ( g e. B /\ h e. B ) -> ( g |` ( dom g i^i dom h ) ) Fn ( dom g i^i dom h ) )
7 1 frrlem1 
 |-  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 ) = ( a G ( g |` Pred ( R , A , a ) ) ) ) }
8 7 abeq2i 
 |-  ( 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 ) = ( a G ( g |` Pred ( R , A , a ) ) ) ) )
9 fndm 
 |-  ( g Fn b -> dom g = b )
10 9 adantr 
 |-  ( ( g Fn b /\ ( b C_ A /\ A. a e. b Pred ( R , A , a ) C_ b ) ) -> dom g = b )
11 10 raleqdv 
 |-  ( ( g Fn b /\ ( b C_ A /\ A. a e. b Pred ( R , A , a ) C_ b ) ) -> ( A. a e. dom g ( g ` a ) = ( a G ( g |` Pred ( R , A , a ) ) ) <-> A. a e. b ( g ` a ) = ( a G ( g |` Pred ( R , A , a ) ) ) ) )
12 11 biimp3ar 
 |-  ( ( g Fn b /\ ( b C_ A /\ A. a e. b Pred ( R , A , a ) C_ b ) /\ A. a e. b ( g ` a ) = ( a G ( g |` Pred ( R , A , a ) ) ) ) -> A. a e. dom g ( g ` a ) = ( a G ( g |` Pred ( R , A , a ) ) ) )
13 rsp 
 |-  ( A. a e. dom g ( g ` a ) = ( a G ( g |` Pred ( R , A , a ) ) ) -> ( a e. dom g -> ( g ` a ) = ( a G ( g |` Pred ( R , A , a ) ) ) ) )
14 12 13 syl 
 |-  ( ( g Fn b /\ ( b C_ A /\ A. a e. b Pred ( R , A , a ) C_ b ) /\ A. a e. b ( g ` a ) = ( a G ( g |` Pred ( R , A , a ) ) ) ) -> ( a e. dom g -> ( g ` a ) = ( a G ( g |` Pred ( R , A , a ) ) ) ) )
15 14 exlimiv 
 |-  ( E. b ( g Fn b /\ ( b C_ A /\ A. a e. b Pred ( R , A , a ) C_ b ) /\ A. a e. b ( g ` a ) = ( a G ( g |` Pred ( R , A , a ) ) ) ) -> ( a e. dom g -> ( g ` a ) = ( a G ( g |` Pred ( R , A , a ) ) ) ) )
16 8 15 sylbi 
 |-  ( g e. B -> ( a e. dom g -> ( g ` a ) = ( a G ( g |` Pred ( R , A , a ) ) ) ) )
17 elinel1 
 |-  ( a e. ( dom g i^i dom h ) -> a e. dom g )
18 16 17 impel 
 |-  ( ( g e. B /\ a e. ( dom g i^i dom h ) ) -> ( g ` a ) = ( a G ( g |` Pred ( R , A , a ) ) ) )
19 18 adantlr 
 |-  ( ( ( g e. B /\ h e. B ) /\ a e. ( dom g i^i dom h ) ) -> ( g ` a ) = ( a G ( g |` Pred ( R , A , a ) ) ) )
20 simpr 
 |-  ( ( ( g e. B /\ h e. B ) /\ a e. ( dom g i^i dom h ) ) -> a e. ( dom g i^i dom h ) )
21 20 fvresd 
 |-  ( ( ( g e. B /\ h e. B ) /\ a e. ( dom g i^i dom h ) ) -> ( ( g |` ( dom g i^i dom h ) ) ` a ) = ( g ` a ) )
22 resres 
 |-  ( ( 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 ) ) )
23 predss 
 |-  Pred ( R , ( dom g i^i dom h ) , a ) C_ ( dom g i^i dom h )
24 sseqin2 
 |-  ( 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 ) )
25 23 24 mpbi 
 |-  ( ( 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 )
26 1 frrlem1 
 |-  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 ) = ( a G ( h |` Pred ( R , A , a ) ) ) ) }
27 26 abeq2i 
 |-  ( 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 ) = ( a G ( h |` Pred ( R , A , a ) ) ) ) )
28 exdistrv 
 |-  ( 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 ) = ( 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 ) = ( 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 ) = ( 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 ) = ( a G ( h |` Pred ( R , A , a ) ) ) ) ) )
29 inss1 
 |-  ( b i^i c ) C_ b
30 simpl2l 
 |-  ( ( ( g Fn b /\ ( b C_ A /\ A. a e. b Pred ( R , A , a ) C_ b ) /\ A. a e. b ( g ` a ) = ( 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 ) = ( a G ( h |` Pred ( R , A , a ) ) ) ) ) -> b C_ A )
31 29 30 sstrid 
 |-  ( ( ( g Fn b /\ ( b C_ A /\ A. a e. b Pred ( R , A , a ) C_ b ) /\ A. a e. b ( g ` a ) = ( 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 ) = ( a G ( h |` Pred ( R , A , a ) ) ) ) ) -> ( b i^i c ) C_ A )
32 simp2r 
 |-  ( ( g Fn b /\ ( b C_ A /\ A. a e. b Pred ( R , A , a ) C_ b ) /\ A. a e. b ( g ` a ) = ( a G ( g |` Pred ( R , A , a ) ) ) ) -> A. a e. b Pred ( R , A , a ) C_ b )
33 simp2r 
 |-  ( ( h Fn c /\ ( c C_ A /\ A. a e. c Pred ( R , A , a ) C_ c ) /\ A. a e. c ( h ` a ) = ( a G ( h |` Pred ( R , A , a ) ) ) ) -> A. a e. c Pred ( R , A , a ) C_ c )
34 nfra1 
 |-  F/ a A. a e. b Pred ( R , A , a ) C_ b
35 nfra1 
 |-  F/ a A. a e. c Pred ( R , A , a ) C_ c
36 34 35 nfan 
 |-  F/ a ( A. a e. b Pred ( R , A , a ) C_ b /\ A. a e. c Pred ( R , A , a ) C_ c )
37 elinel1 
 |-  ( a e. ( b i^i c ) -> a e. b )
38 rsp 
 |-  ( A. a e. b Pred ( R , A , a ) C_ b -> ( a e. b -> Pred ( R , A , a ) C_ b ) )
39 37 38 syl5com 
 |-  ( a e. ( b i^i c ) -> ( A. a e. b Pred ( R , A , a ) C_ b -> Pred ( R , A , a ) C_ b ) )
40 elinel2 
 |-  ( a e. ( b i^i c ) -> a e. c )
41 rsp 
 |-  ( A. a e. c Pred ( R , A , a ) C_ c -> ( a e. c -> Pred ( R , A , a ) C_ c ) )
42 40 41 syl5com 
 |-  ( a e. ( b i^i c ) -> ( A. a e. c Pred ( R , A , a ) C_ c -> Pred ( R , A , a ) C_ c ) )
43 39 42 anim12d 
 |-  ( 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 ) ) )
44 ssin 
 |-  ( ( Pred ( R , A , a ) C_ b /\ Pred ( R , A , a ) C_ c ) <-> Pred ( R , A , a ) C_ ( b i^i c ) )
45 44 biimpi 
 |-  ( ( Pred ( R , A , a ) C_ b /\ Pred ( R , A , a ) C_ c ) -> Pred ( R , A , a ) C_ ( b i^i c ) )
46 43 45 syl6com 
 |-  ( ( 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 ) ) )
47 36 46 ralrimi 
 |-  ( ( 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 ) )
48 32 33 47 syl2an 
 |-  ( ( ( g Fn b /\ ( b C_ A /\ A. a e. b Pred ( R , A , a ) C_ b ) /\ A. a e. b ( g ` a ) = ( 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 ) = ( a G ( h |` Pred ( R , A , a ) ) ) ) ) -> A. a e. ( b i^i c ) Pred ( R , A , a ) C_ ( b i^i c ) )
49 simpl1 
 |-  ( ( ( g Fn b /\ ( b C_ A /\ A. a e. b Pred ( R , A , a ) C_ b ) /\ A. a e. b ( g ` a ) = ( 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 ) = ( a G ( h |` Pred ( R , A , a ) ) ) ) ) -> g Fn b )
50 49 fndmd 
 |-  ( ( ( g Fn b /\ ( b C_ A /\ A. a e. b Pred ( R , A , a ) C_ b ) /\ A. a e. b ( g ` a ) = ( 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 ) = ( a G ( h |` Pred ( R , A , a ) ) ) ) ) -> dom g = b )
51 simpr1 
 |-  ( ( ( g Fn b /\ ( b C_ A /\ A. a e. b Pred ( R , A , a ) C_ b ) /\ A. a e. b ( g ` a ) = ( 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 ) = ( a G ( h |` Pred ( R , A , a ) ) ) ) ) -> h Fn c )
52 51 fndmd 
 |-  ( ( ( g Fn b /\ ( b C_ A /\ A. a e. b Pred ( R , A , a ) C_ b ) /\ A. a e. b ( g ` a ) = ( 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 ) = ( a G ( h |` Pred ( R , A , a ) ) ) ) ) -> dom h = c )
53 ineq12 
 |-  ( ( dom g = b /\ dom h = c ) -> ( dom g i^i dom h ) = ( b i^i c ) )
54 53 sseq1d 
 |-  ( ( dom g = b /\ dom h = c ) -> ( ( dom g i^i dom h ) C_ A <-> ( b i^i c ) C_ A ) )
55 53 sseq2d 
 |-  ( ( dom g = b /\ dom h = c ) -> ( Pred ( R , A , a ) C_ ( dom g i^i dom h ) <-> Pred ( R , A , a ) C_ ( b i^i c ) ) )
56 53 55 raleqbidv 
 |-  ( ( dom g = b /\ dom h = 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 ) ) )
57 54 56 anbi12d 
 |-  ( ( dom g = b /\ dom h = 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 ) ) ) )
58 50 52 57 syl2anc 
 |-  ( ( ( g Fn b /\ ( b C_ A /\ A. a e. b Pred ( R , A , a ) C_ b ) /\ A. a e. b ( g ` a ) = ( 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 ) = ( 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 ) ) <-> ( ( b i^i c ) C_ A /\ A. a e. ( b i^i c ) Pred ( R , A , a ) C_ ( b i^i c ) ) ) )
59 31 48 58 mpbir2and 
 |-  ( ( ( g Fn b /\ ( b C_ A /\ A. a e. b Pred ( R , A , a ) C_ b ) /\ A. a e. b ( g ` a ) = ( 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 ) = ( 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 ) ) )
60 59 exlimivv 
 |-  ( 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 ) = ( 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 ) = ( 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 ) ) )
61 28 60 sylbir 
 |-  ( ( E. b ( g Fn b /\ ( b C_ A /\ A. a e. b Pred ( R , A , a ) C_ b ) /\ A. a e. b ( g ` a ) = ( 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 ) = ( 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 ) ) )
62 8 27 61 syl2anb 
 |-  ( ( 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 ) ) )
63 62 adantr 
 |-  ( ( ( 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 ) ) )
64 preddowncl 
 |-  ( ( ( 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 ) ) )
65 63 20 64 sylc 
 |-  ( ( ( 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 ) )
66 25 65 eqtrid 
 |-  ( ( ( 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 ) )
67 66 reseq2d 
 |-  ( ( ( 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 ) ) )
68 22 67 eqtrid 
 |-  ( ( ( 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 ) ) )
69 68 oveq2d 
 |-  ( ( ( g e. B /\ h e. B ) /\ a e. ( dom g i^i dom h ) ) -> ( a G ( ( g |` ( dom g i^i dom h ) ) |` Pred ( R , ( dom g i^i dom h ) , a ) ) ) = ( a G ( g |` Pred ( R , A , a ) ) ) )
70 19 21 69 3eqtr4d 
 |-  ( ( ( g e. B /\ h e. B ) /\ a e. ( dom g i^i dom h ) ) -> ( ( g |` ( dom g i^i dom h ) ) ` a ) = ( a G ( ( g |` ( dom g i^i dom h ) ) |` Pred ( R , ( dom g i^i dom h ) , a ) ) ) )
71 70 ralrimiva 
 |-  ( ( g e. B /\ h e. B ) -> A. a e. ( dom g i^i dom h ) ( ( g |` ( dom g i^i dom h ) ) ` a ) = ( a G ( ( g |` ( dom g i^i dom h ) ) |` Pred ( R , ( dom g i^i dom h ) , a ) ) ) )
72 6 71 jca 
 |-  ( ( 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 ) = ( a G ( ( g |` ( dom g i^i dom h ) ) |` Pred ( R , ( dom g i^i dom h ) , a ) ) ) ) )