Metamath Proof Explorer


Theorem wfrlem4

Description: Lemma for well-ordered 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 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 ) )
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 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 ) ) )
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 ) ) ) ) )