Intuitionistic Logic Explorer Most Recent Proofs |
||
Mirrors > Home > ILE Home > Th. List > Recent | MPE Most Recent Other > MM 100 |
See the MPE Most Recent Proofs page for news and some useful links.
Color key: | Intuitionistic Logic Explorer | User Mathboxes |
Date | Label | Description |
---|---|---|
Theorem | ||
16-Aug-2019 | frecabex 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-2019 | frecsuc 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-2019 | frecsuclem3 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-2019 | frecsuclem2 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-2019 | frecsuclemdm 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-2019 | frectfr 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-2019 | frecsuclem1 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-2019 | oav2 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-2019 | frec0g 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-2019 | frecfnom 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-2019 | df-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-2019 | acexmidlem1 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-2019 | acexmidlemcase 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-2019 | acexmidlemv 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-2019 | acexmidlemab 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-2019 | acexmidlemph 5398 | Lemma for acexmid 5404. (Contributed by Jim Kingdon, 6-Aug-2019.) |
⊢ A = {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)} & ⊢ B = {x ∈ {∅, {∅}} ∣ (x = {∅} ∨ φ)} & ⊢ 𝐶 = {A, B} ⇒ ⊢ (φ → A = B) | ||
6-Aug-2019 | acexmidlemb 5397 | Lemma for acexmid 5404. (Contributed by Jim Kingdon, 6-Aug-2019.) |
⊢ A = {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)} & ⊢ B = {x ∈ {∅, {∅}} ∣ (x = {∅} ∨ φ)} & ⊢ 𝐶 = {A, B} ⇒ ⊢ (∅ ∈ B → φ) | ||
6-Aug-2019 | acexmidlema 5396 | Lemma for acexmid 5404. (Contributed by Jim Kingdon, 6-Aug-2019.) |
⊢ A = {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)} & ⊢ B = {x ∈ {∅, {∅}} ∣ (x = {∅} ∨ φ)} & ⊢ 𝐶 = {A, B} ⇒ ⊢ ({∅} ∈ A → φ) | ||
5-Aug-2019 | acexmidlem2 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-2019 | acexmid 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-2019 | ordsucunielexmid 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-2019 | onsucelsucexmid 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-2019 | onsucelsucexmidlem 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-2019 | onsucelsucexmidlem1 4170 | Lemma for onsucelsucexmid 4172. (Contributed by Jim Kingdon, 2-Aug-2019.) |
⊢ ∅ ∈ {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)} | ||
2-Aug-2019 | onuniss2 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-2019 | sucunielr 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-2019 | ordtri2orexmid 4168 | Ordinal trichotomy implies excluded middle. (Contributed by Jim Kingdon, 31-Jul-2019.) |
⊢ ∀x ∈ On ∀y ∈ On (x ∈ y ∨ y ⊆ x) ⇒ ⊢ (φ ∨ ¬ φ) | ||
30-Jul-2019 | ordpwsucexmid 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-2019 | onsucsssucexmid 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-2019 | onsucsssucr 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-2019 | oawordi 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-2019 | oafnex 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-2019 | oeicl 5921 | Closure law for ordinal exponentiation. (Contributed by Jim Kingdon, 26-Jul-2019.) |
⊢ ((A ∈ On ∧ B ∈ On) → (A ↑_{𝑜} B) ∈ On) | ||
26-Jul-2019 | rdgon 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-2019 | rdgival 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-2019 | onun2 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-2019 | prexgOLD 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-2019 | ssnel 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-2019 | ordpwsucss 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-2019 | onsucelsucr 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-2019 | rdgss 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-2019 | sucinc2 5906 | Successor is increasing. (Contributed by Jim Kingdon, 14-Jul-2019.) |
⊢ 𝐹 = (z ∈ V ↦ suc z) ⇒ ⊢ ((B ∈ On ∧ A ∈ B) → (𝐹‘A) ⊆ (𝐹‘B)) | ||
13-Jul-2019 | rdgivallem 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-2019 | rdgifnon 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-2019 | rdgi0g 5851 | The initial value of the recursive definition generator. (Contributed by Jim Kingdon, 10-Jul-2019.) |
⊢ ((𝐹 Fn V ∧ A ∈ 𝑉) → (rec(𝐹, A)‘∅) = A) | ||
9-Jul-2019 | oeiv 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-2019 | tfrlemi14d 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-2019 | opeldmg 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-2019 | df-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-2019 | rdgexgg 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-2019 | rdgexggg 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-2019 | rdgruledefg 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-2019 | rdgruledefgg 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-2019 | oeiexg 5912 | Ordinal exponentiation is a set. (Contributed by Mario Carneiro, 3-Jul-2019.) |
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → (A ↑_{𝑜} B) ∈ V) | ||
3-Jul-2019 | fnoei 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-2019 | omexg 5910 | Ordinal multiplication is a set. (Contributed by Mario Carneiro, 3-Jul-2019.) |
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → (A ·_{𝑜} B) ∈ V) | ||
3-Jul-2019 | fnom 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-2019 | oaexg 5908 | Ordinal addition is a set. (Contributed by Mario Carneiro, 3-Jul-2019.) |
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → (A +_{𝑜} B) ∈ V) | ||
3-Jul-2019 | fnoa 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-2019 | rdgexg 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-2019 | tfrex 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-2019 | tfrexlem 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-2019 | mpt2fvexi 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-2019 | mpt2fvex 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-2019 | mptfvex 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-2019 | fvmptss2 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-2019 | tfrlemisucfn 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-2019 | tfrlem3-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-2019 | ordge1n0im 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-2019 | sucinc 5905 | Successor is increasing. (Contributed by Jim Kingdon, 25-Jun-2019.) |
⊢ 𝐹 = (z ∈ V ↦ suc z) ⇒ ⊢ ∀x x ⊆ (𝐹‘x) | ||
15-Jun-2019 | rdgisuc2 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-2019 | rdg0ss 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-2019 | rdgisuc1 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-2019 | rdgruledef 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-2019 | fvex 5087 | Evaluating a set function at a set exists. (Contributed by Mario Carneiro and Jim Kingdon, 28-May-2019.) |
⊢ 𝐹 ∈ 𝑉 & ⊢ A ∈ 𝑊 ⇒ ⊢ (𝐹‘A) ∈ V | ||
28-May-2019 | fvexg 5086 | Evaluating a set function at a set exists. (Contributed by Mario Carneiro and Jim Kingdon, 28-May-2019.) |
⊢ ((𝐹 ∈ 𝑉 ∧ A ∈ 𝑊) → (𝐹‘A) ∈ V) | ||
24-May-2019 | tfri1 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-2019 | tfri1d 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-2019 | tfrlemi14 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-2019 | tfrlemi1 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-2019 | tfrlemiex 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-2019 | tfrlemiubacc 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-2019 | tfrlemibex 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-2019 | tfrlemibfn 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-2019 | tfrlemibxssdm 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-2019 | tfrlemibacc 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-2019 | tfrlemisucaccv 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-2019 | tfrlem7 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-2019 | tfrlem5 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-2019 | tfrlem1 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-2019 | sefvex 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-2019 | relrnfvex 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-2019 | relfvssunirn 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-2019 | fvssunirng 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-2019 | fvss 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-2019 | opex 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-2019 | snex 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-2019 | df-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-2019 | tfri3 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-2019 | tfri2 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] |