Metamath Proof Explorer

Theorem seqval

Description: Value of the sequence builder function. (Contributed by Mario Carneiro, 24-Jun-2013)

Ref Expression
Hypothesis seqval.1 
|- R = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) |` _om )
Assertion seqval 
|- seq M ( .+ , F ) = ran R

Proof

Step Hyp Ref Expression
1 seqval.1 
 |-  R = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) |` _om )
2 df-ima 
 |-  ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om ) = ran ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) |` _om )
3 df-seq 
 |-  seq M ( .+ , F ) = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om )
4 eqid 
 |-  _V = _V
5 fvoveq1 
 |-  ( z = x -> ( F ` ( z + 1 ) ) = ( F ` ( x + 1 ) ) )
6 5 oveq2d 
 |-  ( z = x -> ( w .+ ( F ` ( z + 1 ) ) ) = ( w .+ ( F ` ( x + 1 ) ) ) )
7 oveq1 
 |-  ( w = y -> ( w .+ ( F ` ( x + 1 ) ) ) = ( y .+ ( F ` ( x + 1 ) ) ) )
8 eqid 
 |-  ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z + 1 ) ) ) ) = ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z + 1 ) ) ) )
9 ovex 
 |-  ( y .+ ( F ` ( x + 1 ) ) ) e. _V
10 6 7 8 9 ovmpo 
 |-  ( ( x e. _V /\ y e. _V ) -> ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) = ( y .+ ( F ` ( x + 1 ) ) ) )
11 10 el2v 
 |-  ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) = ( y .+ ( F ` ( x + 1 ) ) )
12 11 opeq2i 
 |-  <. ( x + 1 ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. = <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >.
13 4 4 12 mpoeq123i 
 |-  ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) = ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. )
14 rdgeq1 
 |-  ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) = ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) -> rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) = rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) )
15 13 14 ax-mp 
 |-  rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) = rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
16 15 reseq1i 
 |-  ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) |` _om ) = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) |` _om )
17 1 16 eqtri 
 |-  R = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) |` _om )
18 17 rneqi 
 |-  ran R = ran ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) |` _om )
19 2 3 18 3eqtr4i 
 |-  seq M ( .+ , F ) = ran R