Metamath Proof Explorer

Home

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Definition df-rdgNEW 2971

Description: Define a recursive definition generator on

(the class of ordinal numbers) with characteristic function

and initial value

. This combines functions

in tfr1 2962 and

in tz7.44-1 2966 into one definition. This rather amazing operation allows us to define, with compact direct definitions, functions that are usually defined in textbooks only with indirect self-referencing recursive definitions. A recursive definition requires advanced metalogic to justify - in particular, eliminating a recursive definition is very difficult and often not even shown in textbooks. On the other hand, the elimination of a direct definition is a matter of simple mechanical substitution. The price paid is the mind-boggling complexity of our

operation. But once we get past this hurdle, otherwise recursive definitions become relatively simple, as in, for example, df-aleph 3624. From the direct definition we can prove textbook recursive definitions as theorems using rdgzer 2979, rdgsuc 2980, and rdglim 2981. We can also restrict the

operation to define otherwise recursive functions on the natural numbers

; see frzer 2990 and frsuc 2991. Our

operation apparently does not appear in published literature, although closely related is Definition 25.2 of [Quine] p. 177, which he uses to "turn...a recursion into a genuine or direct definition" (p. 174). Note that the

operator (see df-if 1777) selects cases based on whether

is zero, has a limit ordinal domain, or has a successor domain.

**Assertion**
Ref	Expression
df-rdgNEW	$/\$

Distinct variable group(s):

**Detailed syntax breakdown of Definition df-rdgNEW**
Step	Hyp	Ref	Expression
1		cF	. . 3
2		cA	. . 3
3	1, 2	crdg 2969	. 2
4		vf	. . . . . . . 8
5	4	cv 1089	. . . . . . 7
6		vx	. . . . . . . 8
7	6	cv 1089	. . . . . . 7
8	5, 7	wfn 2417	. . . . . 6
9		vy	. . . . . . . . . 10
10	9	cv 1089	. . . . . . . . 9
11	10, 5	cfv 2422	. . . . . . . 8
12	5, 10	cres 2412	. . . . . . . . 9
13		vz	. . . . . . . . . . . 12
14	13	cv 1089	. . . . . . . . . . 11
15		vg	. . . . . . . . . . . . . 14
16	15	cv 1089	. . . . . . . . . . . . 13
17		c0 1707	. . . . . . . . . . . . 13
18	16, 17	wceq 1091	. . . . . . . . . . . 12
19	16	cdm 2410	. . . . . . . . . . . . . 14
20	19	wlim 2200	. . . . . . . . . . . . 13
21	16	crn 2411	. . . . . . . . . . . . . 14
22	21	cuni 1919	. . . . . . . . . . . . 13
23	19	cuni 1919	. . . . . . . . . . . . . . 15
24	23, 16	cfv 2422	. . . . . . . . . . . . . 14
25	24, 1	cfv 2422	. . . . . . . . . . . . 13
26	20, 22, 25	cif 1776	. . . . . . . . . . . 12
27	18, 2, 26	cif 1776	. . . . . . . . . . 11
28	14, 27	wceq 1091	. . . . . . . . . 10
29	28, 15, 13	copab 2055	. . . . . . . . 9
30	12, 29	cfv 2422	. . . . . . . 8
31	11, 30	wceq 1091	. . . . . . 7
32	31, 9, 7	wral 1201	. . . . . 6
33	8, 32	wa 196	. . . . 5 $/\$
34		con0 2199	. . . . 5
35	33, 6, 34	wrex 1202	. . . 4 $/\$
36	35, 4	cab 1090	. . 3 $/\$
37	36	cuni 1919	. 2 $/\$
38	3, 37	wceq 1091	1 $/\$

Colors of variables: wff set class

metamath.org