Metamath Proof Explorer

Theorem wfrlem14

Description: Lemma for well-founded recursion. Compute the value of C . (Contributed by Scott Fenton, 21-Apr-2011)

Ref Expression
Hypotheses wfrlem13.1 
|- R We A
wfrlem13.2 
|- R Se A
wfrlem13.3 
|- F = wrecs ( R , A , G )
wfrlem13.4 
|- C = ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } )
Assertion wfrlem14 
|- ( z e. ( A \ dom F ) -> ( y e. ( dom F u. { z } ) -> ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 wfrlem13.1 
 |-  R We A
2 wfrlem13.2 
 |-  R Se A
3 wfrlem13.3 
 |-  F = wrecs ( R , A , G )
4 wfrlem13.4 
 |-  C = ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } )
5 1 2 3 4 wfrlem13 
 |-  ( z e. ( A \ dom F ) -> C Fn ( dom F u. { z } ) )
6 elun 
 |-  ( y e. ( dom F u. { z } ) <-> ( y e. dom F \/ y e. { z } ) )
7 velsn 
 |-  ( y e. { z } <-> y = z )
8 7 orbi2i 
 |-  ( ( y e. dom F \/ y e. { z } ) <-> ( y e. dom F \/ y = z ) )
9 6 8 bitri 
 |-  ( y e. ( dom F u. { z } ) <-> ( y e. dom F \/ y = z ) )
10 1 2 3 wfrlem12 
 |-  ( y e. dom F -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) )
11 fnfun 
 |-  ( C Fn ( dom F u. { z } ) -> Fun C )
12 ssun1 
 |-  F C_ ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } )
13 12 4 sseqtrri 
 |-  F C_ C
14 funssfv 
 |-  ( ( Fun C /\ F C_ C /\ y e. dom F ) -> ( C ` y ) = ( F ` y ) )
15 3 wfrdmcl 
 |-  ( y e. dom F -> Pred ( R , A , y ) C_ dom F )
16 fun2ssres 
 |-  ( ( Fun C /\ F C_ C /\ Pred ( R , A , y ) C_ dom F ) -> ( C |` Pred ( R , A , y ) ) = ( F |` Pred ( R , A , y ) ) )
17 15 16 syl3an3 
 |-  ( ( Fun C /\ F C_ C /\ y e. dom F ) -> ( C |` Pred ( R , A , y ) ) = ( F |` Pred ( R , A , y ) ) )
18 17 fveq2d 
 |-  ( ( Fun C /\ F C_ C /\ y e. dom F ) -> ( G ` ( C |` Pred ( R , A , y ) ) ) = ( G ` ( F |` Pred ( R , A , y ) ) ) )
19 14 18 eqeq12d 
 |-  ( ( Fun C /\ F C_ C /\ y e. dom F ) -> ( ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) <-> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) ) )
20 13 19 mp3an2 
 |-  ( ( Fun C /\ y e. dom F ) -> ( ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) <-> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) ) )
21 11 20 sylan 
 |-  ( ( C Fn ( dom F u. { z } ) /\ y e. dom F ) -> ( ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) <-> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) ) )
22 10 21 syl5ibr 
 |-  ( ( C Fn ( dom F u. { z } ) /\ y e. dom F ) -> ( y e. dom F -> ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) ) )
23 22 ex 
 |-  ( C Fn ( dom F u. { z } ) -> ( y e. dom F -> ( y e. dom F -> ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) ) ) )
24 23 pm2.43d 
 |-  ( C Fn ( dom F u. { z } ) -> ( y e. dom F -> ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) ) )
25 vsnid 
 |-  z e. { z }
26 elun2 
 |-  ( z e. { z } -> z e. ( dom F u. { z } ) )
27 25 26 ax-mp 
 |-  z e. ( dom F u. { z } )
28 4 reseq1i 
 |-  ( C |` Pred ( R , A , z ) ) = ( ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } ) |` Pred ( R , A , z ) )
29 resundir 
 |-  ( ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } ) |` Pred ( R , A , z ) ) = ( ( F |` Pred ( R , A , z ) ) u. ( { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } |` Pred ( R , A , z ) ) )
30 wefr 
 |-  ( R We A -> R Fr A )
31 1 30 ax-mp 
 |-  R Fr A
32 predfrirr 
 |-  ( R Fr A -> -. z e. Pred ( R , A , z ) )
33 ressnop0 
 |-  ( -. z e. Pred ( R , A , z ) -> ( { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } |` Pred ( R , A , z ) ) = (/) )
