Metamath Proof Explorer

Theorem frrlem10

Description: Lemma for well-founded recursion. Under the compatibility hypothesis, compute the value of F within its domain. (Contributed by Scott Fenton, 6-Dec-2022)

Ref Expression
Hypotheses frrlem9.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 ) ) ) ) }
frrlem9.2 
|- F = frecs ( R , A , G )
frrlem9.3 
|- ( ( ph /\ ( g e. B /\ h e. B ) ) -> ( ( x g u /\ x h v ) -> u = v ) )
Assertion frrlem10 
|- ( ( ph /\ y e. dom F ) -> ( F ` y ) = ( y G ( F |` Pred ( R , A , y ) ) ) )

Proof

Step Hyp Ref Expression
1 frrlem9.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 frrlem9.2 
 |-  F = frecs ( R , A , G )
3 frrlem9.3 
 |-  ( ( ph /\ ( g e. B /\ h e. B ) ) -> ( ( x g u /\ x h v ) -> u = v ) )
4 vex 
 |-  y e. _V
5 4 eldm2 
 |-  ( y e. dom F <-> E. z <. y , z >. e. F )
6 1 2 frrlem5 
 |-  F = U. B
7 1 unieqi 
 |-  U. B = U. { 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 ) ) ) ) }
8 6 7 eqtri 
 |-  F = U. { 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 ) ) ) ) }
9 8 eleq2i 
 |-  ( <. y , z >. e. F <-> <. y , z >. e. U. { 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 ) ) ) ) } )
10 eluniab 
 |-  ( <. y , z >. e. U. { 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 ) ) ) ) } <-> E. f ( <. y , z >. e. 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 ) ) ) ) ) )
11 9 10 bitri 
 |-  ( <. y , z >. e. F <-> E. f ( <. y , z >. e. 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 ) ) ) ) ) )
12 19.8a 
 |-  ( ( 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 ( 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 ) ) ) ) )
13 12 3ad2ant2 
 |-  ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. 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 ) ) ) ) )
14 abid 
 |-  ( f e. { 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 ) ) ) ) } <-> 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 ) ) ) ) )
15 13 14 sylibr 
 |-  ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. f ) -> f e. { 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 ) ) ) ) } )
16 elssuni 
 |-  ( f e. { 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 ) ) ) ) } -> f C_ U. { 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 ) ) ) ) } )
17 15 16 syl 
 |-  ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. f ) -> f C_ U. { 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 ) ) ) ) } )
18 17 8 sseqtrrdi 
 |-  ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. f ) -> f C_ F )
19 simpl23 
 |-  ( ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. f ) /\ f C_ F ) -> A. y e. x ( f ` y ) = ( y G ( f |` Pred ( R , A , y ) ) ) )
20 simpl3 
 |-  ( ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. f ) /\ f C_ F ) -> <. y , z >. e. f )
21 vex 
 |-  z e. _V
22 4 21 opeldm 
 |-  ( <. y , z >. e. f -> y e. dom f )
23 20 22 syl 
 |-  ( ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. f ) /\ f C_ F ) -> y e. dom f )
24 simpl21 
 |-  ( ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. f ) /\ f C_ F ) -> f Fn x )
25 24 fndmd 
 |-  ( ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. f ) /\ f C_ F ) -> dom f = x )
26 23 25 eleqtrd 
 |-  ( ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. f ) /\ f C_ F ) -> y e. x )
