Metamath Proof Explorer

Theorem fnseqom

Description: An index-aware recursive definition defines a function on the natural numbers. (Contributed by Stefan O'Rear, 1-Nov-2014)

Ref Expression
Hypothesis seqom.a 
|- G = seqom ( F , I )
Assertion fnseqom 
|- G Fn _om

Proof

Step Hyp Ref Expression
1 seqom.a 
 |-  G = seqom ( F , I )
2 seqomlem0 
 |-  rec ( ( a e. _om , b e. _V |-> <. suc a , ( a F b ) >. ) , <. (/) , ( _I ` I ) >. ) = rec ( ( c e. _om , d e. _V |-> <. suc c , ( c F d ) >. ) , <. (/) , ( _I ` I ) >. )
3 2 seqomlem2 
 |-  ( rec ( ( a e. _om , b e. _V |-> <. suc a , ( a F b ) >. ) , <. (/) , ( _I ` I ) >. ) " _om ) Fn _om
4 df-seqom 
 |-  seqom ( F , I ) = ( rec ( ( a e. _om , b e. _V |-> <. suc a , ( a F b ) >. ) , <. (/) , ( _I ` I ) >. ) " _om )
5 1 4 eqtri 
 |-  G = ( rec ( ( a e. _om , b e. _V |-> <. suc a , ( a F b ) >. ) , <. (/) , ( _I ` I ) >. ) " _om )
6 5 fneq1i 
 |-  ( G Fn _om <-> ( rec ( ( a e. _om , b e. _V |-> <. suc a , ( a F b ) >. ) , <. (/) , ( _I ` I ) >. ) " _om ) Fn _om )
7 3 6 mpbir 
 |-  G Fn _om