![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > frfnom | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
frfnom | ⊢ (rec(𝐹, 𝐴) ↾ ω) Fn ω |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rdgfun 7683 | . . 3 ⊢ Fun rec(𝐹, 𝐴) | |
2 | funres 6091 | . . 3 ⊢ (Fun rec(𝐹, 𝐴) → Fun (rec(𝐹, 𝐴) ↾ ω)) | |
3 | 1, 2 | ax-mp 5 | . 2 ⊢ Fun (rec(𝐹, 𝐴) ↾ ω) |
4 | dmres 5578 | . . 3 ⊢ dom (rec(𝐹, 𝐴) ↾ ω) = (ω ∩ dom rec(𝐹, 𝐴)) | |
5 | rdgdmlim 7684 | . . . . 5 ⊢ Lim dom rec(𝐹, 𝐴) | |
6 | limomss 7237 | . . . . 5 ⊢ (Lim dom rec(𝐹, 𝐴) → ω ⊆ dom rec(𝐹, 𝐴)) | |
7 | 5, 6 | ax-mp 5 | . . . 4 ⊢ ω ⊆ dom rec(𝐹, 𝐴) |
8 | df-ss 3730 | . . . 4 ⊢ (ω ⊆ dom rec(𝐹, 𝐴) ↔ (ω ∩ dom rec(𝐹, 𝐴)) = ω) | |
9 | 7, 8 | mpbi 220 | . . 3 ⊢ (ω ∩ dom rec(𝐹, 𝐴)) = ω |
10 | 4, 9 | eqtri 2783 | . 2 ⊢ dom (rec(𝐹, 𝐴) ↾ ω) = ω |
11 | df-fn 6053 | . 2 ⊢ ((rec(𝐹, 𝐴) ↾ ω) Fn ω ↔ (Fun (rec(𝐹, 𝐴) ↾ ω) ∧ dom (rec(𝐹, 𝐴) ↾ ω) = ω)) | |
12 | 3, 10, 11 | mpbir2an 993 | 1 ⊢ (rec(𝐹, 𝐴) ↾ ω) Fn ω |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1632 ∩ cin 3715 ⊆ wss 3716 dom cdm 5267 ↾ cres 5269 Lim wlim 5886 Fun wfun 6044 Fn wfn 6045 ωcom 7232 reccrdg 7676 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1989 ax-6 2055 ax-7 2091 ax-8 2142 ax-9 2149 ax-10 2169 ax-11 2184 ax-12 2197 ax-13 2392 ax-ext 2741 ax-sep 4934 ax-nul 4942 ax-pow 4993 ax-pr 5056 ax-un 7116 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2048 df-eu 2612 df-mo 2613 df-clab 2748 df-cleq 2754 df-clel 2757 df-nfc 2892 df-ne 2934 df-ral 3056 df-rex 3057 df-reu 3058 df-rab 3060 df-v 3343 df-sbc 3578 df-csb 3676 df-dif 3719 df-un 3721 df-in 3723 df-ss 3730 df-pss 3732 df-nul 4060 df-if 4232 df-pw 4305 df-sn 4323 df-pr 4325 df-tp 4327 df-op 4329 df-uni 4590 df-iun 4675 df-br 4806 df-opab 4866 df-mpt 4883 df-tr 4906 df-id 5175 df-eprel 5180 df-po 5188 df-so 5189 df-fr 5226 df-we 5228 df-xp 5273 df-rel 5274 df-cnv 5275 df-co 5276 df-dm 5277 df-rn 5278 df-res 5279 df-ima 5280 df-pred 5842 df-ord 5888 df-on 5889 df-lim 5890 df-suc 5891 df-iota 6013 df-fun 6052 df-fn 6053 df-f 6054 df-f1 6055 df-fo 6056 df-f1o 6057 df-fv 6058 df-om 7233 df-wrecs 7578 df-recs 7639 df-rdg 7677 |
This theorem is referenced by: frsucmptn 7705 seqomlem2 7717 seqomlem3 7718 seqomlem4 7719 unblem4 8383 dffi3 8505 inf0 8694 inf3lem6 8706 alephfplem4 9141 alephfp 9142 infpssrlem3 9340 itunifn 9452 hsmexlem5 9465 axdclem2 9555 wunex2 9773 wuncval2 9782 peano5nni 11236 1nn 11244 peano2nn 11245 om2uzrani 12966 om2uzf1oi 12967 uzrdglem 12971 uzrdgfni 12972 uzrdg0i 12973 hashkf 13334 hashgval2 13380 dftrpred2 32046 trpredpred 32055 trpredex 32064 neibastop2lem 32683 cnfin0 33570 cnfinltrel 33571 |
Copyright terms: Public domain | W3C validator |