Metamath Proof Explorer

Theorem wfrlem12

Description: Lemma for well-founded recursion. Here, we compute the value of the recursive definition generator. (Contributed by Scott Fenton, 21-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Hypotheses wfrfun.1 
|- R We A
wfrfun.2 
|- R Se A
wfrfun.3 
|- F = wrecs ( R , A , G )
Assertion wfrlem12 
|- ( y e. dom F -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) )

Proof

Step Hyp Ref Expression
1 wfrfun.1 
 |-  R We A
2 wfrfun.2 
 |-  R Se A
3 wfrfun.3 
 |-  F = wrecs ( R , A , G )
4 vex 
 |-  y e. _V
5 4 eldm2 
 |-  ( y e. dom F <-> E. z <. y , z >. e. F )
6 df-wrecs 
 |-  wrecs ( R , A , G ) = 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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }
7 3 6 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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }
8 7 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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) } )
9 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 ) = ( 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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) ) )
10 8 9 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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) ) )
11 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 ) = ( 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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) )
12 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 ) = ( 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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) } )
13 12 7 sseqtrrdi 
 |-  ( 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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) } -> f C_ F )
14 11 13 sylbir 
 |-  ( 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 ) ) ) ) -> f C_ F )
15 fnop 
 |-  ( ( f Fn x /\ <. y , z >. e. f ) -> y e. x )
16 15 ex 
 |-  ( f Fn x -> ( <. y , z >. e. f -> y e. x ) )
17 rsp 
 |-  ( A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) -> ( y e. x -> ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) )
18 17 impcom 
 |-  ( ( y e. x /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) -> ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) )
19 rsp 
 |-  ( A. y e. x Pred ( R , A , y ) C_ x -> ( y e. x -> Pred ( R , A , y ) C_ x ) )
20 fndm 
 |-  ( f Fn x -> dom f = x )
21 20 sseq2d 
 |-  ( f Fn x -> ( Pred ( R , A , y ) C_ dom f <-> Pred ( R , A , y ) C_ x ) )
22 20 eleq2d 
 |-  ( f Fn x -> ( y e. dom f <-> y e. x ) )
23 21 22 anbi12d 
 |-  ( f Fn x -> ( ( Pred ( R , A , y ) C_ dom f /\ y e. dom f ) <-> ( Pred ( R , A , y ) C_ x /\ y e. x ) ) )
24 23 biimprd 
 |-  ( f Fn x -> ( ( Pred ( R , A , y ) C_ x /\ y e. x ) -> ( Pred ( R , A , y ) C_ dom f /\ y e. dom f ) ) )
25 24 expd 
 |-  ( f Fn x -> ( Pred ( R , A , y ) C_ x -> ( y e. x -> ( Pred ( R , A , y ) C_ dom f /\ y e. dom f ) ) ) )
26 25 impcom 
 |-  ( ( Pred ( R , A , y ) C_ x /\ f Fn x ) -> ( y e. x -> ( Pred ( R , A , y ) C_ dom f /\ y e. dom f ) ) )
27 1 2 3 wfrfun 
 |-  Fun F
28 funssfv 
 |-  ( ( Fun F /\ f C_ F /\ y e. dom f ) -> ( F ` y ) = ( f ` y ) )
29 28 3adant3l 
 |-  ( ( Fun F /\ f C_ F /\ ( Pred ( R , A , y ) C_ dom f /\ y e. dom f ) ) -> ( F ` y ) = ( f ` y ) )
30 fun2ssres 
 |-  ( ( Fun F /\ f C_ F /\ Pred ( R , A , y ) C_ dom f ) -> ( F |` Pred ( R , A , y ) ) = ( f |` Pred ( R , A , y ) ) )
31 30 3adant3r 
 |-  ( ( Fun F /\ f C_ F /\ ( Pred ( R , A , y ) C_ dom f /\ y e. dom f ) ) -> ( F |` Pred ( R , A , y ) ) = ( f |` Pred ( R , A , y ) ) )
32 31 fveq2d 
 |-  ( ( Fun F /\ f C_ F /\ ( Pred ( R , A , y ) C_ dom f /\ y e. dom f ) ) -> ( G ` ( F |` Pred ( R , A , y ) ) ) = ( G ` ( f |` Pred ( R , A , y ) ) ) )
33 29 32 eqeq12d 
 |-  ( ( Fun F /\ f C_ F /\ ( Pred ( R , A , y ) C_ dom f /\ y e. dom f ) ) -> ( ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) <-> ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) )
34 33 biimprd 
 |-  ( ( Fun F /\ f C_ F /\ ( Pred ( R , A , y ) C_ dom f /\ y e. dom f ) ) -> ( ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) ) )
35 27 34 mp3an1 
 |-  ( ( f C_ F /\ ( Pred ( R , A , y ) C_ dom f /\ y e. dom f ) ) -> ( ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) ) )
36 35 expcom 
 |-  ( ( Pred ( R , A , y ) C_ dom f /\ y e. dom f ) -> ( f C_ F -> ( ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) ) ) )
37 36 com23 
 |-  ( ( Pred ( R , A , y ) C_ dom f /\ y e. dom f ) -> ( ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) -> ( f C_ F -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) ) ) )
38 26 37 syl6com 
 |-  ( y e. x -> ( ( Pred ( R , A , y ) C_ x /\ f Fn x ) -> ( ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) -> ( f C_ F -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) ) ) ) )
39 38 expd 
 |-  ( y e. x -> ( Pred ( R , A , y ) C_ x -> ( f Fn x -> ( ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) -> ( f C_ F -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) ) ) ) ) )
40 39 com34 
 |-  ( y e. x -> ( Pred ( R , A , y ) C_ x -> ( ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) -> ( f Fn x -> ( f C_ F -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) ) ) ) ) )
41 19 40 sylcom 
 |-  ( A. y e. x Pred ( R , A , y ) C_ x -> ( y e. x -> ( ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) -> ( f Fn x -> ( f C_ F -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) ) ) ) ) )
42 41 adantl 
 |-  ( ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) -> ( y e. x -> ( ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) -> ( f Fn x -> ( f C_ F -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) ) ) ) ) )
43 42 com14 
 |-  ( f Fn x -> ( y e. x -> ( ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) -> ( ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) -> ( f C_ F -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) ) ) ) ) )
44 18 43 syl7 
 |-  ( f Fn x -> ( y e. x -> ( ( y e. x /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) -> ( ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) -> ( f C_ F -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) ) ) ) ) )
45 44 exp4a 
 |-  ( f Fn x -> ( y e. x -> ( y e. x -> ( A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) -> ( ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) -> ( f C_ F -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) ) ) ) ) ) )
46 45 pm2.43d 
 |-  ( f Fn x -> ( y e. x -> ( A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) -> ( ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) -> ( f C_ F -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) ) ) ) ) )
47 46 com34 
 |-  ( f Fn x -> ( y e. 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 ) ) ) -> ( f C_ F -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) ) ) ) ) )
48 16 47 syldc 
 |-  ( <. y , z >. e. f -> ( 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 ) ) ) -> ( f C_ F -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) ) ) ) ) )
49 48 3impd 
 |-  ( <. y , z >. e. f -> ( ( 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 ) ) ) ) -> ( f C_ F -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) ) ) )
50 49 exlimdv 
 |-  ( <. 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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) -> ( f C_ F -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) ) ) )
51 14 50 mpdi 
 |-  ( <. 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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) ) )
52 51 imp 
 |-  ( ( <. 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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) ) -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) )
53 52 exlimiv 
 |-  ( 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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) ) -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) )
54 10 53 sylbi 
 |-  ( <. y , z >. e. F -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) )
55 54 exlimiv 
 |-  ( E. z <. y , z >. e. F -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) )
56 5 55 sylbi 
 |-  ( y e. dom F -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) )