MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  frsuc Structured version   Visualization version   GIF version

Theorem frsuc 7231
Description: The successor value resulting from finite recursive definition generation. (Contributed by NM, 15-Oct-1996.) (Revised by Mario Carneiro, 16-Nov-2014.)
Assertion
Ref Expression
frsuc (𝐵 ∈ ω → ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝐵) = (𝐹‘((rec(𝐹, 𝐴) ↾ ω)‘𝐵)))

Proof of Theorem frsuc
StepHypRef Expression
1 rdgdmlim 7212 . . . . 5 Lim dom rec(𝐹, 𝐴)
2 limomss 6774 . . . . 5 (Lim dom rec(𝐹, 𝐴) → ω ⊆ dom rec(𝐹, 𝐴))
31, 2ax-mp 5 . . . 4 ω ⊆ dom rec(𝐹, 𝐴)
43sseli 3450 . . 3 (𝐵 ∈ ω → 𝐵 ∈ dom rec(𝐹, 𝐴))
5 rdgsucg 7218 . . 3 (𝐵 ∈ dom rec(𝐹, 𝐴) → (rec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(rec(𝐹, 𝐴)‘𝐵)))
64, 5syl 17 . 2 (𝐵 ∈ ω → (rec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(rec(𝐹, 𝐴)‘𝐵)))
7 peano2b 6785 . . 3 (𝐵 ∈ ω ↔ suc 𝐵 ∈ ω)
8 fvres 5941 . . 3 (suc 𝐵 ∈ ω → ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝐵) = (rec(𝐹, 𝐴)‘suc 𝐵))
97, 8sylbi 202 . 2 (𝐵 ∈ ω → ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝐵) = (rec(𝐹, 𝐴)‘suc 𝐵))
10 fvres 5941 . . 3 (𝐵 ∈ ω → ((rec(𝐹, 𝐴) ↾ ω)‘𝐵) = (rec(𝐹, 𝐴)‘𝐵))
1110fveq2d 5931 . 2 (𝐵 ∈ ω → (𝐹‘((rec(𝐹, 𝐴) ↾ ω)‘𝐵)) = (𝐹‘(rec(𝐹, 𝐴)‘𝐵)))
126, 9, 113eqtr4d 2549 1 (𝐵 ∈ ω → ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝐵) = (𝐹‘((rec(𝐹, 𝐴) ↾ ω)‘𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1468  wcel 1937  wss 3426  dom cdm 4880  cres 4882  Lim wlim 5475  suc csuc 5476  cfv 5633  ωcom 6769  reccrdg 7204
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-8 1939  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pow 4619  ax-pr 4680  ax-un 6659
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3or 1022  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-reu 2798  df-rab 2800  df-v 3068  df-sbc 3292  df-csb 3386  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3758  df-if 3909  df-pw 3980  df-sn 3996  df-pr 3998  df-tp 4000  df-op 4002  df-uni 4229  df-iun 4309  df-br 4435  df-opab 4494  df-mpt 4495  df-tr 4531  df-eprel 4791  df-id 4795  df-po 4801  df-so 4802  df-fr 4839  df-we 4841  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-pred 5431  df-ord 5477  df-on 5478  df-lim 5479  df-suc 5480  df-iota 5597  df-fun 5635  df-fn 5636  df-f 5637  df-f1 5638  df-fo 5639  df-f1o 5640  df-fv 5641  df-om 6770  df-wrecs 7105  df-recs 7167  df-rdg 7205
This theorem is referenced by:  frsucmpt  7232  frsucmptn  7233  seqomlem1  7244  seqomlem4  7247  onasuc  7307  onmsuc  7308  onesuc  7309  inf3lemc  8216  alephfplem2  8621  ackbij2lem2  8755  infpssrlem2  8819  fin23lem34  8861  fin23lem35  8862  itunisuc  8934  om2uzrdg  12283  uzrdgsuci  12287
  Copyright terms: Public domain W3C validator