Intuitionistic Logic Explorer Home Intuitionistic Logic Explorer
Most Recent Proofs 		 
Mirrors  >  Home  >  ILE Home  >  Th. List  >  Recent MPE Most Recent             Other  >  MM 100
Most recent proofs    These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the iset.mm database for the Intuitionistic Logic Explorer. The iset.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from the commit given on the MPE Most Recent Proofs page. The database from that commit is also available here: iset.mm.

See the MPE Most Recent Proofs page for news and some useful links.

Color key:   Intuitionistic Logic Explorer  Intuitionistic Logic Explorer   User Mathboxes  User Mathboxes  

Last updated on 18-Aug-2019 at 7:42 PM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
16-Aug-2019frecabex 5865 The class abstraction from df-frec 5864 exists. This is a lemma for several other finite recursion proofs. (Contributed by Jim Kingdon, 16-Aug-2019.)
⊢ (φ → 𝑆 ∈ 𝑉)    &   ⊢ (φ → 𝐹 Fn V)    &   ⊢ (φ → A ∈ 𝑊)    ⇒   ⊢ (φ → {x ∣ (∃𝑚 ∈ 𝜔 (dom 𝑆 = suc 𝑚 ∧ x ∈ (𝐹‘(𝑆‘𝑚))) ∨ (dom 𝑆 = ∅ ∧ x ∈ A))} ∈ V)
 
15-Aug-2019frecsuc 5873 The successor value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 15-Aug-2019.)
⊢ ((𝐹 Fn V ∧ A ∈ 𝑉 ∧ B ∈ 𝜔) → (frec(𝐹, A)‘suc B) = (𝐹‘(frec(𝐹, A)‘B)))
 
15-Aug-2019frecsuclem3 5872 Lemma for frecsuc 5873. (Contributed by Jim Kingdon, 15-Aug-2019.)
⊢ 𝐺 = (g ∈ V ↦ {x ∣ (∃𝑚 ∈ 𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom g = ∅ ∧ x ∈ A))})    ⇒   ⊢ ((𝐹 Fn V ∧ A ∈ 𝑉 ∧ B ∈ 𝜔) → (frec(𝐹, A)‘suc B) = (𝐹‘(frec(𝐹, A)‘B)))
 
15-Aug-2019frecsuclem2 5871 Lemma for frecsuc 5873. (Contributed by Jim Kingdon, 15-Aug-2019.)
⊢ 𝐺 = (g ∈ V ↦ {x ∣ (∃𝑚 ∈ 𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom g = ∅ ∧ x ∈ A))})    ⇒   ⊢ ((𝐹 Fn V ∧ A ∈ 𝑉 ∧ B ∈ 𝜔) → ((recs(𝐺) ↾ suc B)‘B) = (frec(𝐹, A)‘B))
 
15-Aug-2019frecsuclemdm 5870 Lemma for frecsuc 5873. (Contributed by Jim Kingdon, 15-Aug-2019.)
⊢ 𝐺 = (g ∈ V ↦ {x ∣ (∃𝑚 ∈ 𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom g = ∅ ∧ x ∈ A))})    ⇒   ⊢ ((𝐹 Fn V ∧ A ∈ 𝑉 ∧ B ∈ 𝜔) → dom (recs(𝐺) ↾ suc B) = suc B)
 
15-Aug-2019frectfr 5866 Lemma to connect transfinite recursion theorems with finite recursion. That is, given the conditions 𝐹 Fn V and A ∈ 𝑉 on frec(𝐹, A), we want to be able to apply tfri1d 5836 or tfri2d 5837, and this lemma lets us satisfy hypotheses of those theorems.

(Contributed by Jim Kingdon, 15-Aug-2019.)

⊢ 𝐺 = (g ∈ V ↦ {x ∣ (∃𝑚 ∈ 𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom g = ∅ ∧ x ∈ A))})    ⇒   ⊢ ((𝐹 Fn V ∧ A ∈ 𝑉) → ∀y(Fun 𝐺 ∧ (𝐺‘y) ∈ V))
 
13-Aug-2019frecsuclem1 5869 Lemma for frecsuc 5873. (Contributed by Jim Kingdon, 13-Aug-2019.)
⊢ 𝐺 = (g ∈ V ↦ {x ∣ (∃𝑚 ∈ 𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom g = ∅ ∧ x ∈ A))})    ⇒   ⊢ ((𝐹 Fn V ∧ A ∈ 𝑉 ∧ B ∈ 𝜔) → (frec(𝐹, A)‘suc B) = (𝐺‘(recs(𝐺) ↾ suc B)))
 
12-Aug-2019oav2 5922 Value of ordinal addition. (Contributed by Mario Carneiro and Jim Kingdon, 12-Aug-2019.)
⊢ ((A ∈ On ∧ B ∈ On) → (A +𝑜 B) = (A ∪ ∪ x ∈ B suc (A +𝑜 x)))
 
11-Aug-2019frec0g 5868 The initial value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 11-Aug-2019.)
⊢ ((𝐹 Fn V ∧ A ∈ 𝑉) → (frec(𝐹, A)‘∅) = A)
 
11-Aug-2019frecfnom 5867 The function generated by finite recursive definition generation is a function on omega. (Contributed by Jim Kingdon, 11-Aug-2019.)
⊢ ((𝐹 Fn V ∧ A ∈ 𝑉) → frec(𝐹, A) Fn 𝜔)
 
10-Aug-2019df-frec 5864 Define a recursive definition generator on 𝜔 (the class of finite ordinals) with characteristic function 𝐹 and initial value 𝐼. 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 daunting complexity of our frec operation (especially when df-recs 5807 that it is built on is also eliminated). But once we get past this hurdle, definitions that would otherwise be recursive become relatively simple; see frec0g 5868 and frecsuc 5873.

