Metamath Proof Explorer

Theorem wfrlem4

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) (Revised by AV, 18-Jul-2022)

Ref Expression
Hypothesis 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 ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) }
Assertion 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 ) = ( F ` ( ( g |` ( dom g i^i dom h ) ) |` Pred ( R , ( dom g i^i dom h ) , a ) ) ) ) )

Proof

Step Hyp Ref Expression
1 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 ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) }
2 1 wfrlem2 
 |-  ( 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 wfrlem1 
 |-  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 ) = ( F ` ( 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 ) = ( F ` ( g |` Pred ( R , A , a ) ) ) ) )
9 fndm 
 |-  ( g Fn b -> dom g = b )
10 9 raleqdv 
 |-  ( g Fn b -> ( A. a e. dom g ( g ` a ) = ( F ` ( g |` Pred ( R , A , a ) ) ) <-> A. a e. b ( g ` a ) = ( F ` ( g |` Pred ( R , A , a ) ) ) ) )
11 10 biimpar 
 |-  ( ( g Fn b /\ A. a e. b ( g ` a ) = ( F ` ( g |` Pred ( R , A , a ) ) ) ) -> A. a e. dom g ( g ` a ) = ( F ` ( g |` Pred ( R , A , a ) ) ) )
12 rsp 
 |-  ( A. a e. dom g ( g ` a ) = ( F ` ( g |` Pred ( R , A , a ) ) ) -> ( a e. dom g -> ( g ` a ) = ( F ` ( g |` Pred ( R , A , a ) ) ) ) )
13 11 12 syl 
 |-  ( ( g Fn b /\ A. a e. b ( g ` a ) = ( F ` ( g |` Pred ( R , A , a ) ) ) ) -> ( a e. dom g -> ( g ` a ) = ( F ` ( g |` Pred ( R , A , a ) ) ) ) )
14 13 3adant2 
 |-  ( ( g Fn b /\ ( b C_ A /\ A. a e. b Pred ( R , A , a ) C_ b ) /\ A. a e. b ( g ` a ) = ( F ` ( g |` Pred ( R , A , a ) ) ) ) -> ( a e. dom g -> ( g ` a ) = ( F ` ( 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 ) = ( F ` ( g |` Pred ( R , A , a ) ) ) ) -> ( a e. dom g -> ( g ` a ) = ( F ` ( g |` Pred ( R , A , a ) ) ) ) )
16 8 15 sylbi 
 |-  ( g e. B -> ( a e. dom g -> ( g ` a ) = ( F ` ( 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 ) = ( F ` ( g |` Pred ( R , A , a ) ) ) )
19 18 adantlr 
 |-  ( ( ( g e. B /\ h e. B ) /\ a e. ( dom g i^i dom h ) ) -> ( g ` a ) = ( F ` ( g |` Pred ( R , A , a ) ) ) )
20 fvres 
 |-  ( a e. ( dom g i^i dom h ) -> ( ( g |` ( dom g i^i dom h ) ) ` a ) = ( g ` a ) )
21 20 adantl 
 |-  ( ( ( 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 wfrlem1 
 |-  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 ) = ( F ` ( 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 ) = ( F ` ( h |` Pred ( R , A , a ) ) ) ) )
28 3an6 
 |-  ( ( ( 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 ) = ( F ` ( g |` Pred ( R , A , a ) ) ) /\ A. a e. c ( h ` a ) = ( F ` ( 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 ) = ( F ` ( 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 ) = ( F ` ( h |` Pred ( R , A , a ) ) ) ) ) )
29 28 2exbii 
 |-  ( 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 ) = ( F ` ( g |` Pred ( R , A , a ) ) ) /\ A. a e. c ( h ` a ) = ( F ` ( 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 ) = ( F ` ( 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 ) = ( F ` ( h |` Pred ( R , A , a ) ) ) ) ) )
30 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 ) = ( F ` ( 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 ) = ( F ` ( 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 ) = ( F ` ( 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 ) = ( F ` ( h |` Pred ( R , A , a ) ) ) ) ) )
31 29 30 bitri 
 |-  ( 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 ) = ( F ` ( g |` Pred ( R , A , a ) ) ) /\ A. a e. c ( h ` a ) = ( F ` ( 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 ) = ( F ` ( 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 ) = ( F ` ( h |` Pred ( R , A , a ) ) ) ) ) )
32 ssinss1 
 |-  ( b C_ A -> ( b i^i c ) C_ A )
33 32 ad2antrr 
 |-  ( ( ( 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 )
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 47 ad2ant2l 
 |-  ( ( ( 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 ) )
49 33 48 jca 
 |-  ( ( ( 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 ) ) )
50 fndm 
 |-  ( h Fn c -> dom h = c )
51 9 50 ineqan12d 
 |-  ( ( g Fn b /\ h Fn c ) -> ( dom g i^i dom h ) = ( b i^i c ) )
52 sseq1 
 |-  ( ( dom g i^i dom h ) = ( b i^i c ) -> ( ( dom g i^i dom h ) C_ A <-> ( b i^i c ) C_ A ) )
53 sseq2 
 |-  ( ( 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 ) ) )
54 53 raleqbi1dv 
 |-  ( ( 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 ) ) )
55 52 54 anbi12d 
 |-  ( ( 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 ) ) ) )
56 55 imbi2d 
 |-  ( ( 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 ) ) ) ) )
57 51 56 syl 
 |-  ( ( 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 ) ) ) ) )
58 49 57 mpbiri 
 |-  ( ( 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 ) ) ) )
59 58 imp 
 |-  ( ( ( 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 ) ) )
60 59 3adant3 
 |-  ( ( ( 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 ) = ( F ` ( g |` Pred ( R , A , a ) ) ) /\ A. a e. c ( h ` a ) = ( F ` ( 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 60 exlimivv 
 |-  ( 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 ) = ( F ` ( g |` Pred ( R , A , a ) ) ) /\ A. a e. c ( h ` a ) = ( F ` ( 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 31 61 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 ) = ( F ` ( 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 ) = ( F ` ( 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 ) ) )
63 8 27 62 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 ) ) )
64 63 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 ) ) )
65 simpr 
 |-  ( ( ( g e. B /\ h e. B ) /\ a e. ( dom g i^i dom h ) ) -> a e. ( dom g i^i dom h ) )
66 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 ) ) )
67 64 65 66 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 ) )
68 25 67 syl5eq 
 |-  ( ( ( 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 ) )
69 68 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 ) ) )
70 22 69 syl5eq 
 |-  ( ( ( 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 ) ) )
71 70 fveq2d 
 |-  ( ( ( g e. B /\ h e. B ) /\ a e. ( dom g i^i dom h ) ) -> ( F ` ( ( g |` ( dom g i^i dom h ) ) |` Pred ( R , ( dom g i^i dom h ) , a ) ) ) = ( F ` ( g |` Pred ( R , A , a ) ) ) )
72 19 21 71 3eqtr4d 
 |-  ( ( ( g e. B /\ h e. B ) /\ a e. ( dom g i^i dom h ) ) -> ( ( g |` ( dom g i^i dom h ) ) ` a ) = ( F ` ( ( g |` ( dom g i^i dom h ) ) |` Pred ( R , ( dom g i^i dom h ) , a ) ) ) )
73 72 ralrimiva 
 |-  ( ( g e. B /\ h e. B ) -> A. a e. ( dom g i^i dom h ) ( ( g |` ( dom g i^i dom h ) ) ` a ) = ( F ` ( ( g |` ( dom g i^i dom h ) ) |` Pred ( R , ( dom g i^i dom h ) , a ) ) ) )
74 6 73 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 ) = ( F ` ( ( g |` ( dom g i^i dom h ) ) |` Pred ( R , ( dom g i^i dom h ) , a ) ) ) ) )