Theorem frfnom 7762

Description: The function generated by finite recursive definition generation is a function on omega. (Contributed by NM, 15-Oct-1996.) (Revised by Mario Carneiro, 14-Nov-2014.)

Assertion

Ref	Expression
frfnom	⊢ (rec(𝐹, 𝐴) ↾ ω) Fn ω

Proof of Theorem frfnom

Step	Hyp	Ref	Expression
1		rdgfun 7744	. . 3 ⊢ Fun rec(𝐹, 𝐴)
2		funres 6139	. . 3 ⊢ (Fun rec(𝐹, 𝐴) → Fun (rec(𝐹, 𝐴) ↾ ω))
3	1, 2	ax-mp 5	. 2 ⊢ Fun (rec(𝐹, 𝐴) ↾ ω)
4		dmres 5622	. . 3 ⊢ dom (rec(𝐹, 𝐴) ↾ ω) = (ω ∩ dom rec(𝐹, 𝐴))
5		rdgdmlim 7745	. . . . 5 ⊢ Lim dom rec(𝐹, 𝐴)
6		limomss 7296	. . . . 5 ⊢ (Lim dom rec(𝐹, 𝐴) → ω ⊆ dom rec(𝐹, 𝐴))
7	5, 6	ax-mp 5	. . . 4 ⊢ ω ⊆ dom rec(𝐹, 𝐴)
8		df-ss 3783	. . . 4 ⊢ (ω ⊆ dom rec(𝐹, 𝐴) ↔ (ω ∩ dom rec(𝐹, 𝐴)) = ω)
9	7, 8	mpbi 221	. . 3 ⊢ (ω ∩ dom rec(𝐹, 𝐴)) = ω
10	4, 9	eqtri 2828	. 2 ⊢ dom (rec(𝐹, 𝐴) ↾ ω) = ω
11		df-fn 6100	. 2 ⊢ ((rec(𝐹, 𝐴) ↾ ω) Fn ω ↔ (Fun (rec(𝐹, 𝐴) ↾ ω) ∧ dom (rec(𝐹, 𝐴) ↾ ω) = ω))
12	3, 10, 11	mpbir2an 693	1 ⊢ (rec(𝐹, 𝐴) ↾ ω) Fn ω

Syntax hints:   = wceq 1637   ∩ cin 3768   ⊆ wss 3769  dom cdm 5311   ↾ cres 5313  Lim wlim 5937  Fun wfun 6091   Fn wfn 6092  ωcom 7291  reccrdg 7737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-om 7292  df-wrecs 7638  df-recs 7700  df-rdg 7738

This theorem is referenced by:  frsucmptn  7766  seqomlem2  7778  seqomlem3  7779  seqomlem4  7780  unblem4  8450  dffi3  8572  inf0  8761  inf3lem6  8773  alephfplem4  9209  alephfp  9210  infpssrlem3  9408  itunifn  9520  hsmexlem5  9533  axdclem2  9623  wunex2  9841  wuncval2  9850  peano5nni  11304  1nn  11312  peano2nn  11313  om2uzrani  12971  om2uzf1oi  12972  uzrdglem  12976  uzrdgfni  12977  uzrdg0i  12978  hashkf  13335  hashgval2  13381  dftrpred2  32034  trpredpred  32043  trpredex  32052  neibastop2lem  32671  cnfin0  33551  cnfinltrel  33552