Unlike with transfinite recursion, finite recurson can readily divide definitions and proofs into zero and successor cases, because even without excluded middle we have theorems such as nn0suc 4223. The analogous situation with transfinite recursion - being able to say that an ordinal is zero, successor, or limit - is enabled by excluded middle and thus is not available to us.

Note: We introduce frec with the philosophical goal of being able to eliminate all definitions with direct mechanical substitution and to verify easily the soundness of definitions. Metamath itself has no built-in technical limitation that prevents multiple-part recursive definitions in the traditional textbook style. (Contributed by Mario Carneiro and Jim Kingdon, 10-Aug-2019.)

⊢ frec(𝐹, 𝐼) = (recs((g ∈ V ↦ {x ∣ (∃𝑚 ∈ 𝜔 (dom g = suc 𝑚 ∧ x ∈ (𝐹‘(g‘𝑚))) ∨ (dom g = ∅ ∧ x ∈ 𝐼))})) ↾ 𝜔)
 
7-Aug-2019acexmidlem1 5401 Lemma for acexmid 5404. List the cases identified in acexmidlemcase 5400 and hook them up to the lemmas which handle each case. (Contributed by Jim Kingdon, 7-Aug-2019.)
⊢ A = {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)}    &   ⊢ B = {x ∈ {∅, {∅}} ∣ (x = {∅} ∨ φ)}    &   ⊢ 𝐶 = {A, B}    ⇒   ⊢ (∀z ∈ 𝐶 ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u) → (φ ∨ ¬ φ))
 
7-Aug-2019acexmidlemcase 5400 Lemma for acexmid 5404. Here we divide the proof into cases (based on the disjunction implicit in an unordered pair, not the sort of case elimination which relies on excluded middle).

The cases are (1) the choice function evaluated at A equals {∅}, (2) the choice function evaluated at B equals ∅, and (3) the choice function evaluated at A equals ∅ and the choice function evaluated at B equals {∅}.

Because of the way we represent the choice function y, the choice function evaluated at A is (℩v ∈ A∃u ∈ y(A ∈ u ∧ v ∈ u)) and the choice function evaluated at B is (℩v ∈ B∃u ∈ y(B ∈ u ∧ v ∈ u)). Other than the difference in notation these work just as (y‘A) and (y‘B) would if y were a function as defined by df-fun 4798.

Although it isn't exactly about the division into cases, it is also convenient for this lemma to also include the step that if the choice function evaluated at A equals {∅}, then {∅} ∈ A and likewise for B.

(Contributed by Jim Kingdon, 7-Aug-2019.)

⊢ A = {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)}    &   ⊢ B = {x ∈ {∅, {∅}} ∣ (x = {∅} ∨ φ)}    &   ⊢ 𝐶 = {A, B}    ⇒   ⊢ (∀z ∈ 𝐶 ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u) → ({∅} ∈ A ∨ ∅ ∈ B ∨ ((℩v ∈ A ∃u ∈ y (A ∈ u ∧ v ∈ u)) = ∅ ∧ (℩v ∈ B ∃u ∈ y (B ∈ u ∧ v ∈ u)) = {∅})))
 
6-Aug-2019acexmidlemv 5403 Lemma for acexmid 5404.

This is acexmid 5404 with additional distinct variable constraints, most notably between φ and x.

(Contributed by Jim Kingdon, 6-Aug-2019.)

⊢ ∃y∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)    ⇒   ⊢ (φ ∨ ¬ φ)
 
6-Aug-2019acexmidlemab 5399 Lemma for acexmid 5404. (Contributed by Jim Kingdon, 6-Aug-2019.)
⊢ A = {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)}    &   ⊢ B = {x ∈ {∅, {∅}} ∣ (x = {∅} ∨ φ)}    &   ⊢ 𝐶 = {A, B}    ⇒   ⊢ (((℩v ∈ A ∃u ∈ y (A ∈ u ∧ v ∈ u)) = ∅ ∧ (℩v ∈ B ∃u ∈ y (B ∈ u ∧ v ∈ u)) = {∅}) → ¬ φ)
 
6-Aug-2019acexmidlemph 5398 Lemma for acexmid 5404. (Contributed by Jim Kingdon, 6-Aug-2019.)
⊢ A = {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)}    &   ⊢ B = {x ∈ {∅, {∅}} ∣ (x = {∅} ∨ φ)}    &   ⊢ 𝐶 = {A, B}    ⇒   ⊢ (φ → A = B)
 
6-Aug-2019acexmidlemb 5397 Lemma for acexmid 5404. (Contributed by Jim Kingdon, 6-Aug-2019.)
⊢ A = {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)}    &   ⊢ B = {x ∈ {∅, {∅}} ∣ (x = {∅} ∨ φ)}    &   ⊢ 𝐶 = {A, B}    ⇒   ⊢ (∅ ∈ B → φ)
 
6-Aug-2019acexmidlema 5396 Lemma for acexmid 5404. (Contributed by Jim Kingdon, 6-Aug-2019.)
⊢ A = {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)}    &   ⊢ B = {x ∈ {∅, {∅}} ∣ (x = {∅} ∨ φ)}    &   ⊢ 𝐶 = {A, B}    ⇒   ⊢ ({∅} ∈ A → φ)
 
5-Aug-2019acexmidlem2 5402 Lemma for acexmid 5404. This builds on acexmidlem1 5401 by noting that every element of 𝐶 is inhabited.

(Note that y is not quite a function in the df-fun 4798 sense because it uses ordered pairs as described in opthreg 4188 rather than df-op 3336).

The set A is also found in onsucelsucexmidlem 4171.

(Contributed by Jim Kingdon, 5-Aug-2019.)

⊢ A = {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)}    &   ⊢ B = {x ∈ {∅, {∅}} ∣ (x = {∅} ∨ φ)}    &   ⊢ 𝐶 = {A, B}    ⇒   ⊢ (∀z ∈ 𝐶 ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u) → (φ ∨ ¬ φ))
 
4-Aug-2019acexmid 5404 The axiom of choice implies excluded middle. Theorem 1.3 in [Bauer] p. 483.

The statement of the axiom of choice given here is ac2 in the Metamath Proof Explorer (version of 3-Aug-2019). In particular, note that the choice function y provides a value when z is inhabited (as opposed to non-empty as in some statements of the axiom of choice).

Essentially the same proof can also be found at "The axiom of choice implies instances of EM", [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic".

(Contributed by Jim Kingdon, 4-Aug-2019.)

⊢ ∃y∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)    ⇒   ⊢ (φ ∨ ¬ φ)
 
2-Aug-2019ordsucunielexmid 4173 The converse of sucunielr 4158 (where B is an ordinal) implies excluded middle. (Contributed by Jim Kingdon, 2-Aug-2019.)
⊢ ∀x ∈ On ∀y ∈ On (x ∈ ∪ y → suc x ∈ y)    ⇒   ⊢ (φ ∨ ¬ φ)
 
2-Aug-2019onsucelsucexmid 4172 The converse of onsucelsucr 4156 implies excluded middle. (Contributed by Jim Kingdon, 2-Aug-2019.)
⊢ ∀x ∈ On ∀y ∈ On (x ∈ y → suc x ∈ suc y)    ⇒   ⊢ (φ ∨ ¬ φ)
 
2-Aug-2019onsucelsucexmidlem 4171 Lemma for onsucelsucexmid 4172. The set {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)} appears as A in the proof of Theorem 1.3 in [Bauer] p. 483 (see acexmidlema 5396), and similar sets also appear in other proofs that various propositions imply excluded middle, for example in ordtriexmidlem 4165. (Contributed by Jim Kingdon, 2-Aug-2019.)
⊢ {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)} ∈ On
 
2-Aug-2019onsucelsucexmidlem1 4170 Lemma for onsucelsucexmid 4172. (Contributed by Jim Kingdon, 2-Aug-2019.)
⊢ ∅ ∈ {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)}
 
2-Aug-2019onuniss2 4160 The union of the ordinal subsets of an ordinal number is that number. (Contributed by Jim Kingdon, 2-Aug-2019.)
⊢ (A ∈ On → ∪ {x ∈ On ∣ x ⊆ A} = A)
 
2-Aug-2019sucunielr 4158 Successor and union. The converse (where B is an ordinal) implies excluded middle, as seen at ordsucunielexmid 4173. (Contributed by Jim Kingdon, 2-Aug-2019.)
⊢ (suc A ∈ B → A ∈ ∪ B)
 
31-Jul-2019ordtri2orexmid 4168 Ordinal trichotomy implies excluded middle. (Contributed by Jim Kingdon, 31-Jul-2019.)
⊢ ∀x ∈ On ∀y ∈ On (x ∈ y ∨ y ⊆ x)    ⇒   ⊢ (φ ∨ ¬ φ)
 
30-Jul-2019ordpwsucexmid 4199 The subset in ordpwsucss 4196 cannot be equality. That is, strengthening it to equality implies excluded middle. (Contributed by Jim Kingdon, 30-Jul-2019.)
⊢ ∀x ∈ On suc x = (𝒫 x ∩ On)    ⇒   ⊢ (φ ∨ ¬ φ)
 
29-Jul-2019onsucsssucexmid 4169 The converse of onsucsssucr 4157 implies excluded middle. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2019.)
⊢ ∀x ∈ On ∀y ∈ On (x ⊆ y → suc x ⊆ suc y)    ⇒   ⊢ (φ ∨ ¬ φ)
 
29-Jul-2019onsucsssucr 4157 The subclass relationship between two ordinals is inherited by their predecessors. The converse implies excluded middle, as shown at onsucsssucexmid 4169. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2019.)
⊢ ((A ∈ On ∧ Ord B) → (suc A ⊆ suc B → A ⊆ B))
 
27-Jul-2019oawordi 5924 Weak ordering property of ordinal addition. (Contributed by Jim Kingdon, 27-Jul-2019.)
⊢ ((A ∈ On ∧ B ∈ On ∧ 𝐶 ∈ On) → (A ⊆ B → (𝐶 +𝑜 A) ⊆ (𝐶 +𝑜 B)))
 
27-Jul-2019oafnex 5904 The characteristic function for ordinal addition is defined everywhere. (Contributed by Jim Kingdon, 27-Jul-2019.)
⊢ (x ∈ V ↦ suc x) Fn V
 
26-Jul-2019oeicl 5921 Closure law for ordinal exponentiation. (Contributed by Jim Kingdon, 26-Jul-2019.)
⊢ ((A ∈ On ∧ B ∈ On) → (A ↑𝑜 B) ∈ On)
 
26-Jul-2019rdgon 5859 Evaluating the recursive definition generator produces an ordinal. There is a hypothesis that the characteristic function produces ordinals on ordinal arguments. (Contributed by Jim Kingdon, 26-Jul-2019.)
⊢ (φ → 𝐹 Fn V)    &   ⊢ (φ → A ∈ On)    &   ⊢ (φ → ∀x ∈ On (𝐹‘x) ∈ On)    ⇒   ⊢ ((φ ∧ B ∈ On) → (rec(𝐹, A)‘B) ∈ On)
 
