Metamath Proof Explorer - mmtheorems30

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Statement List for Metamath Proof Explorer - 2901-3000 - Page 30 of 58

Type	Label	Description
Statement
Theorem	fvresi 2901	The value of a restricted identity function.
⊢ (B ∈ A → ((I ↾ A) ‘B) = B)
Theorem	fconst2 2902	A constant function expressed as a cross product. See also fconstfv 2903.
⊢ B ∈ V    ⇒   ⊢ (F:A–→{B} ↔ F = (A × {B}))
Theorem	fconstfv 2903	A constant function expressed in terms of its functionality, domain, and value. See also fconst2 2902.
⊢ (F:A–→{B} ↔ (F Fn A ∧ ∀x ∈ A (F ‘x) = B))
Theorem	funfvima 2904	A function's value in a pre-image belongs to the image.
⊢ ((Fun F ∧ B ∈ dom F) → (B ∈ A → (F ‘B) ∈ (F “ A)))
Theorem	funfvima2 2905	A function's value in an included pre-image belongs to the image.
⊢ ((Fun F ∧ A ⊆ dom F) → (B ∈ A → (F ‘B) ∈ (F “ A)))
Theorem	funfvima3 2906	A class including a function contains the function's value in the image of the singleton of the argument.
⊢ ((Fun F ∧ F ⊆ G) → (A ∈ dom F → (F ‘A) ∈ (G “ {A})))
Theorem	fvclss 2907	Upper bound for the class of values of a class.
⊢ {y∣∃x y = (F ‘x)} ⊆ (ran F ∪ {∅})
Theorem	fvclex 2908	Existence of the class of values of a set.
⊢ F ∈ V    ⇒   ⊢ {y∣∃x y = (F ‘x)} ∈ V
Theorem	fvresex 2909	Existence of the class of values of a restricted class.
⊢ A ∈ V    ⇒   ⊢ {y∣∃x y = ((F ↾ A) ‘x)} ∈ V
Theorem	abrexexlem1 2910	Lemma for abrexex 2912. Shows the existence of a class of existentially restricted function values.
⊢ A ∈ V    ⇒   ⊢ {y∣∃x ∈ A y = (F ‘x)} ∈ V
Theorem	abrexexlem2 2911	Lemma for abrexex 2912. Almost there, but still requires that B be a set.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ {y∣∃x ∈ A y = B} ∈ V
Theorem	abrexex 2912	Existence of a class abstraction of existentially restricted sets. x is normally a free-variable parameter in B. This simple-looking theorem is actually quite powerful and involves the Axiom of Replacement in an intrinsic way, as can be seen by tracing back through the path abrexexlem2 2911, abrexexlem1 2910, fvresex 2909, resfunexg 2717, and funimaexg 2715. See also abrexex2 2915.
⊢ A ∈ V    ⇒   ⊢ {y∣∃x ∈ A y = B} ∈ V
Theorem	abrexexg 2913	Existence of a class abstraction of existentially restricted sets. x is normally a free-variable parameter in B. The antecedent assures us that A is a set.
⊢ (A ∈ C → {y∣∃x ∈ A y = B} ∈ V)
Theorem	iunex 2914	The existence of an indexed union. x is normally a free-variable parameter in B.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ∪x ∈ A B ∈ V
Theorem	abrexex2 2915	Existence of an existentially restricted class abstraction. φ is normally has free-variable parameters x and y. This is a powerful generalization of abrexex 2912.
⊢ A ∈ V    &   ⊢ {y∣φ} ∈ V    ⇒   ⊢ {y∣∃x ∈ A φ} ∈ V
Theorem	f1fv 2916	A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of [Monk1] p. 43.
⊢ (F:A–1-1→B ↔ (F:A–→B ∧ ∀x ∈ A ∀y ∈ A ((F ‘x) = (F ‘y) → x = y)))
Theorem	f1fvf 2917	A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of [Monk1] p. 43.
⊢ (z ∈ F → ∀x z ∈ F)    &   ⊢ (z ∈ F → ∀y z ∈ F)    ⇒   ⊢ (F:A–1-1→B ↔ (F:A–→B ∧ ∀x ∈ A ∀y ∈ A ((F ‘x) = (F ‘y) → x = y)))
Theorem	f1fveq 2918	Equality of function values for a one-to-one function.
⊢ ((F:A–1-1→B ∧ (C ∈ A ∧ D ∈ A)) → ((F ‘C) = (F ‘D) ↔ C = D))
Theorem	f1ocnvfv1 2919	The converse value of the value of a one-to-one onto function.
⊢ ((F:A–1-1-onto→B ∧ C ∈ A) → (◡F ‘(F ‘C)) = C)
Theorem	f1ocnvfv2 2920	The value of the converse value of a one-to-one onto function.
⊢ ((F:A–1-1-onto→B ∧ C ∈ B) → (F ‘(◡F ‘C)) = C)
Theorem	f1ocnvfv 2921	Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by Raph Levien, 10-Apr-04.)
⊢ ((F:A–1-1-onto→B ∧ C ∈ A) → ((F ‘C) = D → (◡F ‘D) = C))
Theorem	f1ocnvfvb 2922	Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by Raph Levien, 10-Apr-04.)
⊢ ((F:A–1-1-onto→B ∧ (C ∈ A ∧ D ∈ B)) → ((F ‘C) = D ↔ (◡F ‘D) = C))
Theorem	cbvfo 2923	Change bound variable between domain and range of function.
⊢ ((F ‘x) = y → (φ ↔ ψ))    ⇒   ⊢ (F:A–onto→B → (∀x ∈ A φ ↔ ∀y ∈ B ψ))
Theorem	cbvexfo 2924	Change bound variable between domain and range of function.
⊢ ((F ‘x) = y → (φ ↔ ψ))    ⇒   ⊢ (F:A–onto→B → (∃x ∈ A φ ↔ ∃y ∈ B ψ))
Theorem	isoeq1 2925	Equality theorem for isomorphisms.
⊢ (H = G → (H Isom R, S (A, B) ↔ G Isom R, S (A, B)))
Theorem	isoeq2 2926	Equality theorem for isomorphisms.
⊢ (R = T → (H Isom R, S (A, B) ↔ H Isom T, S (A, B)))
Theorem	isoeq3 2927	Equality theorem for isomorphisms.
⊢ (S = T → (H Isom R, S (A, B) ↔ H Isom R, T (A, B)))
Theorem	isoeq4 2928	Equality theorem for isomorphisms.
⊢ (A = C → (H Isom R, S (A, B) ↔ H Isom R, S (C, B)))
Theorem	isoeq5 2929	Equality theorem for isomorphisms.
⊢ (B = C → (H Isom R, S (A, B) ↔ H Isom R, S (A, C)))
Theorem	hbiso 2930	Bound-variable hypothesis builder for an isomorphism.
⊢ (y ∈ H → ∀x y ∈ H)    &   ⊢ (y ∈ R → ∀x y ∈ R)    &   ⊢ (y ∈ S → ∀x y ∈ S)    &   ⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (y ∈ B → ∀x y ∈ B)    ⇒   ⊢ (H Isom R, S (A, B) → ∀x H Isom R, S (A, B))
Theorem	isof1o 2931	An isomorphism is a one-to-one onto function.
⊢ (H Isom R, S (A, B) → H:A–1-1-onto→B)
Theorem	isorel 2932	An isomorphism connects binary relations via its function values.
⊢ ((H Isom R, S (A, B) ∧ (C ∈ A ∧ D ∈ A)) → (CRD ↔ (H ‘C)S(H ‘D)))
Theorem	isoid 2933	Identity law for isomorphism. Proposition 6.30(1) of [TakeutiZaring] p. 33.
⊢ (I ↾ A) Isom R, R (A, A)
Theorem	isocnv 2934	Converse law for isomorphism. Proposition 6.30(2) of [TakeutiZaring] p. 33.
⊢ (H Isom R, S (A, B) → ◡H Isom S, R (B, A))
Theorem	isotr 2935	Composition (transitive) law for isomorphism. Proposition 6.30(3) of [TakeutiZaring] p. 33.
⊢ ((H Isom R, S (A, B) ∧ G Isom S, T (B, C)) → (G ∘ H) Isom R, T (A, C))
Theorem	isotrALT 2936	Composition (transitive) law for isomorphism. Proposition 6.30(3) of [TakeutiZaring] p. 33. This proof is shorter than isotr 2935 in set.mm and uses fewer dummy variables, but it takes 240K vs. 207K for the web page.
⊢ ((H Isom R, S (A, B) ∧ G Isom S, T (B, C)) → (G ∘ H) Isom R, T (A, C))
Theorem	isomin 2937	Isomorphisms preserve minimal elements. Note that (◡R “ {D}) is Takeuti and Zaring's idiom for the initial segment {x∣xRD}. Proposition 6.31(1) of [TakeutiZaring] p. 33.
⊢ ((H Isom R, S (A, B) ∧ (C ⊆ A ∧ D ∈ A)) → ((C ∩ (◡R “ {D})) = ∅ ↔ ((H “ C) ∩ (◡S “ {(H ‘D)})) = ∅))
Theorem	isoini 2938	Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33.
⊢ ((H Isom R, S (A, B) ∧ D ∈ A) → (H “ (A ∩ (◡R “ {D}))) = (B ∩ (◡S “ {(H ‘D)})))
Theorem	isofrlem 2939	Lemma for isofr 2940.
⊢ (H Isom R, S (A, B) → (S Fr B → R Fr A))
Theorem	isofr 2940	An isomorphism preserves foundedness. Proposition 6.32(1) of [TakeutiZaring] p. 33.
⊢ (H Isom R, S (A, B) → (R Fr A ↔ S Fr B))
Theorem	isowe 2941	An isomorphism preserves well ordering. Proposition 6.32(3) of [TakeutiZaring] p. 33.
⊢ (H Isom R, S (A, B) → (R We A ↔ S We B))
Theorem	f1oiso 2942	Any one-to-one onto function determines an isomorphism with an induced relation S. Proposition 6.33 of [TakeutiZaring] p. 34.
⊢ ((H:A–1-1-onto→B ∧ S = {⟨z, w⟩∣∃x ∈ A ∃y ∈ A ((z = (H ‘x) ∧ w = (H ‘y)) ∧ xRy)}) → H Isom R, S (A, B))
Theorem	f1owe 2943	Well-ordering of isomorphic relations.
⊢ R = {⟨x, y⟩∣(F ‘x)S(F ‘y)}    ⇒   ⊢ (F:A–1-1-onto→B → (S We B → R We A))
Theorem	f1oweOLD 2944	Well-ordering of isomorphic relations.
⊢ R = {⟨x, y⟩∣(F ‘x)S(F ‘y)}    ⇒   ⊢ (F:A–1-1-onto→B → (S We B → R We A))
Theorem	canth 2945	No set A is equinumerous to its power set (Cantor's theorem), i.e. no function can map A it onto its power set. Compare Theorem 6B(b) of [Enderton] p. 132. For the equinumerosity version, see canth2 3381. Note that A must be a set: this theorem does not hold when A is too large to be a set; see ncanth 2946 for a counterexample.
⊢ A ∈ V    ⇒   ⊢ ¬ F:A–onto→℘A
Theorem	ncanth 2946	Cantor's theorem fails for the universal class (which is not a set but a proper class by nvelv 1483). Specifically, the identity function maps the universe onto its power class. Compare canth 2945 that works for sets. See also the remark in ru 1437 about NF, in which Cantor's theorem fails for sets that are "too large." This theorem gives some intuition behind that failure, since in NF the universal class is a set.
⊢ I:V–onto→℘V
Theorem	iunon 2947	The indexed union of a set of ordinal numbers is an ordinal number. B normally has free variable x as a parameter.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (∀x ∈ A B ∈ On → ∪x ∈ A B ∈ On)
Theorem	iinon 2948	The indexed intersection of a non-empty class of ordinal numbers is an ordinal number. B normally has free variable x as a parameter. Note that A may be a proper class.
⊢ B ∈ V    ⇒   ⊢ ((∀x ∈ A B ∈ On ∧ ¬ A = ∅) → ∩x ∈ A B ∈ On)
Theorem	tfrlem1 2949	A technical lemma for transfinite recursion. Compare Lemma 1 of [TakeutiZaring] p. 47.
⊢ (A ∈ On → ((F Fn A ∧ G Fn A) → (∀x ∈ A ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → ∀x ∈ A (F ‘x) = (G ‘x))))
Theorem	tfrlem2 2950	Lemma for transfinite recursion. This provides some messy details needed to link tfrlem1 2949 into the main proof.
⊢ ((F Fn A ∧ G Fn A) → ((⟨x, y⟩ ∈ F ∧ ⟨x, z⟩ ∈ G) → (A ∈ On → (∀w(A ∈ On → (w ∈ A → ((F ‘w) = (B ‘(F ↾ w)) ∧ (G ‘w) = (B ‘(G ↾ w))))) → y = z))))
Theorem	tfrlem3 2951	Lemma for transfinite recursion. Let A be the class of "acceptable" functions. The final thing we're interested in is the union of all these acceptable functions. This lemma just changes the bound variables in A for later use.
⊢ A = {f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))}    ⇒   ⊢ A = {g∣∃z ∈ On (g Fn z ∧ ∀y ∈ z (g ‘y) = (G ‘(g ↾ y)))}
Theorem	tfrlem4 2952	Lemma for transfinite recursion. A is the class of all "acceptable" functions, and F is their union. First we show that an acceptable function is in fact a function.
⊢ A = {f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))}    &   ⊢ F = ∪A    ⇒   ⊢ (g ∈ A → Fun g)
Theorem	tfrlem5 2953	Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains.
⊢ A = {f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))}    &   ⊢ F = ∪A    ⇒   ⊢ ((g ∈ A ∧ h ∈ A) → ((⟨x, u⟩ ∈ g ∧ ⟨x, v⟩ ∈ h) → u = v))
Theorem	tfrlem6 2954	Lemma for transfinite recursion. The union of all acceptable functions is a relation.
⊢ A = {f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))}    &   ⊢ F = ∪A    ⇒   ⊢ Rel F
Theorem	tfrlem7 2955	Lemma for transfinite recursion. The union of all acceptable functions is a function.
⊢ A = {f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))}    &   ⊢ F = ∪A    ⇒   ⊢ Fun F
Theorem	tfrlem8 2956	Lemma for transfinite recursion. The domain of F is ordinal.
⊢ A = {f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))}    &   ⊢ F = ∪A    ⇒   ⊢ Ord dom F
Theorem	tfrlem9 2957	Lemma for transfinite recursion. Here we compute the value of F (the union of all acceptable functions).
⊢ A = {f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))}    &   ⊢ F = ∪A    ⇒   ⊢ (y ∈ dom F → (F ‘y) = (G ‘(F ↾ y)))
Theorem	tfrlem10 2958	Lemma for transfinite recursion. We define class C by extending F with one ordered pair. We will assume, falsely, that domain of F is a member of, and thus not equal to, On. Using this assumption we will prove facts about C that will lead to a contradiction in tfrlem13 2961, thus showing the domain of F does in fact equal On. Here we show (under the false assumption) that C is a function extending the domain of F by one.
⊢ A = {f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))}    &   ⊢ F = ∪A    &   ⊢ C = (F ∪ {⟨dom F, (G ‘(F ↾ dom F))⟩})    ⇒   ⊢ (dom F ∈ On → C Fn suc dom F)
Theorem	tfrlem11 2959	Lemma for transfinite recursion. Compute the value of C.
⊢ A = {f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))}    &   ⊢ F = ∪A    &   ⊢ C = (F ∪ {⟨dom F, (G ‘(F ↾ dom F))⟩})    ⇒   ⊢ (dom F ∈ On → (y ∈ suc dom F → (C ‘y) = (G ‘(C ↾ y))))
Theorem	tfrlem12 2960	Lemma for transfinite recursion. Show C is an acceptable function.
⊢ A = {f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))}    &   ⊢ F = ∪A    &   ⊢ C = (F ∪ {⟨dom F, (G ‘(F ↾ dom F))⟩})    ⇒   ⊢ (dom F ∈ On → C ∈ A)
Theorem	tfrlem13 2961	Lemma for transfinite recursion. If dom F is in On, then C is acceptable, and thus a subset of F, but dom C is bigger than dom F. This is a contradiction, so dom F must be On.
⊢ A = {f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))}    &   ⊢ F = ∪A    &   ⊢ C = (F ∪ {⟨dom F, (G ‘(F ↾ dom F))⟩})    ⇒   ⊢ dom F = On
Theorem	tfr1 2962	Principle of Transfinite Recursion, part 1 of 3. Theorem 7.41(1) of [TakeutiZaring] p. 47. We start with an arbitrary class G, normally a function, and define a class A of all "acceptable" functions. The final function we're interested in is the union F of them. F is then said to be defined by transfinite recursion. The purpose of the 3 parts of this theorem is to demonstrate properties of F. In this first part we show that F is a function whose domain is all ordinal numbers.
⊢ A = {f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))}    &   ⊢ F = ∪A    ⇒   ⊢ F Fn On
Theorem	tfr2 2963	Principle of Transfinite Recursion, part 2 of 3. Theorem 7.41(2) of [TakeutiZaring] p. 47. Here we show that the function F has the property that for any function G whatsoever, the "next" value of F is G recursively applied to all "previous" values of F.
⊢ A = {f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))}    &   ⊢ F = ∪A    ⇒   ⊢ (z ∈ On → (F ‘z) = (G ‘(F ↾ z)))
Theorem	tfr3 2964	Principle of Transfinite Recursion, part 3 of 3. Theorem 7.41(3) of [TakeutiZaring] p. 47. Finally we show that F is unique. We do this by showing that any class B with the same properties of F that we showed in parts 1 and 2 is identical to F.
⊢ A = {f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))}    &   ⊢ F = ∪A    ⇒   ⊢ ((B Fn On ∧ ∀x ∈ On (B ‘x) = (G ‘(B ↾ x))) → B = F)
Theorem	tz7.44lem1 2965	G is a function. Lemma for tz7.44-1 2966, tz7.44-2 2967, and tz7.44-3 2968.
⊢ G = {⟨x, y⟩∣((x = ∅ ∧ y = A) ∨ (¬ (x = ∅ ∨ Lim dom x) ∧ y = (H ‘(x ‘∪dom x))) ∨ (Lim dom x ∧ y = ∪ran x))}    ⇒   ⊢ Fun G
Theorem	tz7.44-1 2966	The value of F at ∅. Part 1 of Theorem 7.44 of [TakeutiZaring] p. 49.
⊢ G = {⟨x, y⟩∣((x = ∅ ∧ y = A) ∨ (¬ (x = ∅ ∨ Lim dom x) ∧ y = (H ‘(x ‘∪dom x))) ∨ (Lim dom x ∧ y = ∪ran x))}    &   ⊢ F Fn On    &   ⊢ (x ∈ On → (F ‘x) = (G ‘(F ↾ x)))    &   ⊢ A ∈ V    ⇒   ⊢ (F ‘∅) = A
Theorem	tz7.44-2 2967	The value of F at a successor ordinal. Part 2 of Theorem 7.44 of [TakeutiZaring] p. 49.
⊢ G = {⟨x, y⟩∣((x = ∅ ∧ y = A) ∨ (¬ (x = ∅ ∨ Lim dom x) ∧ y = (H ‘(x ‘∪dom x))) ∨ (Lim dom x ∧ y = ∪ran x))}    &   ⊢ F Fn On    &   ⊢ (x ∈ On → (F ‘x) = (G ‘(F ↾ x)))    &   ⊢ B ∈ On    ⇒   ⊢ (F ‘suc B) = (H ‘(F ‘B))
Theorem	tz7.44-3 2968	The value of F at a limit ordinal. Part 3 of Theorem 7.44 of [TakeutiZaring] p. 49.
⊢ G = {⟨x, y⟩∣((x = ∅ ∧ y = A) ∨ (¬ (x = ∅ ∨ Lim dom x) ∧ y = (H ‘(x ‘∪dom x))) ∨ (Lim dom x ∧ y = ∪ran x))}    &   ⊢ F Fn On    &   ⊢ (x ∈ On → (F ‘x) = (G ‘(F ↾ x)))    &   ⊢ B ∈ On    ⇒   ⊢ (Lim B → (F ‘B) = ∪(F “ B))
Syntax	crdg 2969	Extend class notation with the recursive definition generator.
class rec(A, B)
Definition	df-rdg 2970	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).
⊢ 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)))}
Definition	df-rdgNEW 2971	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). Note that the if operator (see df-if 1777) selects cases based on whether g is zero, has a limit ordinal domain, or has a successor domain.
⊢ rec(F, A) = ∪{f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = ({⟨g, z⟩∣z = if(g = ∅, A, if(Lim dom g, ∪ran g, (F ‘(g ‘∪dom g))))} ‘(f ↾ y)))}
Theorem	rdgeq1 2972	Equality theorem for the recursive definition generator.
⊢ (F = G → rec(F, A) = rec(G, A))
Theorem	rdgeq2 2973	Equality theorem for the recursive definition generator.
⊢ (A = B → rec(F, A) = rec(F, B))
Theorem	hbrdg 2974	Bound-variable hypothesis builder for the recursive definition generator.
⊢ (y ∈ F → ∀x y ∈ F)    &   ⊢ (y ∈ A → ∀x y ∈ A)    ⇒   ⊢ (y ∈ rec(F, A) → ∀x y ∈ rec(F, A))
Theorem	rdglem1 2975	Lemma used with the recursive definition generator. This is a trivial lemma that just changes bound variables for later use.
⊢ {f∣∃x ∈ On (f Fn x ∧ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))} = {g∣∃z ∈ On (g Fn z ∧ ∀w ∈ z (g ‘w) = (G ‘(g ↾ w)))}
Theorem	rdglem2 2976	Lemma used with the recursive definition generator. This is a trivial lemma that just changes bound variables for later use.
⊢ {⟨x, y⟩∣((x = ∅ ∧ y = A) ∨ (¬ (x = ∅ ∨ Lim dom x) ∧ y = (H ‘(x ‘∪dom x))) ∨ (Lim dom x ∧ y = ∪ran x))} = {⟨z, y⟩∣((z = ∅ ∧ y = A) ∨ (¬ (z = ∅ ∨ Lim dom z) ∧ y = (H ‘(z ‘∪dom z))) ∨ (Lim dom z ∧ y = ∪ran z))}
Theorem	rdgfnon 2977	The recursive definition generator is a function on ordinal numbers.
⊢ rec(F, A) Fn On
Theorem	rdgval 2978	Value of the recursive definition generator.
⊢ (g ∈ On → (rec(F, A) ‘g) = ({⟨w, z⟩∣((w = ∅ ∧ z = A) ∨ (¬ (w = ∅ ∨ Lim dom w) ∧ z = (F ‘(w ‘∪dom w))) ∨ (Lim dom w ∧ z = ∪ran w))} ‘(rec(F, A) ↾ g)))
Theorem	rdgzer 2979	The initial value of the recursive definition generator.
⊢ A ∈ V    ⇒   ⊢ (rec(F, A) ‘∅) = A
Theorem	rdgsuc 2980	The value of the recursive definition generator at a successor.
⊢ B ∈ On    ⇒   ⊢ (rec(F, A) ‘suc B) = (F ‘(rec(F, A) ‘B))
Theorem	rdglim 2981	The value of the recursive definition generator at a limit ordinal.
⊢ B ∈ On    ⇒   ⊢ (Lim B → (rec(F, A) ‘B) = ∪(rec(F, A) “ B))
Theorem	rdgzert 2982	The initial value of the recursive definition generator.
⊢ (A ∈ C → (rec(F, A) ‘∅) = A)
Theorem	rdgsuct 2983	The value of the recursive definition generator at a successor.
⊢ (B ∈ On → (rec(F, A) ‘suc B) = (F ‘(rec(F, A) ‘B)))
Theorem	rdgsucopab 2984	The value of the recursive definition generator at a successor (special case where the characteristic function is an ordered pair abstraction).
⊢ (z ∈ A → ∀x z ∈ A)    &   ⊢ (z ∈ B → ∀x z ∈ B)    &   ⊢ (z ∈ D → ∀x z ∈ D)    &   ⊢ F = rec({⟨x, y⟩∣y = C}, A)    &   ⊢ (x = (F ‘B) → C = D)    ⇒   ⊢ ((B ∈ On ∧ D ∈ R) → (F ‘suc B) = D)
Theorem	rdgsucopabn 2985	The value of the recursive definition generator at a successor (special case where the characteristic function is an ordered pair abstraction and where the mapping class D is a proper class). This is a technical lemma that can be used together with rdgsucopab 2984 to help eliminate redundant sethood antecedents.
⊢ (z ∈ A → ∀x z ∈ A)    &   ⊢ (z ∈ B → ∀x z ∈ B)    &   ⊢ (z ∈ D → ∀x z ∈ D)    &   ⊢ F = rec({⟨x, y⟩∣y = C}, A)    &   ⊢ (x = (F ‘B) → C = D)    ⇒   ⊢ (¬ D ∈ V → (F ‘suc B) = ∅)
Theorem	rdglimt 2986	The value of the recursive definition generator at a limit ordinal.
⊢ ((B ∈ C ∧ Lim B) → (rec(F, A) ‘B) = ∪(rec(F, A) “ B))
Theorem	rdglim2 2987	The value of the recursive definition generator at a limit ordinal, in terms of the union of all smaller values.
⊢ ((B ∈ C ∧ Lim B) → (rec(F, A) ‘B) = ∪{y∣∃x ∈ B y = (rec(F, A) ‘x)})
Theorem	rdglim2a 2988	The value of the recursive definition generator at a limit ordinal, in terms of indexed union of all smaller values.
⊢ ((B ∈ C ∧ Lim B) → (rec(F, A) ‘B) = ∪x ∈ B (rec(F, A) ‘x))
Theorem	frfnom 2989	The function generated by finite recursive definition generation is a function on omega.
⊢ (rec(F, A) ↾ ω) Fn ω
Theorem	frzer 2990	The initial value resulting from finite recursive definition generation.
⊢ (A ∈ B → ((rec(F, A) ↾ ω) ‘∅) = A)
Theorem	frsuc 2991	The successor value resulting from finite recursive definition generation.
⊢ (B ∈ ω → ((rec(F, A) ↾ ω) ‘suc B) = (F ‘((rec(F, A) ↾ ω) ‘B)))
Theorem	frsucopab 2992	The successor value resulting from finite recursive definition generation (special case where the generation function is an ordered pair abstraction).
⊢ (z ∈ A → ∀x z ∈ A)    &   ⊢ (z ∈ B → ∀x z ∈ B)    &   ⊢ (z ∈ D → ∀x z ∈ D)    &   ⊢ F = (rec({⟨x, y⟩∣y = C}, A) ↾ ω)    &   ⊢ (x = (F ‘B) → C = D)    ⇒   ⊢ ((B ∈ ω ∧ D ∈ R) → (F ‘suc B) = D)
Theorem	tz7.48lem 2993	A way of showing an ordinal function is one-to