Metamath Proof Explorer

Theorem om2uzrdg

Description: A helper lemma for the value of a recursive definition generator on upper integers (typically either NN or NN0 ) with characteristic function F ( x , y ) and initial value A . Normally F is a function on the partition, and A is a member of the partition. See also comment in om2uz0i . (Contributed by Mario Carneiro, 26-Jun-2013) (Revised by Mario Carneiro, 18-Nov-2014)

Ref Expression
Hypotheses om2uz.1 
|- C e. ZZ
om2uz.2 
|- G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , C ) |` _om )
uzrdg.1 
|- A e. _V
uzrdg.2 
|- R = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om )
Assertion om2uzrdg 
|- ( B e. _om -> ( R ` B ) = <. ( G ` B ) , ( 2nd ` ( R ` B ) ) >. )

Proof

Step Hyp Ref Expression
1 om2uz.1 
 |-  C e. ZZ
2 om2uz.2 
 |-  G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , C ) |` _om )
3 uzrdg.1 
 |-  A e. _V
4 uzrdg.2 
 |-  R = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om )
5 fveq2 
 |-  ( z = (/) -> ( R ` z ) = ( R ` (/) ) )
6 fveq2 
 |-  ( z = (/) -> ( G ` z ) = ( G ` (/) ) )
7 2fveq3 
 |-  ( z = (/) -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` (/) ) ) )
8 6 7 opeq12d 
 |-  ( z = (/) -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. )
9 5 8 eqeq12d 
 |-  ( z = (/) -> ( ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. <-> ( R ` (/) ) = <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. ) )
10 fveq2 
 |-  ( z = v -> ( R ` z ) = ( R ` v ) )
11 fveq2 
 |-  ( z = v -> ( G ` z ) = ( G ` v ) )
12 2fveq3 
 |-  ( z = v -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` v ) ) )
13 11 12 opeq12d 
 |-  ( z = v -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. )
14 10 13 eqeq12d 
 |-  ( z = v -> ( ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. <-> ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) )
15 fveq2 
 |-  ( z = suc v -> ( R ` z ) = ( R ` suc v ) )
16 fveq2 
 |-  ( z = suc v -> ( G ` z ) = ( G ` suc v ) )
17 2fveq3 
 |-  ( z = suc v -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` suc v ) ) )
18 16 17 opeq12d 
 |-  ( z = suc v -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` suc v ) , ( 2nd ` ( R ` suc v ) ) >. )
19 15 18 eqeq12d 
 |-  ( z = suc v -> ( ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. <-> ( R ` suc v ) = <. ( G ` suc v ) , ( 2nd ` ( R ` suc v ) ) >. ) )
20 fveq2 
 |-  ( z = B -> ( R ` z ) = ( R ` B ) )
21 fveq2 
 |-  ( z = B -> ( G ` z ) = ( G ` B ) )
22 2fveq3 
 |-  ( z = B -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` B ) ) )
23 21 22 opeq12d 
 |-  ( z = B -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` B ) , ( 2nd ` ( R ` B ) ) >. )
24 20 23 eqeq12d 
 |-  ( z = B -> ( ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. <-> ( R ` B ) = <. ( G ` B ) , ( 2nd ` ( R ` B ) ) >. ) )
25 4 fveq1i 
 |-  ( R ` (/) ) = ( ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` (/) )
26 opex 
 |-  <. C , A >. e. _V
27 fr0g 
 |-  ( <. C , A >. e. _V -> ( ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` (/) ) = <. C , A >. )
28 26 27 ax-mp 
 |-  ( ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` (/) ) = <. C , A >.
29 25 28 eqtri 
 |-  ( R ` (/) ) = <. C , A >.
30 1 2 om2uz0i 
 |-  ( G ` (/) ) = C
31 29 fveq2i 
 |-  ( 2nd ` ( R ` (/) ) ) = ( 2nd ` <. C , A >. )
32 1 elexi 
 |-  C e. _V
33 32 3 op2nd 
 |-  ( 2nd ` <. C , A >. ) = A
34 31 33 eqtri 
 |-  ( 2nd ` ( R ` (/) ) ) = A
35 30 34 opeq12i 
 |-  <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. = <. C , A >.
36 29 35 eqtr4i 
 |-  ( R ` (/) ) = <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >.
37 frsuc 
 |-  ( v e. _om -> ( ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` suc v ) = ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ` ( ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` v ) ) )
38 4 fveq1i 
 |-  ( R ` suc v ) = ( ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` suc v )
39 4 fveq1i 
 |-  ( R ` v ) = ( ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` v )
40 39 fveq2i 
 |-  ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ` ( R ` v ) ) = ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ` ( ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` v ) )
41 37 38 40 3eqtr4g 
 |-  ( v e. _om -> ( R ` suc v ) = ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ` ( R ` v ) ) )
42 fveq2 
 |-  ( ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. -> ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ` ( R ` v ) ) = ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ` <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) )
43 df-ov 
 |-  ( ( G ` v ) ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ( 2nd ` ( R ` v ) ) ) = ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ` <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. )
44 fvex 
 |-  ( G ` v ) e. _V