26-Jul-2019rdgival 5854 Value of the recursive definition generator. (Contributed by Jim Kingdon, 26-Jul-2019.)
⊢ ((𝐹 Fn V ∧ A ∈ 𝑉 ∧ B ∈ On) → (rec(𝐹, A)‘B) = (A ∪ ∪ x ∈ B (𝐹‘(rec(𝐹, A)‘x))))
 
25-Jul-2019onun2 4139 The union of two ordinal numbers is an ordinal number. (Contributed by Jim Kingdon, 25-Jul-2019.)
⊢ ((A ∈ On ∧ B ∈ On) → (A ∪ B) ∈ On)
 
25-Jul-2019prexgOLD 3898 The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51, but restricted to classes which exist. For proper classes, see prprc 3431, prprc1 3429, and prprc2 3430. This is a special case of prexg 3899 and new proofs should use prexg 3899 instead. (Contributed by Jim Kingdon, 25-Jul-2019.) (New usage is discouraged.)
⊢ ((A ∈ V ∧ B ∈ V) → {A, B} ∈ V)
 
22-Jul-2019ssnel 4198 Relationship between subset and elementhood. In the context of ordinals this can be seen as an ordering law. (Contributed by Jim Kingdon, 22-Jul-2019.)
⊢ (A ⊆ B → ¬ B ∈ A)
 
21-Jul-2019ordpwsucss 4196 The collection of ordinals in the power class of an ordinal is a superset of its successor.

We can think of (𝒫 A ∩ On) as another possible definition of successor, which would be equivalent to df-suc 4031 given excluded middle. It is an ordinal, and has some successor-like properties. For example, if A ∈ On then both ∪ suc A = A (onunisuci 4092) and ∪ {x ∈ On ∣ x ⊆ A} = A (onuniss2 4160).

Constructively (𝒫 A ∩ On) and suc A cannot be shown to be equivalent (as proved at ordpwsucexmid 4199). (Contributed by Jim Kingdon, 21-Jul-2019.)

⊢ (Ord A → suc A ⊆ (𝒫 A ∩ On))
 
17-Jul-2019onsucelsucr 4156 Membership is inherited by predecessors. The converse implies excluded middle, as shown at onsucelsucexmid 4172. (Contributed by Jim Kingdon, 17-Jul-2019.)
⊢ (B ∈ On → (suc A ∈ suc B → A ∈ B))
 
15-Jul-2019rdgss 5855 Subset and recursive definition generator. (Contributed by Jim Kingdon, 15-Jul-2019.)
⊢ (φ → 𝐹 Fn V)    &   ⊢ (φ → 𝐼 ∈ 𝑉)    &   ⊢ (φ → A ∈ On)    &   ⊢ (φ → B ∈ On)    &   ⊢ (φ → A ⊆ B)    ⇒   ⊢ (φ → (rec(𝐹, 𝐼)‘A) ⊆ (rec(𝐹, 𝐼)‘B))
 
14-Jul-2019sucinc2 5906 Successor is increasing. (Contributed by Jim Kingdon, 14-Jul-2019.)
⊢ 𝐹 = (z ∈ V ↦ suc z)    ⇒   ⊢ ((B ∈ On ∧ A ∈ B) → (𝐹‘A) ⊆ (𝐹‘B))
 
13-Jul-2019rdgivallem 5853 Value of the recursive definition generator. Lemma for rdgival 5854 which simplifies the value further. (Contributed by Jim Kingdon, 13-Jul-2019.) (New usage is discouraged.)
⊢ ((𝐹 Fn V ∧ A ∈ 𝑉 ∧ B ∈ On) → (rec(𝐹, A)‘B) = (A ∪ ∪ x ∈ B (𝐹‘((rec(𝐹, A) ↾ B)‘x))))
 
13-Jul-2019rdgifnon 5852 The recursive definition generator is a function on ordinal numbers. The 𝐹 Fn V condition states that the characteristic function is defined for all sets (being defined for all ordinals might be enough, but being defined for all sets will generally hold for the characteristic functions we need to use this with). (Contributed by Jim Kingdon, 13-Jul-2019.)
⊢ ((𝐹 Fn V ∧ A ∈ 𝑉) → rec(𝐹, A) Fn On)
 
10-Jul-2019rdgi0g 5851 The initial value of the recursive definition generator. (Contributed by Jim Kingdon, 10-Jul-2019.)
⊢ ((𝐹 Fn V ∧ A ∈ 𝑉) → (rec(𝐹, A)‘∅) = A)
 
9-Jul-2019oeiv 5915 Value of ordinal exponentiation. (Contributed by Jim Kingdon, 9-Jul-2019.)
⊢ ((A ∈ On ∧ B ∈ On) → (A ↑𝑜 B) = (rec((x ∈ V ↦ (x ·𝑜 A)), 1𝑜)‘B))
 
9-Jul-2019tfrlemi14d 5833 The domain of recs is all ordinals (lemma for transfinite recursion). (Contributed by Jim Kingdon, 9-Jul-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    ⇒   ⊢ (φ → dom recs(𝐹) = On)
 
9-Jul-2019opeldmg 4433 Membership of first of an ordered pair in a domain. (Contributed by Jim Kingdon, 9-Jul-2019.)
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → (⟨A, B⟩ ∈ 𝐶 → A ∈ dom 𝐶))
 
4-Jul-2019df-oexpi 5887 Define the ordinal exponentiation operation.

This definition is similar to a conventional definition of exponentiation except that it defines ∅ ↑𝑜 A to be 1𝑜 for all A ∈ On, in order to avoid having different cases for whether the base is ∅ or not. (Contributed by Mario Carneiro, 4-Jul-2019.)