34 31 32 33 mp2b 
 |-  ( { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } |` Pred ( R , A , z ) ) = (/)
35 34 uneq2i 
 |-  ( ( F |` Pred ( R , A , z ) ) u. ( { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } |` Pred ( R , A , z ) ) ) = ( ( F |` Pred ( R , A , z ) ) u. (/) )
36 un0 
 |-  ( ( F |` Pred ( R , A , z ) ) u. (/) ) = ( F |` Pred ( R , A , z ) )
37 35 36 eqtri 
 |-  ( ( F |` Pred ( R , A , z ) ) u. ( { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } |` Pred ( R , A , z ) ) ) = ( F |` Pred ( R , A , z ) )
38 28 29 37 3eqtri 
 |-  ( C |` Pred ( R , A , z ) ) = ( F |` Pred ( R , A , z ) )
39 38 fveq2i 
 |-  ( G ` ( C |` Pred ( R , A , z ) ) ) = ( G ` ( F |` Pred ( R , A , z ) ) )
40 39 opeq2i 
 |-  <. z , ( G ` ( C |` Pred ( R , A , z ) ) ) >. = <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >.
41 opex 
 |-  <. z , ( G ` ( C |` Pred ( R , A , z ) ) ) >. e. _V
42 41 elsn 
 |-  ( <. z , ( G ` ( C |` Pred ( R , A , z ) ) ) >. e. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } <-> <. z , ( G ` ( C |` Pred ( R , A , z ) ) ) >. = <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. )
43 40 42 mpbir 
 |-  <. z , ( G ` ( C |` Pred ( R , A , z ) ) ) >. e. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. }
44 elun2 
 |-  ( <. z , ( G ` ( C |` Pred ( R , A , z ) ) ) >. e. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } -> <. z , ( G ` ( C |` Pred ( R , A , z ) ) ) >. e. ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } ) )
45 43 44 ax-mp 
 |-  <. z , ( G ` ( C |` Pred ( R , A , z ) ) ) >. e. ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } )
46 45 4 eleqtrri 
 |-  <. z , ( G ` ( C |` Pred ( R , A , z ) ) ) >. e. C
47 fnopfvb 
 |-  ( ( C Fn ( dom F u. { z } ) /\ z e. ( dom F u. { z } ) ) -> ( ( C ` z ) = ( G ` ( C |` Pred ( R , A , z ) ) ) <-> <. z , ( G ` ( C |` Pred ( R , A , z ) ) ) >. e. C ) )
48 46 47 mpbiri 
 |-  ( ( C Fn ( dom F u. { z } ) /\ z e. ( dom F u. { z } ) ) -> ( C ` z ) = ( G ` ( C |` Pred ( R , A , z ) ) ) )
49 27 48 mpan2 
 |-  ( C Fn ( dom F u. { z } ) -> ( C ` z ) = ( G ` ( C |` Pred ( R , A , z ) ) ) )
50 fveq2 
 |-  ( y = z -> ( C ` y ) = ( C ` z ) )
51 predeq3 
 |-  ( y = z -> Pred ( R , A , y ) = Pred ( R , A , z ) )
52 51 reseq2d 
 |-  ( y = z -> ( C |` Pred ( R , A , y ) ) = ( C |` Pred ( R , A , z ) ) )
53 52 fveq2d 
 |-  ( y = z -> ( G ` ( C |` Pred ( R , A , y ) ) ) = ( G ` ( C |` Pred ( R , A , z ) ) ) )
54 50 53 eqeq12d 
 |-  ( y = z -> ( ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) <-> ( C ` z ) = ( G ` ( C |` Pred ( R , A , z ) ) ) ) )
55 49 54 syl5ibrcom 
 |-  ( C Fn ( dom F u. { z } ) -> ( y = z -> ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) ) )
56 24 55 jaod 
 |-  ( C Fn ( dom F u. { z } ) -> ( ( y e. dom F \/ y = z ) -> ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) ) )
57 9 56 syl5bi 
 |-  ( C Fn ( dom F u. { z } ) -> ( y e. ( dom F u. { z } ) -> ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) ) )
58 5 57 syl 
 |-  ( z e. ( A \ dom F ) -> ( y e. ( dom F u. { z } ) -> ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) ) )