Definition df-rdg 2970

Description: Define a recursive definition generator on On (the class of ordinal numbers) with characteristic function F and initial value A. This combines functions F in tfr1 2962 and G 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 rec 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 rec operation to define otherwise recursive functions on the natural numbers ω; see frzer 2990 and frsuc 2991. Our rec 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).

Assertion

Ref	Expression
df-rdg	⊢ rec(F, A) = ∪{f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = ({⟨g, z⟩∣((g = ∅ ∧ z = A) ∨ (¬ (g = ∅ ∨ Lim dom g) ∧ z = (F ‘(g ‘∪dom g))) ∨ (Lim dom g ∧ z = ∪ran g))} ‘(f ↾ y)))}

Distinct variable group(s):   x,y,z,f,g,F   x,A,y,z,f,g

Detailed syntax breakdown of Definition df-rdg

Step	Hyp	Ref	Expression
1		cF	. . 3 class F
2		cA	. . 3 class A
3	1, 2	crdg 2969	. 2 class rec(F, A)
4		vf	. . . . . . . 8 set f
5	4	cv 1089	. . . . . . 7 class f
6		vx	. . . . . . . 8 set x
7	6	cv 1089	. . . . . . 7 class x
8	5, 7	wfn 2417	. . . . . 6 wff f Fn x
9		vy	. . . . . . . . . 10 set y
10	9	cv 1089	. . . . . . . . 9 class y
11	10, 5	cfv 2422	. . . . . . . 8 class (f ‘y)
12	5, 10	cres 2412	. . . . . . . . 9 class (f ↾ y)
13		vg	. . . . . . . . . . . . . 14 set g
14	13	cv 1089	. . . . . . . . . . . . 13 class g
15		c0 1707	. . . . . . . . . . . . 13 class ∅
16	14, 15	wceq 1091	. . . . . . . . . . . 12 wff g = ∅
17		vz	. . . . . . . . . . . . . 14 set z
18	17	cv 1089	. . . . . . . . . . . . 13 class z
19	18, 2	wceq 1091	. . . . . . . . . . . 12 wff z = A
20	16, 19	wa 196	. . . . . . . . . . 11 wff (g = ∅ ∧ z = A)
21	14	cdm 2410	. . . . . . . . . . . . . . 15 class dom g
22	21	wlim 2200	. . . . . . . . . . . . . 14 wff Lim dom g
23	16, 22	wo 195	. . . . . . . . . . . . 13 wff (g = ∅ ∨ Lim dom g)
24	23	wn 1	. . . . . . . . . . . 12 wff ¬ (g = ∅ ∨ Lim dom g)
25	21	cuni 1919	. . . . . . . . . . . . . . 15 class ∪dom g
26	25, 14	cfv 2422	. . . . . . . . . . . . . 14 class (g ‘∪dom g)
27	26, 1	cfv 2422	. . . . . . . . . . . . 13 class (F ‘(g ‘∪dom g))
28	18, 27	wceq 1091	. . . . . . . . . . . 12 wff z = (F ‘(g ‘∪dom g))
29	24, 28	wa 196	. . . . . . . . . . 11 wff (¬ (g = ∅ ∨ Lim dom g) ∧ z = (F ‘(g ‘∪dom g)))
30	14	crn 2411	. . . . . . . . . . . . . 14 class ran g
31	30	cuni 1919	. . . . . . . . . . . . 13 class ∪ran g
32	18, 31	wceq 1091	. . . . . . . . . . . 12 wff z = ∪ran g
33	22, 32	wa 196	. . . . . . . . . . 11 wff (Lim dom g ∧ z = ∪ran g)
34	20, 29, 33	w3o 580	. . . . . . . . . 10 wff ((g = ∅ ∧ z = A) ∨ (¬ (g = ∅ ∨ Lim dom g) ∧ z = (F ‘(g ‘∪dom g))) ∨ (Lim dom g ∧ z = ∪ran g))
35	34, 13, 17	copab 2055	. . . . . . . . 9 class {⟨g, z⟩∣((g = ∅ ∧ z = A) ∨ (¬ (g = ∅ ∨ Lim dom g) ∧ z = (F ‘(g ‘∪dom g))) ∨ (Lim dom g ∧ z = ∪ran g))}
36	12, 35	cfv 2422	. . . . . . . 8 class ({⟨g, z⟩∣((g = ∅ ∧ z = A) ∨ (¬ (g = ∅ ∨ Lim dom g) ∧ z = (F ‘(g ‘∪dom g))) ∨ (Lim dom g ∧ z = ∪ran g))} ‘(f ↾ y))
37	11, 36	wceq 1091	. . . . . . 7 wff (f ‘y) = ({⟨g, z⟩∣((g = ∅ ∧ z = A) ∨ (¬ (g = ∅ ∨ Lim dom g) ∧ z = (F ‘(g ‘∪dom g))) ∨ (Lim dom g ∧ z = ∪ran g))} ‘(f ↾ y))
38	37, 9, 7	wral 1201	. . . . . 6 wff ∀y ∈ x (f ‘y) = ({⟨g, z⟩∣((g = ∅ ∧ z = A) ∨ (¬ (g = ∅ ∨ Lim dom g) ∧ z = (F ‘(g ‘∪dom g))) ∨ (Lim dom g ∧ z = ∪ran g))} ‘(f ↾ y))
39	8, 38	wa 196	. . . . 5 wff (f Fn x ∧ ∀y ∈ x (f ‘y) = ({⟨g, z⟩∣((g = ∅ ∧ z = A) ∨ (¬ (g = ∅ ∨ Lim dom g) ∧ z = (F ‘(g ‘∪dom g))) ∨ (Lim dom g ∧ z = ∪ran g))} ‘(f ↾ y)))
40		con0 2199	. . . . 5 class On
41	39, 6, 40	wrex 1202	. . . 4 wff ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = ({⟨g, z⟩∣((g = ∅ ∧ z = A) ∨ (¬ (g = ∅ ∨ Lim dom g) ∧ z = (F ‘(g ‘∪dom g))) ∨ (Lim dom g ∧ z = ∪ran g))} ‘(f ↾ y)))
42	41, 4	cab 1090	. . 3 class {f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = ({⟨g, z⟩∣((g = ∅ ∧ z = A) ∨ (¬ (g = ∅ ∨ Lim dom g) ∧ z = (F ‘(g ‘∪dom g))) ∨ (Lim dom g ∧ z = ∪ran g))} ‘(f ↾ y)))}
43	42	cuni 1919	. 2 class ∪{f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = ({⟨g, z⟩∣((g = ∅ ∧ z = A) ∨ (¬ (g = ∅ ∨ Lim dom g) ∧ z = (F ‘(g ‘∪dom g))) ∨ (Lim dom g ∧ z = ∪ran g))} ‘(f ↾ y)))}
44	3, 43	wceq 1091	1 wff rec(F, A) = ∪{f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = ({⟨g, z⟩∣((g = ∅ ∧ z = A) ∨ (¬ (g = ∅ ∨ Lim dom g) ∧ z = (F ‘(g ‘∪dom g))) ∨ (Lim dom g ∧ z = ∪ran g))} ‘(f ↾ y)))}

This definition is referenced by:  rdgeq1 2972  rdgeq2 2973  hbrdg 2974  rdgfnon 2977  rdgval 2978

metamath.org