⊢ ↑𝑜 = (x ∈ On, y ∈ On ↦ (rec((z ∈ V ↦ (z ·𝑜 x)), 1𝑜)‘y))
 
4-Jul-2019rdgexgg 5850 The recursive definition generator produces a set on a set input. (Contributed by Jim Kingdon, 4-Jul-2019.)
⊢ 𝐹 Fn V    ⇒   ⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → (rec(𝐹, A)‘B) ∈ V)
 
4-Jul-2019rdgexggg 5849 The recursive definition generator produces a set on a set input. (Contributed by Jim Kingdon, 4-Jul-2019.)
⊢ ((𝐹 Fn V ∧ A ∈ 𝑉 ∧ B ∈ 𝑊) → (rec(𝐹, A)‘B) ∈ V)
 
4-Jul-2019rdgruledefg 5848 The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 4-Jul-2019.)
⊢ 𝐹 Fn V    ⇒   ⊢ (A ∈ 𝑉 → (Fun (g ∈ V ↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x)))) ∧ ((g ∈ V ↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x))))‘f) ∈ V))
 
4-Jul-2019rdgruledefgg 5847 The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 4-Jul-2019.)
⊢ ((𝐹 Fn V ∧ A ∈ 𝑉) → (Fun (g ∈ V ↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x)))) ∧ ((g ∈ V ↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x))))‘f) ∈ V))
 
3-Jul-2019oeiexg 5912 Ordinal exponentiation is a set. (Contributed by Mario Carneiro, 3-Jul-2019.)
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → (A ↑𝑜 B) ∈ V)
 
3-Jul-2019fnoei 5911 Functionality and domain of ordinal exponentiation. (Contributed by Mario Carneiro, 29-May-2015.) (Revised by Mario Carneiro, 3-Jul-2019.)
⊢ ↑𝑜 Fn (On × On)
 
3-Jul-2019omexg 5910 Ordinal multiplication is a set. (Contributed by Mario Carneiro, 3-Jul-2019.)
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → (A ·𝑜 B) ∈ V)
 
3-Jul-2019fnom 5909 Functionality and domain of ordinal multiplication. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 3-Jul-2019.)
⊢ ·𝑜 Fn (On × On)
 
3-Jul-2019oaexg 5908 Ordinal addition is a set. (Contributed by Mario Carneiro, 3-Jul-2019.)
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → (A +𝑜 B) ∈ V)
 
3-Jul-2019fnoa 5907 Functionality and domain of ordinal addition. (Contributed by NM, 26-Aug-1995.) (Proof shortened by Mario Carneiro, 3-Jul-2019.)
⊢ +𝑜 Fn (On × On)
 
3-Jul-2019rdgexg 5862 The recursive definition generator produces a set on a set input. (Contributed by Mario Carneiro, 3-Jul-2019.)
⊢ A ∈ V    &   ⊢ 𝐹 Fn V    ⇒   ⊢ (B ∈ 𝑉 → (rec(𝐹, A)‘B) ∈ V)
 