45 fvex 
 |-  ( 2nd ` ( R ` v ) ) e. _V
46 oveq1 
 |-  ( w = ( G ` v ) -> ( w + 1 ) = ( ( G ` v ) + 1 ) )
47 oveq1 
 |-  ( w = ( G ` v ) -> ( w F z ) = ( ( G ` v ) F z ) )
48 46 47 opeq12d 
 |-  ( w = ( G ` v ) -> <. ( w + 1 ) , ( w F z ) >. = <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F z ) >. )
49 oveq2 
 |-  ( z = ( 2nd ` ( R ` v ) ) -> ( ( G ` v ) F z ) = ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) )
50 49 opeq2d 
 |-  ( z = ( 2nd ` ( R ` v ) ) -> <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F z ) >. = <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. )
51 oveq1 
 |-  ( x = w -> ( x + 1 ) = ( w + 1 ) )
52 oveq1 
 |-  ( x = w -> ( x F y ) = ( w F y ) )
53 51 52 opeq12d 
 |-  ( x = w -> <. ( x + 1 ) , ( x F y ) >. = <. ( w + 1 ) , ( w F y ) >. )
54 oveq2 
 |-  ( y = z -> ( w F y ) = ( w F z ) )
55 54 opeq2d 
 |-  ( y = z -> <. ( w + 1 ) , ( w F y ) >. = <. ( w + 1 ) , ( w F z ) >. )
56 53 55 cbvmpov 
 |-  ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) = ( w e. _V , z e. _V |-> <. ( w + 1 ) , ( w F z ) >. )
57 opex 
 |-  <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. e. _V
58 48 50 56 57 ovmpo 
 |-  ( ( ( G ` v ) e. _V /\ ( 2nd ` ( R ` v ) ) e. _V ) -> ( ( G ` v ) ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ( 2nd ` ( R ` v ) ) ) = <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. )
59 44 45 58 mp2an 
 |-  ( ( G ` v ) ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ( 2nd ` ( R ` v ) ) ) = <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >.
60 43 59 eqtr3i 
 |-  ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ` <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) = <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >.
61 42 60 eqtrdi 
 |-  ( ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. -> ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ` ( R ` v ) ) = <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. )
62 41 61 sylan9eq 
 |-  ( ( v e. _om /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) -> ( R ` suc v ) = <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. )
63 1 2 om2uzsuci 
 |-  ( v e. _om -> ( G ` suc v ) = ( ( G ` v ) + 1 ) )
64 63 adantr 
 |-  ( ( v e. _om /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) -> ( G ` suc v ) = ( ( G ` v ) + 1 ) )
65 62 fveq2d 
 |-  ( ( v e. _om /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) -> ( 2nd ` ( R ` suc v ) ) = ( 2nd ` <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. ) )
66 ovex 
 |-  ( ( G ` v ) + 1 ) e. _V
67 ovex 
 |-  ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) e. _V
68 66 67 op2nd 
 |-  ( 2nd ` <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. ) = ( ( G ` v ) F ( 2nd ` ( R ` v ) ) )
69 65 68 eqtrdi 
 |-  ( ( v e. _om /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) -> ( 2nd ` ( R ` suc v ) ) = ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) )
70 64 69 opeq12d 
 |-  ( ( v e. _om /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) -> <. ( G ` suc v ) , ( 2nd ` ( R ` suc v ) ) >. = <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. )
71 62 70 eqtr4d 
 |-  ( ( v e. _om /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) -> ( R ` suc v ) = <. ( G ` suc v ) , ( 2nd ` ( R ` suc v ) ) >. )
72 71 ex 
 |-  ( v e. _om -> ( ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. -> ( R ` suc v ) = <. ( G ` suc v ) , ( 2nd ` ( R ` suc v ) ) >. ) )
73 9 14 19 24 36 72 finds 
 |-  ( B e. _om -> ( R ` B ) = <. ( G ` B ) , ( 2nd ` ( R ` B ) ) >. )