![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fr0g | Structured version Visualization version GIF version |
Description: The initial value resulting from finite recursive definition generation. (Contributed by NM, 15-Oct-1996.) |
Ref | Expression |
---|---|
fr0g | ⊢ (𝐴 ∈ 𝐵 → ((rec(𝐹, 𝐴) ↾ ω)‘∅) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | peano1 7416 | . . 3 ⊢ ∅ ∈ ω | |
2 | fvres 6518 | . . 3 ⊢ (∅ ∈ ω → ((rec(𝐹, 𝐴) ↾ ω)‘∅) = (rec(𝐹, 𝐴)‘∅)) | |
3 | 1, 2 | ax-mp 5 | . 2 ⊢ ((rec(𝐹, 𝐴) ↾ ω)‘∅) = (rec(𝐹, 𝐴)‘∅) |
4 | rdg0g 7867 | . 2 ⊢ (𝐴 ∈ 𝐵 → (rec(𝐹, 𝐴)‘∅) = 𝐴) | |
5 | 3, 4 | syl5eq 2826 | 1 ⊢ (𝐴 ∈ 𝐵 → ((rec(𝐹, 𝐴) ↾ ω)‘∅) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 ∈ wcel 2050 ∅c0 4178 ↾ cres 5409 ‘cfv 6188 ωcom 7396 reccrdg 7849 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5060 ax-nul 5067 ax-pow 5119 ax-pr 5186 ax-un 7279 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-ral 3093 df-rex 3094 df-reu 3095 df-rab 3097 df-v 3417 df-sbc 3682 df-csb 3787 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-pss 3845 df-nul 4179 df-if 4351 df-pw 4424 df-sn 4442 df-pr 4444 df-tp 4446 df-op 4448 df-uni 4713 df-iun 4794 df-br 4930 df-opab 4992 df-mpt 5009 df-tr 5031 df-id 5312 df-eprel 5317 df-po 5326 df-so 5327 df-fr 5366 df-we 5368 df-xp 5413 df-rel 5414 df-cnv 5415 df-co 5416 df-dm 5417 df-rn 5418 df-res 5419 df-ima 5420 df-pred 5986 df-ord 6032 df-on 6033 df-lim 6034 df-suc 6035 df-iota 6152 df-fun 6190 df-fn 6191 df-f 6192 df-f1 6193 df-fo 6194 df-f1o 6195 df-fv 6196 df-om 7397 df-wrecs 7750 df-recs 7812 df-rdg 7850 |
This theorem is referenced by: unblem2 8566 dffi3 8690 inf0 8878 inf3lemb 8882 trcl 8964 alephfplem1 9324 infpssrlem1 9523 fin23lem34 9566 ituni0 9638 hsmexlem7 9643 axdclem2 9740 wunex2 9958 wuncval2 9967 peano5nni 11442 1nn 11452 om2uz0i 13130 om2uzrdg 13139 uzrdg0i 13142 trpredlem1 32593 trpredpred 32594 trpredmintr 32597 trpred0 32602 trpredrec 32604 neibastop2lem 33235 |
Copyright terms: Public domain | W3C validator |