Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nffrecs Structured version   Visualization version   GIF version

Theorem nffrecs 32094
Description: Bound-variable hypothesis builder for the founded recursion generator. (Contributed by Scott Fenton, 23-Dec-2021.)
Hypotheses
Ref Expression
nffrecs.1 𝑥𝑅
nffrecs.2 𝑥𝐴
nffrecs.3 𝑥𝐹
Assertion
Ref Expression
nffrecs 𝑥frecs(𝑅, 𝐴, 𝐹)

Proof of Theorem nffrecs
Dummy variables 𝑓 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-frecs 32092 . 2 frecs(𝑅, 𝐴, 𝐹) = {𝑓 ∣ ∃𝑦(𝑓 Fn 𝑦 ∧ (𝑦𝐴 ∧ ∀𝑧𝑦 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑦) ∧ ∀𝑧𝑦 (𝑓𝑧) = (𝑧𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑧))))}
2 nfv 2005 . . . . . 6 𝑥 𝑓 Fn 𝑦
3 nfcv 2948 . . . . . . . 8 𝑥𝑦
4 nffrecs.2 . . . . . . . 8 𝑥𝐴
53, 4nfss 3791 . . . . . . 7 𝑥 𝑦𝐴
6 nffrecs.1 . . . . . . . . . 10 𝑥𝑅
7 nfcv 2948 . . . . . . . . . 10 𝑥𝑧
86, 4, 7nfpred 5898 . . . . . . . . 9 𝑥Pred(𝑅, 𝐴, 𝑧)
98, 3nfss 3791 . . . . . . . 8 𝑥Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑦
103, 9nfral 3133 . . . . . . 7 𝑥𝑧𝑦 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑦
115, 10nfan 1990 . . . . . 6 𝑥(𝑦𝐴 ∧ ∀𝑧𝑦 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑦)
12 nffrecs.3 . . . . . . . . 9 𝑥𝐹
13 nfcv 2948 . . . . . . . . . 10 𝑥𝑓
1413, 8nfres 5599 . . . . . . . . 9 𝑥(𝑓 ↾ Pred(𝑅, 𝐴, 𝑧))
157, 12, 14nfov 6900 . . . . . . . 8 𝑥(𝑧𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑧)))
1615nfeq2 2964 . . . . . . 7 𝑥(𝑓𝑧) = (𝑧𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑧)))
173, 16nfral 3133 . . . . . 6 𝑥𝑧𝑦 (𝑓𝑧) = (𝑧𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑧)))
182, 11, 17nf3an 1993 . . . . 5 𝑥(𝑓 Fn 𝑦 ∧ (𝑦𝐴 ∧ ∀𝑧𝑦 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑦) ∧ ∀𝑧𝑦 (𝑓𝑧) = (𝑧𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑧))))
1918nfex 2330 . . . 4 𝑥𝑦(𝑓 Fn 𝑦 ∧ (𝑦𝐴 ∧ ∀𝑧𝑦 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑦) ∧ ∀𝑧𝑦 (𝑓𝑧) = (𝑧𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑧))))
2019nfab 2953 . . 3 𝑥{𝑓 ∣ ∃𝑦(𝑓 Fn 𝑦 ∧ (𝑦𝐴 ∧ ∀𝑧𝑦 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑦) ∧ ∀𝑧𝑦 (𝑓𝑧) = (𝑧𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑧))))}
2120nfuni 4636 . 2 𝑥 {𝑓 ∣ ∃𝑦(𝑓 Fn 𝑦 ∧ (𝑦𝐴 ∧ ∀𝑧𝑦 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑦) ∧ ∀𝑧𝑦 (𝑓𝑧) = (𝑧𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑧))))}
221, 21nfcxfr 2946 1 𝑥frecs(𝑅, 𝐴, 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wa 384  w3a 1100   = wceq 1637  wex 1859  {cab 2792  wnfc 2935  wral 3096  wss 3769   cuni 4630  cres 5313  Predcpred 5892   Fn wfn 6092  cfv 6097  (class class class)co 6870  frecscfrecs 32091
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-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-xp 5317  df-cnv 5319  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-iota 6060  df-fv 6105  df-ov 6873  df-frecs 32092
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator