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

Theorem nfrdg 8082
Description: Bound-variable hypothesis builder for the recursive definition generator. (Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro, 8-Sep-2013.)
Hypotheses
Ref Expression
nfrdg.1 𝑥𝐹
nfrdg.2 𝑥𝐴
Assertion
Ref Expression
nfrdg 𝑥rec(𝐹, 𝐴)

Proof of Theorem nfrdg
Dummy variable 𝑔 is distinct from all other variables.
StepHypRef Expression
1 df-rdg 8078 . 2 rec(𝐹, 𝐴) = recs((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐴, if(Lim dom 𝑔, ran 𝑔, (𝐹‘(𝑔 dom 𝑔))))))
2 nfcv 2900 . . . 4 𝑥V
3 nfv 1921 . . . . 5 𝑥 𝑔 = ∅
4 nfrdg.2 . . . . 5 𝑥𝐴
5 nfv 1921 . . . . . 6 𝑥Lim dom 𝑔
6 nfcv 2900 . . . . . 6 𝑥 ran 𝑔
7 nfrdg.1 . . . . . . 7 𝑥𝐹
8 nfcv 2900 . . . . . . 7 𝑥(𝑔 dom 𝑔)
97, 8nffv 6687 . . . . . 6 𝑥(𝐹‘(𝑔 dom 𝑔))
105, 6, 9nfif 4445 . . . . 5 𝑥if(Lim dom 𝑔, ran 𝑔, (𝐹‘(𝑔 dom 𝑔)))
113, 4, 10nfif 4445 . . . 4 𝑥if(𝑔 = ∅, 𝐴, if(Lim dom 𝑔, ran 𝑔, (𝐹‘(𝑔 dom 𝑔))))
122, 11nfmpt 5128 . . 3 𝑥(𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐴, if(Lim dom 𝑔, ran 𝑔, (𝐹‘(𝑔 dom 𝑔)))))
1312nfrecs 8043 . 2 𝑥recs((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐴, if(Lim dom 𝑔, ran 𝑔, (𝐹‘(𝑔 dom 𝑔))))))
141, 13nfcxfr 2898 1 𝑥rec(𝐹, 𝐴)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wnfc 2880  Vcvv 3399  c0 4212  ifcif 4415   cuni 4797  cmpt 5111  dom cdm 5526  ran crn 5527  Lim wlim 6174  cfv 6340  recscrecs 8039  reccrdg 8077
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3401  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-nul 4213  df-if 4416  df-sn 4518  df-pr 4520  df-op 4524  df-uni 4798  df-br 5032  df-opab 5094  df-mpt 5112  df-xp 5532  df-cnv 5534  df-dm 5536  df-rn 5537  df-res 5538  df-ima 5539  df-pred 6130  df-iota 6298  df-fv 6348  df-wrecs 7979  df-recs 8040  df-rdg 8078
This theorem is referenced by:  rdgsucmptf  8096  rdgsucmptnf  8097  frsucmpt  8105  frsucmptn  8106  nfseq  13473  trpredlem1  33374  trpredrec  33385  rdgssun  35195  exrecfnlem  35196  finxpreclem6  35213
  Copyright terms: Public domain W3C validator