3-Jul-2019tfrex 5841 The transfinite recursion function is set-like if the input is. (Contributed by Mario Carneiro, 3-Jul-2019.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (φ → ∀x(Fun 𝐺 ∧ (𝐺‘x) ∈ V))    ⇒   ⊢ ((φ ∧ A ∈ 𝑉) → (𝐹‘A) ∈ V)
 
3-Jul-2019tfrexlem 5835 The transfinite recursion function is set-like if the input is. (Contributed by Mario Carneiro, 3-Jul-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    ⇒   ⊢ ((φ ∧ 𝐶 ∈ 𝑉) → (recs(𝐹)‘𝐶) ∈ V)
 
3-Jul-2019mpt2fvexi 5721 Sufficient condition for an operation maps-to notation to be set-like. (Contributed by Mario Carneiro, 3-Jul-2019.)
⊢ 𝐹 = (x ∈ A, y ∈ B ↦ 𝐶)    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝑅 ∈ V    &   ⊢ 𝑆 ∈ V    ⇒   ⊢ (𝑅𝐹𝑆) ∈ V
 
3-Jul-2019mpt2fvex 5718 Sufficient condition for an operation maps-to notation to be set-like. (Contributed by Mario Carneiro, 3-Jul-2019.)
⊢ 𝐹 = (x ∈ A, y ∈ B ↦ 𝐶)    ⇒   ⊢ ((∀x∀y 𝐶 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ 𝑆 ∈ 𝑋) → (𝑅𝐹𝑆) ∈ V)
 
3-Jul-2019mptfvex 5148 Sufficient condition for a maps-to notation to be set-like. (Contributed by Mario Carneiro, 3-Jul-2019.)
⊢ 𝐹 = (x ∈ A ↦ B)    ⇒   ⊢ ((∀x B ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐹‘𝐶) ∈ V)
 
3-Jul-2019fvmptss2 5139 A mapping always evaluates to a subset of the substituted expression in the mapping, even if this is a proper class, or we are out of the domain. (Contributed by Mario Carneiro, 13-Feb-2015.) (Revised by Mario Carneiro, 3-Jul-2019.)
⊢ (x = 𝐷 → B = 𝐶)    &   ⊢ 𝐹 = (x ∈ A ↦ B)    ⇒   ⊢ (𝐹‘𝐷) ⊆ 𝐶
 
2-Jul-2019tfrlemisucfn 5824 We can extend an acceptable function by one element to produce a function. Lemma for tfrlemi1 5832. (Contributed by Jim Kingdon, 2-Jul-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    &   ⊢ (φ → z ∈ On)    &   ⊢ (φ → g Fn z)    &   ⊢ (φ → g ∈ A)    ⇒   ⊢ (φ → (g ∪ {⟨z, (𝐹‘g)⟩}) Fn suc z)
 
2-Jul-2019tfrlem3-2d 5815 Lemma for transfinite recursion which changes a bound variable (Contributed by Jim Kingdon, 2-Jul-2019.)
⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    ⇒   ⊢ (φ → (Fun 𝐹 ∧ (𝐹‘g) ∈ V))
 
26-Jun-2019ordge1n0im 5899 An ordinal greater than or equal to 1 is nonzero. (Contributed by Jim Kingdon, 26-Jun-2019.)
⊢ (Ord A → (1𝑜 ⊆ A → A ≠ ∅))
 
25-Jun-2019sucinc 5905 Successor is increasing. (Contributed by Jim Kingdon, 25-Jun-2019.)
⊢ 𝐹 = (z ∈ V ↦ suc z)    ⇒   ⊢ ∀x x ⊆ (𝐹‘x)
 
15-Jun-2019rdgisuc2 5858 The value of the recursive definition generator.

Given the hypothesis that the characteristic function is increasing, we can remove the initial value from rdgisuc1 5856 by using rdg0ss 5857. (Contributed by Jim Kingdon, 15-Jun-2019.)

⊢ (φ → 𝐹 Fn V)    &   ⊢ (φ → A ∈ 𝑉)    &   ⊢ (φ → B ∈ On)    &   ⊢ (φ → ∀x x ⊆ (𝐹‘x))    ⇒   ⊢ (φ → (rec(𝐹, A)‘suc B) = (∪ x ∈ B (𝐹‘(rec(𝐹, A)‘x)) ∪ (𝐹‘(rec(𝐹, A)‘B))))
 
11-Jun-2019rdg0ss 5857 The initial value is a subset of the recursive definition generator evaluated at any ordinal. This is a consequence of the way that df-irdg 5843 handles the initial value. (Contributed by Jim Kingdon, 11-Jun-2019.)
⊢ (φ → 𝐹 Fn V)    &   ⊢ (φ → A ∈ 𝑉)    &   ⊢ (φ → B ∈ On)    ⇒   ⊢ (φ → A ⊆ (rec(𝐹, A)‘B))
 
9-Jun-2019rdgisuc1 5856 One way of describing the value of the recursive definition generator at a successor. There is no condition on the characteristic function 𝐹 other than 𝐹 Fn V. Given that, the resulting expression encompasses both the expected successor term (𝐹‘(rec(𝐹, A)‘B)) but also terms that correspond to the initial value A and to limit ordinals ∪ x ∈ B(𝐹‘(rec(𝐹, A)‘x)).

If we add conditions on the characteristic function, we can show tighter results such as rdgisuc2 5858. The eventual goal is (rec(𝐹, A)‘suc B) = (𝐹‘(rec(𝐹, A)‘B)). (Contributed by Jim Kingdon, 9-Jun-2019.)

⊢ (φ → 𝐹 Fn V)    &   ⊢ (φ → A ∈ 𝑉)    &   ⊢ (φ → B ∈ On)    ⇒   ⊢ (φ → (rec(𝐹, A)‘suc B) = (A ∪ (∪ x ∈ B (𝐹‘(rec(𝐹, A)‘x)) ∪ (𝐹‘(rec(𝐹, A)‘B)))))
 
29-May-2019rdgruledef 5860 The recursion rule for the recursive definition generator is defined everywhere. Lemma for rdg0 5861. (Contributed by Jim Kingdon, 29-May-2019.)
⊢ A ∈ V    &   ⊢ 𝐹 Fn V    ⇒   ⊢ (Fun (g ∈ V ↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x)))) ∧ ((g ∈ V ↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x))))‘f) ∈ V)
 
28-May-2019fvex 5087 Evaluating a set function at a set exists. (Contributed by Mario Carneiro and Jim Kingdon, 28-May-2019.)
⊢ 𝐹 ∈ 𝑉    &   ⊢ A ∈ 𝑊    ⇒   ⊢ (𝐹‘A) ∈ V
 
28-May-2019fvexg 5086 Evaluating a set function at a set exists. (Contributed by Mario Carneiro and Jim Kingdon, 28-May-2019.)
⊢ ((𝐹 ∈ 𝑉 ∧ A ∈ 𝑊) → (𝐹‘A) ∈ V)
 
24-May-2019tfri1 5838 Principle of Transfinite Recursion, part 1 of 3. Theorem 7.41(1) of [TakeutiZaring] p. 47, with an additional condition.

The condition is that 𝐺 is defined "everywhere" and here is stated as (𝐺‘x) ∈ V. Alternatively ∀x ∈ On∀f(f Fn x → f ∈ dom 𝐺) would suffice.

Given a function 𝐺 satisfying that condition, we define a class A of all "acceptable" functions. The final function we're interested in is the union 𝐹 = recs(𝐺) of them. 𝐹 is then said to be defined by transfinite recursion. The purpose of the 3 parts of this theorem is to demonstrate properties of 𝐹. In this first part we show that 𝐹 is a function whose domain is all ordinal numbers. (Contributed by Jim Kingdon, 4-May-2019.) (Revised by Mario Carneiro, 24-May-2019.)

⊢ 𝐹 = recs(𝐺)    &   ⊢ (Fun 𝐺 ∧ (𝐺‘x) ∈ V)    ⇒   ⊢ 𝐹 Fn On
 
24-May-2019tfri1d 5836 Principle of Transfinite Recursion, part 1 of 3. Theorem 7.41(1) of [TakeutiZaring] p. 47, with an additional condition.

The condition is that 𝐺 is defined "everywhere" and here is stated as (𝐺‘x) ∈ V. Alternatively ∀x ∈ On∀f(f Fn x → f ∈ dom 𝐺) would suffice.

Given a function 𝐺 satisfying that condition, we define a class A of all "acceptable" functions. The final function we're interested in is the union 𝐹 = recs(𝐺) of them. 𝐹 is then said to be defined by transfinite recursion. The purpose of the 3 parts of this theorem is to demonstrate properties of 𝐹. In this first part we show that 𝐹 is a function whose domain is all ordinal numbers. (Contributed by Jim Kingdon, 4-May-2019.) (Revised by Mario Carneiro, 24-May-2019.)

⊢ 𝐹 = recs(𝐺)    &   ⊢ (φ → ∀x(Fun 𝐺 ∧ (𝐺‘x) ∈ V))    ⇒   ⊢ (φ → 𝐹 Fn On)
 
24-May-2019tfrlemi14 5834 The domain of recs is all ordinals (lemma for transfinite recursion). (Contributed by Jim Kingdon, 4-May-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (Fun 𝐹 ∧ (𝐹‘x) ∈ V)    ⇒   ⊢ dom recs(𝐹) = On
 
24-May-2019tfrlemi1 5832 We can define an acceptable function on any ordinal.

As with many of the transfinite recursion theorems, we have a hypothesis that states that 𝐹 is a function and that it is defined for all ordinals. (Contributed by Jim Kingdon, 4-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)

⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    ⇒   ⊢ ((φ ∧ 𝐶 ∈ On) → ∃g(g Fn 𝐶 ∧ ∀u ∈ 𝐶 (g‘u) = (𝐹‘(g ↾ u))))
 
24-May-2019tfrlemiex 5831 Lemma for tfrlemi1 5832. (Contributed by Jim Kingdon, 18-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    &   ⊢ B = {ℎ ∣ ∃z ∈ x ∃g(g Fn z ∧ g ∈ A ∧ ℎ = (g ∪ {⟨z, (𝐹‘g)⟩}))}    &   ⊢ (φ → x ∈ On)    &   ⊢ (φ → ∀z ∈ x ∃g(g Fn z ∧ ∀w ∈ z (g‘w) = (𝐹‘(g ↾ w))))    ⇒   ⊢ (φ → ∃f(f Fn x ∧ ∀u ∈ x (f‘u) = (𝐹‘(f ↾ u))))
 
24-May-2019tfrlemiubacc 5830 The union of B satisfies the recursion rule (lemma for tfrlemi1 5832). (Contributed by Jim Kingdon, 22-Apr-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    &   ⊢ B = {ℎ ∣ ∃z ∈ x ∃g(g Fn z ∧ g ∈ A ∧ ℎ = (g ∪ {⟨z, (𝐹‘g)⟩}))}    &   ⊢ (φ → x ∈ On)    &   ⊢ (φ → ∀z ∈ x ∃g(g Fn z ∧ ∀w ∈ z (g‘w) = (𝐹‘(g ↾ w))))    ⇒   ⊢ (φ → ∀u ∈ x (∪ B‘u) = (𝐹‘(∪ B ↾ u)))
 
24-May-2019tfrlemibex 5829 The set B exists. Lemma for tfrlemi1 5832. (Contributed by Jim Kingdon, 17-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    &   ⊢ B = {ℎ ∣ ∃z ∈ x ∃g(g Fn z ∧ g ∈ A ∧ ℎ = (g ∪ {⟨z, (𝐹‘g)⟩}))}    &   ⊢ (φ → x ∈ On)    &   ⊢ (φ → ∀z ∈ x ∃g(g Fn z ∧ ∀w ∈ z (g‘w) = (𝐹‘(g ↾ w))))    ⇒   ⊢ (φ → B ∈ V)
 
24-May-2019tfrlemibfn 5828 The union of B is a function defined on x. Lemma for tfrlemi1 5832. (Contributed by Jim Kingdon, 18-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    &   ⊢ B = {ℎ ∣ ∃z ∈ x ∃g(g Fn z ∧ g ∈ A ∧ ℎ = (g ∪ {⟨z, (𝐹‘g)⟩}))}    &   ⊢ (φ → x ∈ On)    &   ⊢ (φ → ∀z ∈ x ∃g(g Fn z ∧ ∀w ∈ z (g‘w) = (𝐹‘(g ↾ w))))    ⇒   ⊢ (φ → ∪ B Fn x)
 
24-May-2019tfrlemibxssdm 5827 The union of B is defined on all ordinals. Lemma for tfrlemi1 5832. (Contributed by Jim Kingdon, 18-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    &   ⊢ B = {ℎ ∣ ∃z ∈ x ∃g(g Fn z ∧ g ∈ A ∧ ℎ = (g ∪ {⟨z, (𝐹‘g)⟩}))}    &   ⊢ (φ → x ∈ On)    &   ⊢ (φ → ∀z ∈ x ∃g(g Fn z ∧ ∀w ∈ z (g‘w) = (𝐹‘(g ↾ w))))    ⇒   ⊢ (φ → x ⊆ dom ∪ B)
 
24-May-2019tfrlemibacc 5826 Each element of B is an acceptable function. Lemma for tfrlemi1 5832. (Contributed by Jim Kingdon, 14-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    &   ⊢ B = {ℎ ∣ ∃z ∈ x ∃g(g Fn z ∧ g ∈ A ∧ ℎ = (g ∪ {⟨z, (𝐹‘g)⟩}))}    &   ⊢ (φ → x ∈ On)    &   ⊢ (φ → ∀z ∈ x ∃g(g Fn z ∧ ∀w ∈ z (g‘w) = (𝐹‘(g ↾ w))))    ⇒   ⊢ (φ → B ⊆ A)
 
24-May-2019tfrlemisucaccv 5825 We can extend an acceptable function by one element to produce an acceptable function. Lemma for tfrlemi1 5832. (Contributed by Jim Kingdon, 4-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    &   ⊢ (φ → z ∈ On)    &   ⊢ (φ → g Fn z)    &   ⊢ (φ → g ∈ A)    ⇒   ⊢ (φ → (g ∪ {⟨z, (𝐹‘g)⟩}) ∈ A)
 
24-May-2019tfrlem7 5820 Lemma for transfinite recursion. The union of all acceptable functions is a function. (Contributed by NM, 9-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    ⇒   ⊢ Fun recs(𝐹)
 
24-May-2019tfrlem5 5817 Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    ⇒   ⊢ ((g ∈ A ∧ ℎ ∈ A) → ((xgu ∧ xℎv) → u = v))
 
24-May-2019tfrlem1 5810 A technical lemma for transfinite recursion. Compare Lemma 1 of [TakeutiZaring] p. 47. (Contributed by NM, 23-Mar-1995.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ (φ → A ∈ On)    &   ⊢ (φ → (Fun 𝐹 ∧ A ⊆ dom 𝐹))    &   ⊢ (φ → (Fun 𝐺 ∧ A ⊆ dom 𝐺))    &   ⊢ (φ → ∀x ∈ A (𝐹‘x) = (B‘(𝐹 ↾ x)))    &   ⊢ (φ → ∀x ∈ A (𝐺‘x) = (B‘(𝐺 ↾ x)))    ⇒   ⊢ (φ → ∀x ∈ A (𝐹‘x) = (𝐺‘x))
 
24-May-2019sefvex 5088 If a function is set-like, then the function value exists if the input does. (Contributed by Mario Carneiro, 24-May-2019.)
⊢ ((◡𝐹 Se V ∧ A ∈ V) → (𝐹‘A) ∈ V)
 
24-May-2019relrnfvex 5085 If a function has a set range, then the function value exists unconditional on the domain. (Contributed by Mario Carneiro, 24-May-2019.)
⊢ ((Rel 𝐹 ∧ ran 𝐹 ∈ V) → (𝐹‘A) ∈ V)
 
24-May-2019relfvssunirn 5083 The result of a function value is always a subset of the union of the range, even if it is invalid and thus empty. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ (Rel 𝐹 → (𝐹‘A) ⊆ ∪ ran 𝐹)
 
24-May-2019fvssunirng 5082 The result of a function value is always a subset of the union of the range, if the input is a set. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ (A ∈ V → (𝐹‘A) ⊆ ∪ ran 𝐹)
 
24-May-2019fvss 5081 The value of a function is a subset of B if every element that could be a candidate for the value is a subset of B. (Contributed by Mario Carneiro, 24-May-2019.)
⊢ (∀x(A𝐹x → x ⊆ B) → (𝐹‘A) ⊆ B)
 
24-May-2019opex 3918 An ordered pair of sets is a set. (Contributed by Jim Kingdon, 24-Sep-2018.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ⟨A, B⟩ ∈ V
 
24-May-2019snex 3889 A singleton whose element exists is a set. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ A ∈ V    ⇒   ⊢ {A} ∈ V
 
19-May-2019df-irdg 5843 Define a recursive definition generator on On (the class of ordinal numbers) with characteristic function 𝐹 and initial value 𝐼. 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 daunting complexity of our rec operation (especially when df-recs 5807 that it is built on is also eliminated). But once we get past this hurdle, definitions that would otherwise be recursive become relatively simple. In classical logic it would be easier to divide this definition into cases based on whether the domain of g is zero, a successor, or a limit ordinal. Cases do not (in general) work that way in intuitionistic logic, so instead we choose a definition which takes the union of all the results of the characteristic function for ordinals in the domain of g. This means that this definition has the expected properties for increasing and continuous ordinal functions, which include ordinal addition and multiplication.

Note: We introduce rec with the philosophical goal of being able to eliminate all definitions with direct mechanical substitution and to verify easily the soundness of definitions. Metamath itself has no built-in technical limitation that prevents multiple-part recursive definitions in the traditional textbook style. (Contributed by Jim Kingdon, 19-May-2019.)

⊢ rec(𝐹, 𝐼) = recs((g ∈ V ↦ (𝐼 ∪ ∪ x ∈ dom g(𝐹‘(g‘x)))))
 
4-May-2019tfri3 5840 Principle of Transfinite Recursion, part 3 of 3. Theorem 7.41(3) of [TakeutiZaring] p. 47, with an additional condition on the recursion rule 𝐺 ( as described at tfri1 5838). Finally, we show that 𝐹 is unique. We do this by showing that any class B with the same properties of 𝐹 that we showed in parts 1 and 2 is identical to 𝐹. (Contributed by Jim Kingdon, 4-May-2019.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (Fun 𝐺 ∧ (𝐺‘x) ∈ V)    ⇒   ⊢ ((B Fn On ∧ ∀x ∈ On (B‘x) = (𝐺‘(B ↾ x))) → B = 𝐹)
 
4-May-2019tfri2 5839 Principle of Transfinite Recursion, part 2 of 3. Theorem 7.41(2) of [TakeutiZaring] p. 47, with an additional condition on the recursion rule 𝐺 ( as described at tfri1 5838). Here we show that the function 𝐹 has the property that for any function 𝐺 satisfying that condition, the "next" value of 𝐹 is 𝐺 recursively applied to all "previous" values of 𝐹. (Contributed by Jim Kingdon, 4-May-2019.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (Fun 𝐺 ∧ (𝐺‘x) ∈ V)    ⇒   ⊢ (A ∈ On → (𝐹‘A) = (𝐺‘(𝐹 ↾ A)))
  Copyright terms: Public domain W3C HTML validation [external]