Metamath Proof Explorer

Theorem seqex

Description: Existence of the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013)

Ref Expression
Assertion seqex 
|- seq M ( .+ , F ) e. _V

Proof

Step Hyp Ref Expression
1 df-seq 
 |-  seq M ( .+ , F ) = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om )
2 rdgfun 
 |-  Fun rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
3 omex 
 |-  _om e. _V
4 funimaexg 
 |-  ( ( Fun rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) /\ _om e. _V ) -> ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om ) e. _V )
5 2 3 4 mp2an 
 |-  ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om ) e. _V
6 1 5 eqeltri 
 |-  seq M ( .+ , F ) e. _V