27 rsp 
 |-  ( A. y e. x ( f ` y ) = ( y G ( f |` Pred ( R , A , y ) ) ) -> ( y e. x -> ( f ` y ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) )
28 19 26 27 sylc 
 |-  ( ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. f ) /\ f C_ F ) -> ( f ` y ) = ( y G ( f |` Pred ( R , A , y ) ) ) )
29 simpl1 
 |-  ( ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. f ) /\ f C_ F ) -> ph )
30 1 2 3 frrlem9 
 |-  ( ph -> Fun F )
31 29 30 syl 
 |-  ( ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. f ) /\ f C_ F ) -> Fun F )
32 simpr 
 |-  ( ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. f ) /\ f C_ F ) -> f C_ F )
33 funssfv 
 |-  ( ( Fun F /\ f C_ F /\ y e. dom f ) -> ( F ` y ) = ( f ` y ) )
34 31 32 23 33 syl3anc 
 |-  ( ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. f ) /\ f C_ F ) -> ( F ` y ) = ( f ` y ) )
35 simp22r 
 |-  ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. f ) -> A. y e. x Pred ( R , A , y ) C_ x )
36 35 adantr 
 |-  ( ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. f ) /\ f C_ F ) -> A. y e. x Pred ( R , A , y ) C_ x )
37 rsp 
 |-  ( A. y e. x Pred ( R , A , y ) C_ x -> ( y e. x -> Pred ( R , A , y ) C_ x ) )
38 36 26 37 sylc 
 |-  ( ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. f ) /\ f C_ F ) -> Pred ( R , A , y ) C_ x )
39 38 25 sseqtrrd 
 |-  ( ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. f ) /\ f C_ F ) -> Pred ( R , A , y ) C_ dom f )
40 fun2ssres 
 |-  ( ( Fun F /\ f C_ F /\ Pred ( R , A , y ) C_ dom f ) -> ( F |` Pred ( R , A , y ) ) = ( f |` Pred ( R , A , y ) ) )
41 31 32 39 40 syl3anc 
 |-  ( ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. f ) /\ f C_ F ) -> ( F |` Pred ( R , A , y ) ) = ( f |` Pred ( R , A , y ) ) )
42 41 oveq2d 
 |-  ( ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. f ) /\ f C_ F ) -> ( y G ( F |` Pred ( R , A , y ) ) ) = ( y G ( f |` Pred ( R , A , y ) ) ) )
43 28 34 42 3eqtr4d 
 |-  ( ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. f ) /\ f C_ F ) -> ( F ` y ) = ( y G ( F |` Pred ( R , A , y ) ) ) )
44 18 43 mpdan 
 |-  ( ( ph /\ ( 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 ) ) ) ) /\ <. y , z >. e. f ) -> ( F ` y ) = ( y G ( F |` Pred ( R , A , y ) ) ) )
45 44 3exp 
 |-  ( ph -> ( ( 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 ) ) ) ) -> ( <. y , z >. e. f -> ( F ` y ) = ( y G ( F |` Pred ( R , A , y ) ) ) ) ) )
46 45 exlimdv 
 |-  ( ph -> ( 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 ) ) ) ) -> ( <. y , z >. e. f -> ( F ` y ) = ( y G ( F |` Pred ( R , A , y ) ) ) ) ) )
47 46 impcomd 
 |-  ( ph -> ( ( <. y , z >. e. 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 ) ) ) ) ) -> ( F ` y ) = ( y G ( F |` Pred ( R , A , y ) ) ) ) )
48 47 exlimdv 
 |-  ( ph -> ( E. f ( <. y , z >. e. 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 ) ) ) ) ) -> ( F ` y ) = ( y G ( F |` Pred ( R , A , y ) ) ) ) )
49 11 48 biimtrid 
 |-  ( ph -> ( <. y , z >. e. F -> ( F ` y ) = ( y G ( F |` Pred ( R , A , y ) ) ) ) )
50 49 exlimdv 
 |-  ( ph -> ( E. z <. y , z >. e. F -> ( F ` y ) = ( y G ( F |` Pred ( R , A , y ) ) ) ) )
51 5 50 biimtrid 
 |-  ( ph -> ( y e. dom F -> ( F ` y ) = ( y G ( F |` Pred ( R , A , y ) ) ) ) )
52 51 imp 
 |-  ( ( ph /\ y e. dom F ) -> ( F ` y ) = ( y G ( F |` Pred ( R , A , y ) ) ) )