Definition df-wrecs 8311

Description: Define the well-ordered recursive function generator. This function takes the usual expressions from recursion theorems and forms a unified definition. Specifically, given a function 𝐹, a relation 𝑅, and a base set 𝐴, this definition generates a function 𝐺 = wrecs(𝑅, 𝐴, 𝐹) that has property that, at any point 𝑥 ∈ 𝐴, (𝐺‘𝑥) = (𝐹‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑥))). See wfr1 8349, wfr2 8350, and wfr3 8351. (Contributed by Scott Fenton, 7-Jun-2018.) (Revised by BJ, 27-Oct-2024.)

Assertion

Ref	Expression
df-wrecs	⊢ wrecs(𝑅, 𝐴, 𝐹) = frecs(𝑅, 𝐴, (𝐹 ∘ 2nd ))

Detailed syntax breakdown of Definition df-wrecs

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3		cF	. . 3 class 𝐹
4	1, 2, 3	cwrecs 8310	. 2 class wrecs(𝑅, 𝐴, 𝐹)
5		c2nd 7986	. . . 4 class 2nd
6	3, 5	ccom 5676	. . 3 class (𝐹 ∘ 2nd )
7	1, 2, 6	cfrecs 8279	. 2 class frecs(𝑅, 𝐴, (𝐹 ∘ 2nd ))
8	4, 7	wceq 1534	1 wff wrecs(𝑅, 𝐴, 𝐹) = frecs(𝑅, 𝐴, (𝐹 ∘ 2nd ))

This definition is referenced by:  dfwrecsOLD  8312  wrecseq123  8313  nfwrecs  8315  csbwrecsg  8320  wfrrel  8343  wfrdmss  8344  wfrdmcl  8345  wfrfun  8346  wfrresex  8347  wfr2a  8348  wfr1  8349  dfrecs3  8386

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »