Home | Intuitionistic Logic Explorer Theorem List (p. 64 of 137) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | tfrcllemsucaccv 6301* | Lemma for tfrcl 6311. We can extend an acceptable function by one element to produce an acceptable function. (Contributed by Jim Kingdon, 24-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆) & ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝑧 ∈ 𝑌) & ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) & ⊢ (𝜑 → 𝑔:𝑧⟶𝑆) & ⊢ (𝜑 → 𝑔 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ∈ 𝐴) | ||
Theorem | tfrcllembacc 6302* | Lemma for tfrcl 6311. Each element of 𝐵 is an acceptable function. (Contributed by Jim Kingdon, 25-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆) & ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} & ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}))} & ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) ⇒ ⊢ (𝜑 → 𝐵 ⊆ 𝐴) | ||
Theorem | tfrcllembxssdm 6303* | Lemma for tfrcl 6311. The union of 𝐵 is defined on all elements of 𝑋. (Contributed by Jim Kingdon, 25-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆) & ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} & ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}))} & ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) ⇒ ⊢ (𝜑 → 𝐷 ⊆ dom ∪ 𝐵) | ||
Theorem | tfrcllembfn 6304* | Lemma for tfrcl 6311. The union of 𝐵 is a function defined on 𝑥. (Contributed by Jim Kingdon, 25-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆) & ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} & ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}))} & ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) ⇒ ⊢ (𝜑 → ∪ 𝐵:𝐷⟶𝑆) | ||
Theorem | tfrcllembex 6305* | Lemma for tfrcl 6311. The set 𝐵 exists. (Contributed by Jim Kingdon, 25-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆) & ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} & ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}))} & ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) ⇒ ⊢ (𝜑 → 𝐵 ∈ V) | ||
Theorem | tfrcllemubacc 6306* | Lemma for tfrcl 6311. The union of 𝐵 satisfies the recursion rule. (Contributed by Jim Kingdon, 25-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆) & ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} & ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}))} & ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) ⇒ ⊢ (𝜑 → ∀𝑢 ∈ 𝐷 (∪ 𝐵‘𝑢) = (𝐺‘(∪ 𝐵 ↾ 𝑢))) | ||
Theorem | tfrcllemex 6307* | Lemma for tfrcl 6311. (Contributed by Jim Kingdon, 26-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆) & ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} & ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}))} & ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔:𝑧⟶𝑆 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝐷⟶𝑆 ∧ ∀𝑢 ∈ 𝐷 (𝑓‘𝑢) = (𝐺‘(𝑓 ↾ 𝑢)))) | ||
Theorem | tfrcllemaccex 6308* |
We can define an acceptable function on any element of 𝑋.
As with many of the transfinite recursion theorems, we have hypotheses that state that 𝐹 is a function and that it is defined up to 𝑋. (Contributed by Jim Kingdon, 26-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆) & ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} & ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → ∃𝑔(𝑔:𝐶⟶𝑆 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) | ||
Theorem | tfrcllemres 6309* | Lemma for tfr1on 6297. Recursion is defined on an ordinal if the characteristic function is defined up to a suitable point. (Contributed by Jim Kingdon, 18-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆) & ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓:𝑥⟶𝑆 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} & ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝑌 ⊆ dom 𝐹) | ||
Theorem | tfrcldm 6310* | Recursion is defined on an ordinal if the characteristic function satisfies a closure hypothesis up to a suitable point. (Contributed by Jim Kingdon, 26-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) & ⊢ (𝜑 → 𝑌 ∈ ∪ 𝑋) ⇒ ⊢ (𝜑 → 𝑌 ∈ dom 𝐹) | ||
Theorem | tfrcl 6311* | Closure for transfinite recursion. As with tfr1on 6297, the characteristic function must be defined up to a suitable point, not necessarily on all ordinals. (Contributed by Jim Kingdon, 25-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓:𝑥⟶𝑆) → (𝐺‘𝑓) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) & ⊢ (𝜑 → 𝑌 ∈ ∪ 𝑋) ⇒ ⊢ (𝜑 → (𝐹‘𝑌) ∈ 𝑆) | ||
Theorem | tfri1 6312* |
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", which is stated here as (𝐺‘𝑥) ∈ V. Alternately, ∀𝑥 ∈ On∀𝑓(𝑓 Fn 𝑥 → 𝑓 ∈ dom 𝐺) would suffice. Given a function 𝐺 satisfying that condition, we define a class 𝐴 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 𝐺 ∧ (𝐺‘𝑥) ∈ V) ⇒ ⊢ 𝐹 Fn On | ||
Theorem | tfri2 6313* | 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 6312). 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 𝐺 ∧ (𝐺‘𝑥) ∈ V) ⇒ ⊢ (𝐴 ∈ On → (𝐹‘𝐴) = (𝐺‘(𝐹 ↾ 𝐴))) | ||
Theorem | tfri3 6314* | 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 6312). Finally, we show that 𝐹 is unique. We do this by showing that any class 𝐵 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 𝐺 ∧ (𝐺‘𝑥) ∈ V) ⇒ ⊢ ((𝐵 Fn On ∧ ∀𝑥 ∈ On (𝐵‘𝑥) = (𝐺‘(𝐵 ↾ 𝑥))) → 𝐵 = 𝐹) | ||
Theorem | tfrex 6315* | The transfinite recursion function is set-like if the input is. (Contributed by Mario Carneiro, 3-Jul-2019.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → ∀𝑥(Fun 𝐺 ∧ (𝐺‘𝑥) ∈ V)) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (𝐹‘𝐴) ∈ V) | ||
Syntax | crdg 6316 | Extend class notation with the recursive definition generator, with characteristic function 𝐹 and initial value 𝐼. |
class rec(𝐹, 𝐼) | ||
Definition | df-irdg 6317* |
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 6252
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 𝑔 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 𝑔. This means that this definition has
the expected
properties for increasing and continuous ordinal functions, which
include ordinal addition and multiplication.
For finite recursion we also define df-frec 6338 and for suitable characteristic functions df-frec 6338 yields the same result as rec restricted to ω, as seen at frecrdg 6355. 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((𝑔 ∈ V ↦ (𝐼 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))) | ||
Theorem | rdgeq1 6318 | Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.) |
⊢ (𝐹 = 𝐺 → rec(𝐹, 𝐴) = rec(𝐺, 𝐴)) | ||
Theorem | rdgeq2 6319 | Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.) |
⊢ (𝐴 = 𝐵 → rec(𝐹, 𝐴) = rec(𝐹, 𝐵)) | ||
Theorem | rdgfun 6320 | The recursive definition generator is a function. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ Fun rec(𝐹, 𝐴) | ||
Theorem | rdgtfr 6321* | The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 14-May-2020.) |
⊢ ((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) → (Fun (𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)))) ∧ ((𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘𝑓) ∈ V)) | ||
Theorem | rdgruledefgg 6322* | The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 4-Jul-2019.) |
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉) → (Fun (𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)))) ∧ ((𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘𝑓) ∈ V)) | ||
Theorem | rdgruledefg 6323* | The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 4-Jul-2019.) |
⊢ 𝐹 Fn V ⇒ ⊢ (𝐴 ∈ 𝑉 → (Fun (𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥)))) ∧ ((𝑔 ∈ V ↦ (𝐴 ∪ ∪ 𝑥 ∈ dom 𝑔(𝐹‘(𝑔‘𝑥))))‘𝑓) ∈ V)) | ||
Theorem | rdgexggg 6324 | The recursive definition generator produces a set on a set input. (Contributed by Jim Kingdon, 4-Jul-2019.) |
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (rec(𝐹, 𝐴)‘𝐵) ∈ V) | ||
Theorem | rdgexgg 6325 | The recursive definition generator produces a set on a set input. (Contributed by Jim Kingdon, 4-Jul-2019.) |
⊢ 𝐹 Fn V ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (rec(𝐹, 𝐴)‘𝐵) ∈ V) | ||
Theorem | rdgifnon 6326 | 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 if being used in a manner similar to rdgon 6333; in cases like df-oadd 6367 either presumably could work). (Contributed by Jim Kingdon, 13-Jul-2019.) |
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉) → rec(𝐹, 𝐴) Fn On) | ||
Theorem | rdgifnon2 6327* | The recursive definition generator is a function on ordinal numbers. (Contributed by Jim Kingdon, 14-May-2020.) |
⊢ ((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) → rec(𝐹, 𝐴) Fn On) | ||
Theorem | rdgivallem 6328* | Value of the recursive definition generator. Lemma for rdgival 6329 which simplifies the value further. (Contributed by Jim Kingdon, 13-Jul-2019.) (New usage is discouraged.) |
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) → (rec(𝐹, 𝐴)‘𝐵) = (𝐴 ∪ ∪ 𝑥 ∈ 𝐵 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝐵)‘𝑥)))) | ||
Theorem | rdgival 6329* | Value of the recursive definition generator. (Contributed by Jim Kingdon, 26-Jul-2019.) |
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) → (rec(𝐹, 𝐴)‘𝐵) = (𝐴 ∪ ∪ 𝑥 ∈ 𝐵 (𝐹‘(rec(𝐹, 𝐴)‘𝑥)))) | ||
Theorem | rdgss 6330 | Subset and recursive definition generator. (Contributed by Jim Kingdon, 15-Jul-2019.) |
⊢ (𝜑 → 𝐹 Fn V) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (rec(𝐹, 𝐼)‘𝐴) ⊆ (rec(𝐹, 𝐼)‘𝐵)) | ||
Theorem | rdgisuc1 6331* |
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(𝐹, 𝐴)‘𝐵)) but also terms that correspond to
the initial value 𝐴 and to limit ordinals
∪ 𝑥 ∈ 𝐵(𝐹‘(rec(𝐹, 𝐴)‘𝑥)).
If we add conditions on the characteristic function, we can show tighter results such as rdgisucinc 6332. (Contributed by Jim Kingdon, 9-Jun-2019.) |
⊢ (𝜑 → 𝐹 Fn V) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ On) ⇒ ⊢ (𝜑 → (rec(𝐹, 𝐴)‘suc 𝐵) = (𝐴 ∪ (∪ 𝑥 ∈ 𝐵 (𝐹‘(rec(𝐹, 𝐴)‘𝑥)) ∪ (𝐹‘(rec(𝐹, 𝐴)‘𝐵))))) | ||
Theorem | rdgisucinc 6332* |
Value of the recursive definition generator at a successor.
This can be thought of as a generalization of oasuc 6411 and omsuc 6419. (Contributed by Jim Kingdon, 29-Aug-2019.) |
⊢ (𝜑 → 𝐹 Fn V) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → ∀𝑥 𝑥 ⊆ (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → (rec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(rec(𝐹, 𝐴)‘𝐵))) | ||
Theorem | rdgon 6333* | 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.) (Revised by Jim Kingdon, 13-Apr-2022.) |
⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → ∀𝑥 ∈ On (𝐹‘𝑥) ∈ On) ⇒ ⊢ ((𝜑 ∧ 𝐵 ∈ On) → (rec(𝐹, 𝐴)‘𝐵) ∈ On) | ||
Theorem | rdg0 6334 | The initial value of the recursive definition generator. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (rec(𝐹, 𝐴)‘∅) = 𝐴 | ||
Theorem | rdg0g 6335 | The initial value of the recursive definition generator. (Contributed by NM, 25-Apr-1995.) |
⊢ (𝐴 ∈ 𝐶 → (rec(𝐹, 𝐴)‘∅) = 𝐴) | ||
Theorem | rdgexg 6336 | The recursive definition generator produces a set on a set input. (Contributed by Mario Carneiro, 3-Jul-2019.) |
⊢ 𝐴 ∈ V & ⊢ 𝐹 Fn V ⇒ ⊢ (𝐵 ∈ 𝑉 → (rec(𝐹, 𝐴)‘𝐵) ∈ V) | ||
Syntax | cfrec 6337 | Extend class notation with the finite recursive definition generator, with characteristic function 𝐹 and initial value 𝐼. |
class frec(𝐹, 𝐼) | ||
Definition | df-frec 6338* |
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 6252
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 6344 and frecsuc 6354.
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 4563. 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. For the characteristic functions which satisfy the conditions given at frecrdg 6355, this definition and df-irdg 6317 restricted to ω produce the same result. 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((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐼))})) ↾ ω) | ||
Theorem | freceq1 6339 | Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) |
⊢ (𝐹 = 𝐺 → frec(𝐹, 𝐴) = frec(𝐺, 𝐴)) | ||
Theorem | freceq2 6340 | Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) |
⊢ (𝐴 = 𝐵 → frec(𝐹, 𝐴) = frec(𝐹, 𝐵)) | ||
Theorem | frecex 6341 | Finite recursion produces a set. (Contributed by Jim Kingdon, 20-Aug-2021.) |
⊢ frec(𝐹, 𝐴) ∈ V | ||
Theorem | frecfun 6342 | Finite recursion produces a function. See also frecfnom 6348 which also states that the domain of that function is ω but which puts conditions on 𝐴 and 𝐹. (Contributed by Jim Kingdon, 13-Feb-2022.) |
⊢ Fun frec(𝐹, 𝐴) | ||
Theorem | nffrec 6343 | Bound-variable hypothesis builder for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥frec(𝐹, 𝐴) | ||
Theorem | frec0g 6344 | The initial value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 7-May-2020.) |
⊢ (𝐴 ∈ 𝑉 → (frec(𝐹, 𝐴)‘∅) = 𝐴) | ||
Theorem | frecabex 6345* | The class abstraction from df-frec 6338 exists. This is a lemma for other finite recursion proofs. (Contributed by Jim Kingdon, 13-May-2020.) |
⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → ∀𝑦(𝐹‘𝑦) ∈ V) & ⊢ (𝜑 → 𝐴 ∈ 𝑊) ⇒ ⊢ (𝜑 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑆 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑆‘𝑚))) ∨ (dom 𝑆 = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ V) | ||
Theorem | frecabcl 6346* | The class abstraction from df-frec 6338 exists. Unlike frecabex 6345 the function 𝐹 only needs to be defined on 𝑆, not all sets. This is a lemma for other finite recursion proofs. (Contributed by Jim Kingdon, 21-Mar-2022.) |
⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → 𝐺:𝑁⟶𝑆) & ⊢ (𝜑 → ∀𝑦 ∈ 𝑆 (𝐹‘𝑦) ∈ 𝑆) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) ⇒ ⊢ (𝜑 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ 𝑆) | ||
Theorem | frectfr 6347* |
Lemma to connect transfinite recursion theorems with finite recursion.
That is, given the conditions 𝐹 Fn V and 𝐴 ∈ 𝑉 on
frec(𝐹, 𝐴), we want to be able to apply tfri1d 6282 or tfri2d 6283,
and this lemma lets us satisfy hypotheses of those theorems.
(Contributed by Jim Kingdon, 15-Aug-2019.) |
⊢ 𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))}) ⇒ ⊢ ((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) → ∀𝑦(Fun 𝐺 ∧ (𝐺‘𝑦) ∈ V)) | ||
Theorem | frecfnom 6348* | The function generated by finite recursive definition generation is a function on omega. (Contributed by Jim Kingdon, 13-May-2020.) |
⊢ ((∀𝑧(𝐹‘𝑧) ∈ V ∧ 𝐴 ∈ 𝑉) → frec(𝐹, 𝐴) Fn ω) | ||
Theorem | freccllem 6349* | Lemma for freccl 6350. Just giving a name to a common expression to simplify the proof. (Contributed by Jim Kingdon, 27-Mar-2022.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐹‘𝑧) ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ ω) & ⊢ 𝐺 = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})) ⇒ ⊢ (𝜑 → (frec(𝐹, 𝐴)‘𝐵) ∈ 𝑆) | ||
Theorem | freccl 6350* | Closure for finite recursion. (Contributed by Jim Kingdon, 27-Mar-2022.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐹‘𝑧) ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ ω) ⇒ ⊢ (𝜑 → (frec(𝐹, 𝐴)‘𝐵) ∈ 𝑆) | ||
Theorem | frecfcllem 6351* | Lemma for frecfcl 6352. Just giving a name to a common expression to simplify the proof. (Contributed by Jim Kingdon, 30-Mar-2022.) |
⊢ 𝐺 = recs((𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))})) ⇒ ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) → frec(𝐹, 𝐴):ω⟶𝑆) | ||
Theorem | frecfcl 6352* | Finite recursion yields a function on the natural numbers. (Contributed by Jim Kingdon, 30-Mar-2022.) |
⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) → frec(𝐹, 𝐴):ω⟶𝑆) | ||
Theorem | frecsuclem 6353* | Lemma for frecsuc 6354. Just giving a name to a common expression to simplify the proof. (Contributed by Jim Kingdon, 29-Mar-2022.) |
⊢ 𝐺 = (𝑔 ∈ V ↦ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑔 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝑔‘𝑚))) ∨ (dom 𝑔 = ∅ ∧ 𝑥 ∈ 𝐴))}) ⇒ ⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵))) | ||
Theorem | frecsuc 6354* | The successor value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 31-Mar-2022.) |
⊢ ((∀𝑧 ∈ 𝑆 (𝐹‘𝑧) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ ω) → (frec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(frec(𝐹, 𝐴)‘𝐵))) | ||
Theorem | frecrdg 6355* |
Transfinite recursion restricted to omega.
Given a suitable characteristic function, df-frec 6338 produces the same results as df-irdg 6317 restricted to ω. Presumably the theorem would also hold if 𝐹 Fn V were changed to ∀𝑧(𝐹‘𝑧) ∈ V. (Contributed by Jim Kingdon, 29-Aug-2019.) |
⊢ (𝜑 → 𝐹 Fn V) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ∀𝑥 𝑥 ⊆ (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → frec(𝐹, 𝐴) = (rec(𝐹, 𝐴) ↾ ω)) | ||
Syntax | c1o 6356 | Extend the definition of a class to include the ordinal number 1. |
class 1o | ||
Syntax | c2o 6357 | Extend the definition of a class to include the ordinal number 2. |
class 2o | ||
Syntax | c3o 6358 | Extend the definition of a class to include the ordinal number 3. |
class 3o | ||
Syntax | c4o 6359 | Extend the definition of a class to include the ordinal number 4. |
class 4o | ||
Syntax | coa 6360 | Extend the definition of a class to include the ordinal addition operation. |
class +o | ||
Syntax | comu 6361 | Extend the definition of a class to include the ordinal multiplication operation. |
class ·o | ||
Syntax | coei 6362 | Extend the definition of a class to include the ordinal exponentiation operation. |
class ↑o | ||
Definition | df-1o 6363 | Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.) |
⊢ 1o = suc ∅ | ||
Definition | df-2o 6364 | Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.) |
⊢ 2o = suc 1o | ||
Definition | df-3o 6365 | Define the ordinal number 3. (Contributed by Mario Carneiro, 14-Jul-2013.) |
⊢ 3o = suc 2o | ||
Definition | df-4o 6366 | Define the ordinal number 4. (Contributed by Mario Carneiro, 14-Jul-2013.) |
⊢ 4o = suc 3o | ||
Definition | df-oadd 6367* | Define the ordinal addition operation. (Contributed by NM, 3-May-1995.) |
⊢ +o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ suc 𝑧), 𝑥)‘𝑦)) | ||
Definition | df-omul 6368* | Define the ordinal multiplication operation. (Contributed by NM, 26-Aug-1995.) |
⊢ ·o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 +o 𝑥)), ∅)‘𝑦)) | ||
Definition | df-oexpi 6369* |
Define the ordinal exponentiation operation.
This definition is similar to a conventional definition of exponentiation except that it defines ∅ ↑o 𝐴 to be 1o for all 𝐴 ∈ On, in order to avoid having different cases for whether the base is ∅ or not. (Contributed by Mario Carneiro, 4-Jul-2019.) |
⊢ ↑o = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 ·o 𝑥)), 1o)‘𝑦)) | ||
Theorem | 1on 6370 | Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.) |
⊢ 1o ∈ On | ||
Theorem | 1oex 6371 | Ordinal 1 is a set. (Contributed by BJ, 4-Jul-2022.) |
⊢ 1o ∈ V | ||
Theorem | 2on 6372 | Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ 2o ∈ On | ||
Theorem | 2on0 6373 | Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011.) |
⊢ 2o ≠ ∅ | ||
Theorem | 3on 6374 | Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 3o ∈ On | ||
Theorem | 4on 6375 | Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 4o ∈ On | ||
Theorem | df1o2 6376 | Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.) |
⊢ 1o = {∅} | ||
Theorem | df2o3 6377 | Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 2o = {∅, 1o} | ||
Theorem | df2o2 6378 | Expanded value of the ordinal number 2. (Contributed by NM, 29-Jan-2004.) |
⊢ 2o = {∅, {∅}} | ||
Theorem | 1n0 6379 | Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.) |
⊢ 1o ≠ ∅ | ||
Theorem | xp01disj 6380 | Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by NM, 2-Jun-2007.) |
⊢ ((𝐴 × {∅}) ∩ (𝐶 × {1o})) = ∅ | ||
Theorem | xp01disjl 6381 | Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊢ (({∅} × 𝐴) ∩ ({1o} × 𝐶)) = ∅ | ||
Theorem | ordgt0ge1 6382 | Two ways to express that an ordinal class is positive. (Contributed by NM, 21-Dec-2004.) |
⊢ (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 1o ⊆ 𝐴)) | ||
Theorem | ordge1n0im 6383 | An ordinal greater than or equal to 1 is nonzero. (Contributed by Jim Kingdon, 26-Jun-2019.) |
⊢ (Ord 𝐴 → (1o ⊆ 𝐴 → 𝐴 ≠ ∅)) | ||
Theorem | el1o 6384 | Membership in ordinal one. (Contributed by NM, 5-Jan-2005.) |
⊢ (𝐴 ∈ 1o ↔ 𝐴 = ∅) | ||
Theorem | dif1o 6385 | Two ways to say that 𝐴 is a nonzero number of the set 𝐵. (Contributed by Mario Carneiro, 21-May-2015.) |
⊢ (𝐴 ∈ (𝐵 ∖ 1o) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅)) | ||
Theorem | 2oconcl 6386 | Closure of the pair swapping function on 2o. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ (𝐴 ∈ 2o → (1o ∖ 𝐴) ∈ 2o) | ||
Theorem | 0lt1o 6387 | Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005.) |
⊢ ∅ ∈ 1o | ||
Theorem | 0lt2o 6388 | Ordinal zero is less than ordinal two. (Contributed by Jim Kingdon, 31-Jul-2022.) |
⊢ ∅ ∈ 2o | ||
Theorem | 1lt2o 6389 | Ordinal one is less than ordinal two. (Contributed by Jim Kingdon, 31-Jul-2022.) |
⊢ 1o ∈ 2o | ||
Theorem | el2oss1o 6390 | Being an element of ordinal two implies being a subset of ordinal one. The converse is equivalent to excluded middle by ss1oel2o 13576. (Contributed by Jim Kingdon, 8-Aug-2022.) |
⊢ (𝐴 ∈ 2o → 𝐴 ⊆ 1o) | ||
Theorem | oafnex 6391 | The characteristic function for ordinal addition is defined everywhere. (Contributed by Jim Kingdon, 27-Jul-2019.) |
⊢ (𝑥 ∈ V ↦ suc 𝑥) Fn V | ||
Theorem | sucinc 6392* | Successor is increasing. (Contributed by Jim Kingdon, 25-Jun-2019.) |
⊢ 𝐹 = (𝑧 ∈ V ↦ suc 𝑧) ⇒ ⊢ ∀𝑥 𝑥 ⊆ (𝐹‘𝑥) | ||
Theorem | sucinc2 6393* | Successor is increasing. (Contributed by Jim Kingdon, 14-Jul-2019.) |
⊢ 𝐹 = (𝑧 ∈ V ↦ suc 𝑧) ⇒ ⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵)) | ||
Theorem | fnoa 6394 | Functionality and domain of ordinal addition. (Contributed by NM, 26-Aug-1995.) (Proof shortened by Mario Carneiro, 3-Jul-2019.) |
⊢ +o Fn (On × On) | ||
Theorem | oaexg 6395 | Ordinal addition is a set. (Contributed by Mario Carneiro, 3-Jul-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 +o 𝐵) ∈ V) | ||
Theorem | omfnex 6396* | The characteristic function for ordinal multiplication is defined everywhere. (Contributed by Jim Kingdon, 23-Aug-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ V ↦ (𝑥 +o 𝐴)) Fn V) | ||
Theorem | fnom 6397 | Functionality and domain of ordinal multiplication. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 3-Jul-2019.) |
⊢ ·o Fn (On × On) | ||
Theorem | omexg 6398 | Ordinal multiplication is a set. (Contributed by Mario Carneiro, 3-Jul-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ·o 𝐵) ∈ V) | ||
Theorem | fnoei 6399 | Functionality and domain of ordinal exponentiation. (Contributed by Mario Carneiro, 29-May-2015.) (Revised by Mario Carneiro, 3-Jul-2019.) |
⊢ ↑o Fn (On × On) | ||
Theorem | oeiexg 6400 | Ordinal exponentiation is a set. (Contributed by Mario Carneiro, 3-Jul-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑o 𝐵) ∈ V) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |