Home | Metamath
Proof Explorer Theorem List (p. 86 of 426) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | zfregclOLD 8501* | Obsolete version of zfregcl 8499 as of 28-Apr-2021. (Contributed by NM, 5-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴) | ||
Theorem | zfregOLD 8502* | Obsolete version of zfreg 8500 as of 28-Apr-2021. (Contributed by NM, 26-Nov-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅) | ||
Theorem | zfreg2OLD 8503* | Alternate version of zfreg 8500 obsolete as of 28-Apr-2021. (Contributed by NM, 17-Sep-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 (𝐴 ∩ 𝑥) = ∅) | ||
Theorem | elirrv 8504 | The membership relation is irreflexive: no set is a member of itself. Theorem 105 of [Suppes] p. 54. (This is trivial to prove from zfregfr 8509 and efrirr 5095, but this proof is direct from the Axiom of Regularity.) (Contributed by NM, 19-Aug-1993.) |
⊢ ¬ 𝑥 ∈ 𝑥 | ||
Theorem | elirr 8505 | No class is a member of itself. Exercise 6 of [TakeutiZaring] p. 22. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ ¬ 𝐴 ∈ 𝐴 | ||
Theorem | sucprcreg 8506 | A class is equal to its successor iff it is a proper class (assuming the Axiom of Regularity). (Contributed by NM, 9-Jul-2004.) (Proof shortened by BJ, 16-Apr-2019.) |
⊢ (¬ 𝐴 ∈ V ↔ suc 𝐴 = 𝐴) | ||
Theorem | ruv 8507 | The Russell class is equal to the universe V. Exercise 5 of [TakeutiZaring] p. 22. (Contributed by Alan Sare, 4-Oct-2008.) |
⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V | ||
Theorem | ruALT 8508 | Alternate proof of ru 3434, simplified using (indirectly) the Axiom of Regularity ax-reg 8497. (Contributed by Alan Sare, 4-Oct-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} ∉ V | ||
Theorem | zfregfr 8509 | The epsilon relation is well-founded on any class. (Contributed by NM, 26-Nov-1995.) |
⊢ E Fr 𝐴 | ||
Theorem | en2lp 8510 | No class has 2-cycle membership loops. Theorem 7X(b) of [Enderton] p. 206. (Contributed by NM, 16-Oct-1996.) (Revised by Mario Carneiro, 25-Jun-2015.) |
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴) | ||
Theorem | en3lplem1 8511* | Lemma for en3lp 8513. (Contributed by Alan Sare, 28-Oct-2011.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 = 𝐴 → (𝑥 ∩ {𝐴, 𝐵, 𝐶}) ≠ ∅)) | ||
Theorem | en3lplem2 8512* | Lemma for en3lp 8513. (Contributed by Alan Sare, 28-Oct-2011.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 ∈ {𝐴, 𝐵, 𝐶} → (𝑥 ∩ {𝐴, 𝐵, 𝐶}) ≠ ∅)) | ||
Theorem | en3lp 8513 | No class has 3-cycle membership loops. This proof was automatically generated from the virtual deduction proof en3lpVD 39080 using a translation program. (Contributed by Alan Sare, 24-Oct-2011.) |
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) | ||
Theorem | preleq 8514 | Equality of two unordered pairs when one member of each pair contains the other member. (Contributed by NM, 16-Oct-1996.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (((𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷) ∧ {𝐴, 𝐵} = {𝐶, 𝐷}) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | opthreg 8515 | Theorem for alternate representation of ordered pairs, requiring the Axiom of Regularity ax-reg 8497 (via the preleq 8514 step). See df-op 4184 for a description of other ordered pair representations. Exercise 34 of [Enderton] p. 207. (Contributed by NM, 16-Oct-1996.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ ({𝐴, {𝐴, 𝐵}} = {𝐶, {𝐶, 𝐷}} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | suc11reg 8516 | The successor operation behaves like a one-to-one function (assuming the Axiom of Regularity). Exercise 35 of [Enderton] p. 208 and its converse. (Contributed by NM, 25-Oct-2003.) |
⊢ (suc 𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵) | ||
Theorem | dford2 8517* | Assuming ax-reg 8497, an ordinal is a transitive class on which inclusion satisfies trichotomy. (Contributed by Scott Fenton, 27-Oct-2010.) |
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))) | ||
Theorem | inf0 8518* | Our Axiom of Infinity derived from existence of omega. The proof shows that the especially contrived class "ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) " exists, is a subset of its union, and contains a given set 𝑥 (and thus is nonempty). Thus, it provides an example demonstrating that a set 𝑦 exists with the necessary properties demanded by ax-inf 8535. (Contributed by NM, 15-Oct-1996.) |
⊢ ω ∈ V ⇒ ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))) | ||
Theorem | inf1 8519 | Variation of Axiom of Infinity (using zfinf 8536 as a hypothesis). Axiom of Infinity in [FreydScedrov] p. 283. (Contributed by NM, 14-Oct-1996.) (Revised by David Abernethy, 1-Oct-2013.) |
⊢ ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))) ⇒ ⊢ ∃𝑥(𝑥 ≠ ∅ ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))) | ||
Theorem | inf2 8520* | Variation of Axiom of Infinity. There exists a nonempty set that is a subset of its union (using zfinf 8536 as a hypothesis). Abbreviated version of the Axiom of Infinity in [FreydScedrov] p. 283. (Contributed by NM, 28-Oct-1996.) |
⊢ ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))) ⇒ ⊢ ∃𝑥(𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) | ||
Theorem | inf3lema 8521* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 8532 for detailed description. (Contributed by NM, 28-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ (𝐺‘𝐵) ↔ (𝐴 ∈ 𝑥 ∧ (𝐴 ∩ 𝑥) ⊆ 𝐵)) | ||
Theorem | inf3lemb 8522* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 8532 for detailed description. (Contributed by NM, 28-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹‘∅) = ∅ | ||
Theorem | inf3lemc 8523* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 8532 for detailed description. (Contributed by NM, 28-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ ω → (𝐹‘suc 𝐴) = (𝐺‘(𝐹‘𝐴))) | ||
Theorem | inf3lemd 8524* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 8532 for detailed description. (Contributed by NM, 28-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ ω → (𝐹‘𝐴) ⊆ 𝑥) | ||
Theorem | inf3lem1 8525* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 8532 for detailed description. (Contributed by NM, 28-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ ω → (𝐹‘𝐴) ⊆ (𝐹‘suc 𝐴)) | ||
Theorem | inf3lem2 8526* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 8532 for detailed description. (Contributed by NM, 28-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ≠ 𝑥)) | ||
Theorem | inf3lem3 8527* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 8532 for detailed description. In the proof, we invoke the Axiom of Regularity in the form of zfreg 8500. (Contributed by NM, 29-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ≠ (𝐹‘suc 𝐴))) | ||
Theorem | inf3lem4 8528* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 8532 for detailed description. (Contributed by NM, 29-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ⊊ (𝐹‘suc 𝐴))) | ||
Theorem | inf3lem5 8529* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 8532 for detailed description. (Contributed by NM, 29-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → (𝐹‘𝐵) ⊊ (𝐹‘𝐴))) | ||
Theorem | inf3lem6 8530* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 8532 for detailed description. (Contributed by NM, 29-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → 𝐹:ω–1-1→𝒫 𝑥) | ||
Theorem | inf3lem7 8531* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 8532 for detailed description. In the proof, we invoke the Axiom of Replacement in the form of f1dmex 7136. (Contributed by NM, 29-Oct-1996.) (Proof shortened by Mario Carneiro, 19-Jan-2013.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → ω ∈ V) | ||
Theorem | inf3 8532 |
Our Axiom of Infinity ax-inf 8535 implies the standard Axiom of Infinity.
The hypothesis is a variant of our Axiom of Infinity provided by
inf2 8520, and the conclusion is the version of the Axiom of Infinity
shown as Axiom 7 in [TakeutiZaring] p. 43. (Other standard versions are
proved later as axinf2 8537 and zfinf2 8539.) The main proof is provided by
inf3lema 8521 through inf3lem7 8531, and this final piece eliminates the
auxiliary hypothesis of inf3lem7 8531. This proof is due to
Ian Sutherland, Richard Heck, and Norman Megill and was posted
on Usenet as shown below. Although the result is not new, the authors
were unable to find a published proof.
(As posted to sci.logic on 30-Oct-1996, with annotations added.) Theorem: The statement "There exists a nonempty set that is a subset of its union" implies the Axiom of Infinity. Proof: Let X be a nonempty set which is a subset of its union; the latter property is equivalent to saying that for any y in X, there exists a z in X such that y is in z. Define by finite recursion a function F:omega-->(power X) such that F_0 = 0 (See inf3lemb 8522.) F_n+1 = {y<X | y^X subset F_n} (See inf3lemc 8523.) Note: ^ means intersect, < means \in ("element of"). (Finite recursion as typically done requires the existence of omega; to avoid this we can just use transfinite recursion restricted to omega. F is a class-term that is not necessarily a set at this point.) Lemma 1. F_n subset F_n+1. (See inf3lem1 8525.) Proof: By induction: F_0 subset F_1. If y < F_n+1, then y^X subset F_n, so if F_n subset F_n+1, then y^X subset F_n+1, so y < F_n+2. Lemma 2. F_n =/= X. (See inf3lem2 8526.) Proof: By induction: F_0 =/= X because X is not empty. Assume F_n =/= X. Then there is a y in X that is not in F_n. By definition of X, there is a z in X that contains y. Suppose F_n+1 = X. Then z is in F_n+1, and z^X contains y, so z^X is not a subset of F_n, contrary to the definition of F_n+1. Lemma 3. F_n =/= F_n+1. (See inf3lem3 8527.) Proof: Using the identity y^X subset F_n <-> y^(X-F_n) = 0, we have F_n+1 = {y<X | y^(X-F_n) = 0}. Let q = {y<X-F_n | y^(X-F_n) = 0}. Then q subset F_n+1. Since X-F_n is not empty by Lemma 2 and q is the set of \in-minimal elements of X-F_n, by Foundation q is not empty, so q and therefore F_n+1 have an element not in F_n. Lemma 4. F_n proper_subset F_n+1. (See inf3lem4 8528.) Proof: Lemmas 1 and 3. Lemma 5. F_m proper_subset F_n, m < n. (See inf3lem5 8529.) Proof: Fix m and use induction on n > m. Basis: F_m proper_subset F_m+1 by Lemma 4. Induction: Assume F_m proper_subset F_n. Then since F_n proper_subset F_n+1, F_m proper_subset F_n+1 by transitivity of proper subset. By Lemma 5, F_m =/= F_n for m =/= n, so F is 1-1. (See inf3lem6 8530.) Thus, the inverse of F is a function with range omega and domain a subset of power X, so omega exists by Replacement. (See inf3lem7 8531.) Q.E.D.(Contributed by NM, 29-Oct-1996.) |
⊢ ∃𝑥(𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) ⇒ ⊢ ω ∈ V | ||
Theorem | infeq5i 8533 | Half of infeq5 8534. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ (ω ∈ V → ∃𝑥 𝑥 ⊊ ∪ 𝑥) | ||
Theorem | infeq5 8534 | The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (shown on the right-hand side in the form of omex 8540.) The left-hand side provides us with a very short way to express the Axiom of Infinity using only elementary symbols. This proof of equivalence does not depend on the Axiom of Infinity. (Contributed by NM, 23-Mar-2004.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ (∃𝑥 𝑥 ⊊ ∪ 𝑥 ↔ ω ∈ V) | ||
Axiom | ax-inf 8535* |
Axiom of Infinity. An axiom of Zermelo-Fraenkel set theory. This axiom
is the gateway to "Cantor's paradise" (an expression coined by
Hilbert).
It asserts that given a starting set 𝑥, an infinite set 𝑦 built
from it exists. Although our version is apparently not given in the
literature, it is similar to, but slightly shorter than, the Axiom of
Infinity in [FreydScedrov] p. 283
(see inf1 8519 and inf2 8520). More
standard versions, which essentially state that there exists a set
containing all the natural numbers, are shown as zfinf2 8539 and omex 8540 and
are based on the (nontrivial) proof of inf3 8532.
This version has the
advantage that when expanded to primitives, it has fewer symbols than
the standard version ax-inf2 8538. Theorem inf0 8518
shows the reverse
derivation of our axiom from a standard one. Theorem inf5 8542
shows a
very short way to state this axiom.
The standard version of Infinity ax-inf2 8538 requires this axiom along with Regularity ax-reg 8497 for its derivation (as theorem axinf2 8537 below). In order to more easily identify the normal uses of Regularity, we will usually reference ax-inf2 8538 instead of this one. The derivation of this axiom from ax-inf2 8538 is shown by theorem axinf 8541. Proofs should normally use the standard version ax-inf2 8538 instead of this axiom. (New usage is discouraged.) (Contributed by NM, 16-Aug-1993.) |
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))) | ||
Theorem | zfinf 8536* | Axiom of Infinity expressed with the fewest number of different variables. (New usage is discouraged.) (Contributed by NM, 14-Aug-2003.) |
⊢ ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))) | ||
Theorem | axinf2 8537* |
A standard version of Axiom of Infinity, expanded to primitives, derived
from our version of Infinity ax-inf 8535 and Regularity ax-reg 8497.
This theorem should not be referenced in any proof. Instead, use ax-inf2 8538 below so that the ordinary uses of Regularity can be more easily identified. (New usage is discouraged.) (Contributed by NM, 3-Nov-1996.) |
⊢ ∃𝑥(∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑧 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))))) | ||
Axiom | ax-inf2 8538* | A standard version of Axiom of Infinity of ZF set theory. In English, it says: there exists a set that contains the empty set and the successors of all of its members. Theorem zfinf2 8539 shows it converted to abbreviations. This axiom was derived as theorem axinf2 8537 above, using our version of Infinity ax-inf 8535 and the Axiom of Regularity ax-reg 8497. We will reference ax-inf2 8538 instead of axinf2 8537 so that the ordinary uses of Regularity can be more easily identified. The reverse derivation of ax-inf 8535 from ax-inf2 8538 is shown by theorem axinf 8541. (Contributed by NM, 3-Nov-1996.) |
⊢ ∃𝑥(∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑧 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))))) | ||
Theorem | zfinf2 8539* | A standard version of the Axiom of Infinity, using definitions to abbreviate. Axiom Inf of [BellMachover] p. 472. (See ax-inf2 8538 for the unabbreviated version.) (Contributed by NM, 30-Aug-1993.) |
⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) | ||
Theorem | omex 8540 |
The existence of omega (the class of natural numbers). Axiom 7 of
[TakeutiZaring] p. 43. This
theorem is proved assuming the Axiom of
Infinity and in fact is equivalent to it, as shown by the reverse
derivation inf0 8518.
A finitist (someone who doesn't believe in infinity) could, without contradiction, replace the Axiom of Infinity by its denial ¬ ω ∈ V; this would lead to ω = On by omon 7076 and Fin = V (the universe of all sets) by fineqv 8175. The finitist could still develop natural number, integer, and rational number arithmetic but would be denied the real numbers (as well as much of the rest of mathematics). In deference to the finitist, much of our development is done, when possible, without invoking the Axiom of Infinity; an example is Peano's axioms peano1 7085 through peano5 7089 (which many textbooks prove more easily assuming Infinity). (Contributed by NM, 6-Aug-1994.) |
⊢ ω ∈ V | ||
Theorem | axinf 8541* | The first version of the Axiom of Infinity ax-inf 8535 proved from the second version ax-inf2 8538. Note that we didn't use ax-reg 8497, unlike the other direction axinf2 8537. (Contributed by NM, 24-Apr-2009.) |
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))) | ||
Theorem | inf5 8542 | The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (see theorem infeq5 8534). This provides us with a very compact way to express the Axiom of Infinity using only elementary symbols. (Contributed by NM, 3-Jun-2005.) |
⊢ ∃𝑥 𝑥 ⊊ ∪ 𝑥 | ||
Theorem | omelon 8543 | Omega is an ordinal number. (Contributed by NM, 10-May-1998.) (Revised by Mario Carneiro, 30-Jan-2013.) |
⊢ ω ∈ On | ||
Theorem | dfom3 8544* | The class of natural numbers omega can be defined as the smallest "inductive set," which is valid provided we assume the Axiom of Infinity. Definition 6.3 of [Eisenberg] p. 82. (Contributed by NM, 6-Aug-1994.) |
⊢ ω = ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} | ||
Theorem | elom3 8545* | A simplification of elom 7068 assuming the Axiom of Infinity. (Contributed by NM, 30-May-2003.) |
⊢ (𝐴 ∈ ω ↔ ∀𝑥(Lim 𝑥 → 𝐴 ∈ 𝑥)) | ||
Theorem | dfom4 8546* | A simplification of df-om 7066 assuming the Axiom of Infinity. (Contributed by NM, 30-May-2003.) |
⊢ ω = {𝑥 ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)} | ||
Theorem | dfom5 8547 | ω is the smallest limit ordinal and can be defined as such (although the Axiom of Infinity is needed to ensure that at least one limit ordinal exists). (Contributed by FL, 22-Feb-2011.) (Revised by Mario Carneiro, 2-Feb-2013.) |
⊢ ω = ∩ {𝑥 ∣ Lim 𝑥} | ||
Theorem | oancom 8548 | Ordinal addition is not commutative. This theorem shows a counterexample. Remark in [TakeutiZaring] p. 60. (Contributed by NM, 10-Dec-2004.) |
⊢ (1𝑜 +𝑜 ω) ≠ (ω +𝑜 1𝑜) | ||
Theorem | isfinite 8549 | A set is finite iff it is strictly dominated by the class of natural number. Theorem 42 of [Suppes] p. 151. The Axiom of Infinity is used for the forward implication. (Contributed by FL, 16-Apr-2011.) |
⊢ (𝐴 ∈ Fin ↔ 𝐴 ≺ ω) | ||
Theorem | fict 8550 | A finite set is countable (weaker version of isfinite 8549). (Contributed by Thierry Arnoux, 27-Mar-2018.) |
⊢ (𝐴 ∈ Fin → 𝐴 ≼ ω) | ||
Theorem | nnsdom 8551 | A natural number is strictly dominated by the set of natural numbers. Example 3 of [Enderton] p. 146. (Contributed by NM, 28-Oct-2003.) |
⊢ (𝐴 ∈ ω → 𝐴 ≺ ω) | ||
Theorem | omenps 8552 | Omega is equinumerous to a proper subset of itself. Example 13.2(4) of [Eisenberg] p. 216. (Contributed by NM, 30-Jul-2003.) |
⊢ ω ≈ (ω ∖ {∅}) | ||
Theorem | omensuc 8553 | The set of natural numbers is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.) |
⊢ ω ≈ suc ω | ||
Theorem | infdifsn 8554 | Removing a singleton from an infinite set does not change the cardinality of the set. (Contributed by Mario Carneiro, 30-Apr-2015.) (Revised by Mario Carneiro, 16-May-2015.) |
⊢ (ω ≼ 𝐴 → (𝐴 ∖ {𝐵}) ≈ 𝐴) | ||
Theorem | infdiffi 8555 | Removing a finite set from an infinite set does not change the cardinality of the set. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ ((ω ≼ 𝐴 ∧ 𝐵 ∈ Fin) → (𝐴 ∖ 𝐵) ≈ 𝐴) | ||
Theorem | unbnn3 8556* | Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. This version of unbnn 8216 eliminates its hypothesis by assuming the Axiom of Infinity. (Contributed by NM, 4-May-2005.) |
⊢ ((𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦) → 𝐴 ≈ ω) | ||
Theorem | noinfep 8557* | Using the Axiom of Regularity in the form zfregfr 8509, show that there are no infinite descending ∈-chains. Proposition 7.34 of [TakeutiZaring] p. 44. (Contributed by NM, 26-Jan-2006.) (Revised by Mario Carneiro, 22-Mar-2013.) |
⊢ ∃𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥) | ||
Syntax | ccnf 8558 | Extend class notation with the Cantor normal form function. |
class CNF | ||
Definition | df-cnf 8559* | Define the Cantor normal form function, which takes as input a finitely supported function from 𝑦 to 𝑥 and outputs the corresponding member of the ordinal exponential 𝑥 ↑𝑜 𝑦. The content of the original Cantor Normal Form theorem is that for 𝑥 = ω this function is a bijection onto ω ↑𝑜 𝑦 for any ordinal 𝑦 (or, since the function restricts naturally to different ordinals, the statement that the composite function is a bijection to On). More can be said about the function, however, and in particular it is an order isomorphism for a certain easily defined well-ordering of the finitely supported functions, which gives an alternate definition cantnffval2 8592 of this function in terms of df-oi 8415. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 28-Jun-2019.) |
⊢ CNF = (𝑥 ∈ On, 𝑦 ∈ On ↦ (𝑓 ∈ {𝑔 ∈ (𝑥 ↑𝑚 𝑦) ∣ 𝑔 finSupp ∅} ↦ ⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝑥 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)), ∅)‘dom ℎ))) | ||
Theorem | cantnffval 8560* | The value of the Cantor normal form function. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 28-Jun-2019.) |
⊢ 𝑆 = {𝑔 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑔 finSupp ∅} & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) ⇒ ⊢ (𝜑 → (𝐴 CNF 𝐵) = (𝑓 ∈ 𝑆 ↦ ⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)), ∅)‘dom ℎ))) | ||
Theorem | cantnfdm 8561* | The domain of the Cantor normal form function (in later lemmas we will use dom (𝐴 CNF 𝐵) to abbreviate "the set of finitely supported functions from 𝐵 to 𝐴"). (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 28-Jun-2019.) |
⊢ 𝑆 = {𝑔 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑔 finSupp ∅} & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) ⇒ ⊢ (𝜑 → dom (𝐴 CNF 𝐵) = 𝑆) | ||
Theorem | cantnfvalf 8562* | Lemma for cantnf 8590. The function appearing in cantnfval 8565 is unconditionally a function. (Contributed by Mario Carneiro, 20-May-2015.) |
⊢ 𝐹 = seq𝜔((𝑘 ∈ 𝐴, 𝑧 ∈ 𝐵 ↦ (𝐶 +𝑜 𝐷)), ∅) ⇒ ⊢ 𝐹:ω⟶On | ||
Theorem | cantnfs 8563 | Elementhood in the set of finitely supported functions from 𝐵 to 𝐴. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 28-Jun-2019.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) ⇒ ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))) | ||
Theorem | cantnfcl 8564 | Basic properties of the order isomorphism 𝐺 used later. The support of an 𝐹 ∈ 𝑆 is a finite subset of 𝐴, so it is well-ordered by E and the order isomorphism has domain a finite ordinal. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 28-Jun-2019.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅)) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) ⇒ ⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω)) | ||
Theorem | cantnfval 8565* | The value of the Cantor normal form function. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 28-Jun-2019.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅)) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)), ∅) ⇒ ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (𝐻‘dom 𝐺)) | ||
Theorem | cantnfval2 8566* | Alternate expression for the value of the Cantor normal form function. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 28-Jun-2019.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅)) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)), ∅) ⇒ ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (seq𝜔((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)), ∅)‘dom 𝐺)) | ||
Theorem | cantnfsuc 8567* | The value of the recursive function 𝐻 at a successor. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 28-Jun-2019.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅)) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)), ∅) ⇒ ⊢ ((𝜑 ∧ 𝐾 ∈ ω) → (𝐻‘suc 𝐾) = (((𝐴 ↑𝑜 (𝐺‘𝐾)) ·𝑜 (𝐹‘(𝐺‘𝐾))) +𝑜 (𝐻‘𝐾))) | ||
Theorem | cantnfle 8568* | A lower bound on the CNF function. Since ((𝐴 CNF 𝐵)‘𝐹) is defined as the sum of (𝐴 ↑𝑜 𝑥) ·𝑜 (𝐹‘𝑥) over all 𝑥 in the support of 𝐹, it is larger than any of these terms (and all other terms are zero, so we can extend the statement to all 𝐶 ∈ 𝐵 instead of just those 𝐶 in the support). (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 28-Jun-2019.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅)) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)), ∅) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝐴 ↑𝑜 𝐶) ·𝑜 (𝐹‘𝐶)) ⊆ ((𝐴 CNF 𝐵)‘𝐹)) | ||
Theorem | cantnflt 8569* | An upper bound on the partial sums of the CNF function. Since each term dominates all previous terms, by induction we can bound the whole sum with any exponent 𝐴 ↑𝑜 𝐶 where 𝐶 is larger than any exponent (𝐺‘𝑥), 𝑥 ∈ 𝐾 which has been summed so far. (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 29-Jun-2019.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅)) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)), ∅) & ⊢ (𝜑 → ∅ ∈ 𝐴) & ⊢ (𝜑 → 𝐾 ∈ suc dom 𝐺) & ⊢ (𝜑 → 𝐶 ∈ On) & ⊢ (𝜑 → (𝐺 “ 𝐾) ⊆ 𝐶) ⇒ ⊢ (𝜑 → (𝐻‘𝐾) ∈ (𝐴 ↑𝑜 𝐶)) | ||
Theorem | cantnflt2 8570 | An upper bound on the CNF function. (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 29-Jun-2019.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ (𝜑 → ∅ ∈ 𝐴) & ⊢ (𝜑 → 𝐶 ∈ On) & ⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐶) ⇒ ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑𝑜 𝐶)) | ||
Theorem | cantnff 8571 | The CNF function is a function from finitely supported functions from 𝐵 to 𝐴, to the ordinal exponential 𝐴 ↑𝑜 𝐵. (Contributed by Mario Carneiro, 28-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) ⇒ ⊢ (𝜑 → (𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑𝑜 𝐵)) | ||
Theorem | cantnf0 8572 | The value of the zero function. (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → ∅ ∈ 𝐴) ⇒ ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅) | ||
Theorem | cantnfrescl 8573* | A function is finitely supported from 𝐵 to 𝐴 iff the extended function is finitely supported from 𝐷 to 𝐴. (Contributed by Mario Carneiro, 25-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → 𝐷 ∈ On) & ⊢ (𝜑 → 𝐵 ⊆ 𝐷) & ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐷 ∖ 𝐵)) → 𝑋 = ∅) & ⊢ (𝜑 → ∅ ∈ 𝐴) & ⊢ 𝑇 = dom (𝐴 CNF 𝐷) ⇒ ⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋) ∈ 𝑆 ↔ (𝑛 ∈ 𝐷 ↦ 𝑋) ∈ 𝑇)) | ||
Theorem | cantnfres 8574* | The CNF function respects extensions of the domain to a larger ordinal. (Contributed by Mario Carneiro, 25-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → 𝐷 ∈ On) & ⊢ (𝜑 → 𝐵 ⊆ 𝐷) & ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐷 ∖ 𝐵)) → 𝑋 = ∅) & ⊢ (𝜑 → ∅ ∈ 𝐴) & ⊢ 𝑇 = dom (𝐴 CNF 𝐷) & ⊢ (𝜑 → (𝑛 ∈ 𝐵 ↦ 𝑋) ∈ 𝑆) ⇒ ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑛 ∈ 𝐵 ↦ 𝑋)) = ((𝐴 CNF 𝐷)‘(𝑛 ∈ 𝐷 ↦ 𝑋))) | ||
Theorem | cantnfp1lem1 8575* | Lemma for cantnfp1 8578. (Contributed by Mario Carneiro, 20-Jun-2015.) (Revised by AV, 30-Jun-2019.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝑋) & ⊢ 𝐹 = (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡))) ⇒ ⊢ (𝜑 → 𝐹 ∈ 𝑆) | ||
Theorem | cantnfp1lem2 8576* | Lemma for cantnfp1 8578. (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 30-Jun-2019.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝑋) & ⊢ 𝐹 = (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡))) & ⊢ (𝜑 → ∅ ∈ 𝑌) & ⊢ 𝑂 = OrdIso( E , (𝐹 supp ∅)) ⇒ ⊢ (𝜑 → dom 𝑂 = suc ∪ dom 𝑂) | ||
Theorem | cantnfp1lem3 8577* | Lemma for cantnfp1 8578. (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 1-Jul-2019.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝑋) & ⊢ 𝐹 = (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡))) & ⊢ (𝜑 → ∅ ∈ 𝑌) & ⊢ 𝑂 = OrdIso( E , (𝐹 supp ∅)) & ⊢ 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (𝑂‘𝑘)) ·𝑜 (𝐹‘(𝑂‘𝑘))) +𝑜 𝑧)), ∅) & ⊢ 𝐾 = OrdIso( E , (𝐺 supp ∅)) & ⊢ 𝑀 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (𝐾‘𝑘)) ·𝑜 (𝐺‘(𝐾‘𝑘))) +𝑜 𝑧)), ∅) ⇒ ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴 ↑𝑜 𝑋) ·𝑜 𝑌) +𝑜 ((𝐴 CNF 𝐵)‘𝐺))) | ||
Theorem | cantnfp1 8578* | If 𝐹 is created by adding a single term (𝐹‘𝑋) = 𝑌 to 𝐺, where 𝑋 is larger than any element of the support of 𝐺, then 𝐹 is also a finitely supported function and it is assigned the value ((𝐴 ↑𝑜 𝑋) ·𝑜 𝑌) +𝑜 𝑧 where 𝑧 is the value of 𝐺. (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 1-Jul-2019.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝑋) & ⊢ 𝐹 = (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡))) ⇒ ⊢ (𝜑 → (𝐹 ∈ 𝑆 ∧ ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴 ↑𝑜 𝑋) ·𝑜 𝑌) +𝑜 ((𝐴 CNF 𝐵)‘𝐺)))) | ||
Theorem | oemapso 8579* | The relation 𝑇 is a strict order on 𝑆 (a corollary of wemapso2 8458). (Contributed by Mario Carneiro, 28-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ⇒ ⊢ (𝜑 → 𝑇 Or 𝑆) | ||
Theorem | oemapval 8580* | Value of the relation 𝑇. (Contributed by Mario Carneiro, 28-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐹𝑇𝐺 ↔ ∃𝑧 ∈ 𝐵 ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) | ||
Theorem | oemapvali 8581* | If 𝐹 < 𝐺, then there is some 𝑧 witnessing this, but we can say more and in fact there is a definable expression 𝑋 that also witnesses 𝐹 < 𝐺. (Contributed by Mario Carneiro, 25-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) & ⊢ (𝜑 → 𝐹𝑇𝐺) & ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ (𝐹‘𝑋) ∈ (𝐺‘𝑋) ∧ ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))) | ||
Theorem | cantnflem1a 8582* | Lemma for cantnf 8590. (Contributed by Mario Carneiro, 4-Jun-2015.) (Revised by AV, 2-Jul-2019.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) & ⊢ (𝜑 → 𝐹𝑇𝐺) & ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝐺 supp ∅)) | ||
Theorem | cantnflem1b 8583* | Lemma for cantnf 8590. (Contributed by Mario Carneiro, 4-Jun-2015.) (Revised by AV, 2-Jul-2019.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) & ⊢ (𝜑 → 𝐹𝑇𝐺) & ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} & ⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅)) ⇒ ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑋 ⊆ (𝑂‘𝑢)) | ||
Theorem | cantnflem1c 8584* | Lemma for cantnf 8590. (Contributed by Mario Carneiro, 4-Jun-2015.) (Revised by AV, 2-Jul-2019.) (Proof shortened by AV, 4-Apr-2020.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) & ⊢ (𝜑 → 𝐹𝑇𝐺) & ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} & ⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅)) ⇒ ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑥 ∈ (𝐺 supp ∅)) | ||
Theorem | cantnflem1d 8585* | Lemma for cantnf 8590. (Contributed by Mario Carneiro, 4-Jun-2015.) (Revised by AV, 2-Jul-2019.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) & ⊢ (𝜑 → 𝐹𝑇𝐺) & ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} & ⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅)) & ⊢ 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (𝑂‘𝑘)) ·𝑜 (𝐺‘(𝑂‘𝑘))) +𝑜 𝑧)), ∅) ⇒ ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (◡𝑂‘𝑋))) | ||
Theorem | cantnflem1 8586* | Lemma for cantnf 8590. This part of the proof is showing uniqueness of the Cantor normal form. We already know that the relation 𝑇 is a strict order, but we haven't shown it is a well-order yet. But being a strict order is enough to show that two distinct 𝐹, 𝐺 are 𝑇 -related as 𝐹 < 𝐺 or 𝐺 < 𝐹, and WLOG assuming that 𝐹 < 𝐺, we show that CNF respects this order and maps these two to different ordinals. (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 2-Jul-2019.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) & ⊢ (𝜑 → 𝐹𝑇𝐺) & ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} & ⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅)) & ⊢ 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (𝑂‘𝑘)) ·𝑜 (𝐺‘(𝑂‘𝑘))) +𝑜 𝑧)), ∅) ⇒ ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘𝐺)) | ||
Theorem | cantnflem2 8587* | Lemma for cantnf 8590. (Contributed by Mario Carneiro, 28-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝐶 ∈ (𝐴 ↑𝑜 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ ran (𝐴 CNF 𝐵)) & ⊢ (𝜑 → ∅ ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐶 ∈ (On ∖ 1𝑜))) | ||
Theorem | cantnflem3 8588* | Lemma for cantnf 8590. Here we show existence of Cantor normal forms. Assuming (by transfinite induction) that every number less than 𝐶 has a normal form, we can use oeeu 7683 to factor 𝐶 into the form ((𝐴 ↑𝑜 𝑋) ·𝑜 𝑌) +𝑜 𝑍 where 0 < 𝑌 < 𝐴 and 𝑍 < (𝐴 ↑𝑜 𝑋) (and a fortiori 𝑋 < 𝐵). Then since 𝑍 < (𝐴 ↑𝑜 𝑋) ≤ (𝐴 ↑𝑜 𝑋) ·𝑜 𝑌 ≤ 𝐶, 𝑍 has a normal form, and by appending the term (𝐴 ↑𝑜 𝑋) ·𝑜 𝑌 using cantnfp1 8578 we get a normal form for 𝐶. (Contributed by Mario Carneiro, 28-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝐶 ∈ (𝐴 ↑𝑜 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ ran (𝐴 CNF 𝐵)) & ⊢ (𝜑 → ∅ ∈ 𝐶) & ⊢ 𝑋 = ∪ ∩ {𝑐 ∈ On ∣ 𝐶 ∈ (𝐴 ↑𝑜 𝑐)} & ⊢ 𝑃 = (℩𝑑∃𝑎 ∈ On ∃𝑏 ∈ (𝐴 ↑𝑜 𝑋)(𝑑 = 〈𝑎, 𝑏〉 ∧ (((𝐴 ↑𝑜 𝑋) ·𝑜 𝑎) +𝑜 𝑏) = 𝐶)) & ⊢ 𝑌 = (1st ‘𝑃) & ⊢ 𝑍 = (2nd ‘𝑃) & ⊢ (𝜑 → 𝐺 ∈ 𝑆) & ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = 𝑍) & ⊢ 𝐹 = (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡))) ⇒ ⊢ (𝜑 → 𝐶 ∈ ran (𝐴 CNF 𝐵)) | ||
Theorem | cantnflem4 8589* | Lemma for cantnf 8590. Complete the induction step of cantnflem3 8588. (Contributed by Mario Carneiro, 25-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝐶 ∈ (𝐴 ↑𝑜 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ ran (𝐴 CNF 𝐵)) & ⊢ (𝜑 → ∅ ∈ 𝐶) & ⊢ 𝑋 = ∪ ∩ {𝑐 ∈ On ∣ 𝐶 ∈ (𝐴 ↑𝑜 𝑐)} & ⊢ 𝑃 = (℩𝑑∃𝑎 ∈ On ∃𝑏 ∈ (𝐴 ↑𝑜 𝑋)(𝑑 = 〈𝑎, 𝑏〉 ∧ (((𝐴 ↑𝑜 𝑋) ·𝑜 𝑎) +𝑜 𝑏) = 𝐶)) & ⊢ 𝑌 = (1st ‘𝑃) & ⊢ 𝑍 = (2nd ‘𝑃) ⇒ ⊢ (𝜑 → 𝐶 ∈ ran (𝐴 CNF 𝐵)) | ||
Theorem | cantnf 8590* | The Cantor Normal Form theorem. The function (𝐴 CNF 𝐵), which maps a finitely supported function from 𝐵 to 𝐴 to the sum ((𝐴 ↑𝑜 𝑓(𝑎1)) ∘ 𝑎1) +𝑜 ((𝐴 ↑𝑜 𝑓(𝑎2)) ∘ 𝑎2) +𝑜 ... over all indexes 𝑎 < 𝐵 such that 𝑓(𝑎) is nonzero, is an order isomorphism from the ordering 𝑇 of finitely supported functions to the set (𝐴 ↑𝑜 𝐵) under the natural order. Setting 𝐴 = ω and letting 𝐵 be arbitrarily large, the surjectivity of this function implies that every ordinal has a Cantor normal form (and injectivity, together with coherence cantnfres 8574, implies that such a representation is unique). (Contributed by Mario Carneiro, 28-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ⇒ ⊢ (𝜑 → (𝐴 CNF 𝐵) Isom 𝑇, E (𝑆, (𝐴 ↑𝑜 𝐵))) | ||
Theorem | oemapwe 8591* | The lexicographic order on a function space of ordinals gives a well-ordering with order type equal to the ordinal exponential. This provides an alternate definition of the ordinal exponential. (Contributed by Mario Carneiro, 28-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ⇒ ⊢ (𝜑 → (𝑇 We 𝑆 ∧ dom OrdIso(𝑇, 𝑆) = (𝐴 ↑𝑜 𝐵))) | ||
Theorem | cantnffval2 8592* | An alternate definition of df-cnf 8559 which relies on cantnf 8590. (Note that although the use of 𝑆 seems self-referential, one can use cantnfdm 8561 to eliminate it.) (Contributed by Mario Carneiro, 28-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ⇒ ⊢ (𝜑 → (𝐴 CNF 𝐵) = ◡OrdIso(𝑇, 𝑆)) | ||
Theorem | cantnff1o 8593 | Simplify the isomorphism of cantnf 8590 to simple bijection. (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ 𝑆 = dom (𝐴 CNF 𝐵) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) ⇒ ⊢ (𝜑 → (𝐴 CNF 𝐵):𝑆–1-1-onto→(𝐴 ↑𝑜 𝐵)) | ||
Theorem | wemapwe 8594* | Construct lexicographic order on a function space based on a reverse well-ordering of the indexes and a well-ordering of the values. (Contributed by Mario Carneiro, 29-May-2015.) (Revised by AV, 3-Jul-2019.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑧𝑅𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ 𝑈 = {𝑥 ∈ (𝐵 ↑𝑚 𝐴) ∣ 𝑥 finSupp 𝑍} & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑆 We 𝐵) & ⊢ (𝜑 → 𝐵 ≠ ∅) & ⊢ 𝐹 = OrdIso(𝑅, 𝐴) & ⊢ 𝐺 = OrdIso(𝑆, 𝐵) & ⊢ 𝑍 = (𝐺‘∅) ⇒ ⊢ (𝜑 → 𝑇 We 𝑈) | ||
Theorem | oef1o 8595* | A bijection of the base sets induces a bijection on ordinal exponentials. (The assumption (𝐹‘∅) = ∅ can be discharged using fveqf1o 6557.) (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 3-Jul-2019.) |
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐶) & ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷) & ⊢ (𝜑 → 𝐴 ∈ (On ∖ 1𝑜)) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → 𝐶 ∈ On) & ⊢ (𝜑 → 𝐷 ∈ On) & ⊢ (𝜑 → (𝐹‘∅) = ∅) & ⊢ 𝐾 = (𝑦 ∈ {𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡𝐺))) & ⊢ 𝐻 = (((𝐶 CNF 𝐷) ∘ 𝐾) ∘ ◡(𝐴 CNF 𝐵)) ⇒ ⊢ (𝜑 → 𝐻:(𝐴 ↑𝑜 𝐵)–1-1-onto→(𝐶 ↑𝑜 𝐷)) | ||
Theorem | cnfcomlem 8596* | Lemma for cnfcom 8597. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 3-Jul-2019.) |
⊢ 𝑆 = dom (ω CNF 𝐴) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ (ω ↑𝑜 𝐴)) & ⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵) & ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅)) & ⊢ 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +𝑜 𝑧)), ∅) & ⊢ 𝑇 = seq𝜔((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅) & ⊢ 𝑀 = ((ω ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) & ⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑥))) & ⊢ (𝜑 → 𝐼 ∈ dom 𝐺) & ⊢ (𝜑 → 𝑂 ∈ (ω ↑𝑜 (𝐺‘𝐼))) & ⊢ (𝜑 → (𝑇‘𝐼):(𝐻‘𝐼)–1-1-onto→𝑂) ⇒ ⊢ (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) | ||
Theorem | cnfcom 8597* | Any ordinal 𝐵 is equinumerous to the leading term of its Cantor normal form. Here we show that bijection explicitly. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 3-Jul-2019.) |
⊢ 𝑆 = dom (ω CNF 𝐴) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ (ω ↑𝑜 𝐴)) & ⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵) & ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅)) & ⊢ 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +𝑜 𝑧)), ∅) & ⊢ 𝑇 = seq𝜔((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅) & ⊢ 𝑀 = ((ω ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) & ⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑥))) & ⊢ (𝜑 → 𝐼 ∈ dom 𝐺) ⇒ ⊢ (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) | ||
Theorem | cnfcom2lem 8598* | Lemma for cnfcom2 8599. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 3-Jul-2019.) |
⊢ 𝑆 = dom (ω CNF 𝐴) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ (ω ↑𝑜 𝐴)) & ⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵) & ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅)) & ⊢ 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +𝑜 𝑧)), ∅) & ⊢ 𝑇 = seq𝜔((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅) & ⊢ 𝑀 = ((ω ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) & ⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑥))) & ⊢ 𝑊 = (𝐺‘∪ dom 𝐺) & ⊢ (𝜑 → ∅ ∈ 𝐵) ⇒ ⊢ (𝜑 → dom 𝐺 = suc ∪ dom 𝐺) | ||
Theorem | cnfcom2 8599* | Any nonzero ordinal 𝐵 is equinumerous to the leading term of its Cantor normal form. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 3-Jul-2019.) |
⊢ 𝑆 = dom (ω CNF 𝐴) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ (ω ↑𝑜 𝐴)) & ⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵) & ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅)) & ⊢ 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +𝑜 𝑧)), ∅) & ⊢ 𝑇 = seq𝜔((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅) & ⊢ 𝑀 = ((ω ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) & ⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑥))) & ⊢ 𝑊 = (𝐺‘∪ dom 𝐺) & ⊢ (𝜑 → ∅ ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑇‘dom 𝐺):𝐵–1-1-onto→((ω ↑𝑜 𝑊) ·𝑜 (𝐹‘𝑊))) | ||
Theorem | cnfcom3lem 8600* | Lemma for cnfcom3 8601. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 4-Jul-2019.) |
⊢ 𝑆 = dom (ω CNF 𝐴) & ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ (ω ↑𝑜 𝐴)) & ⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵) & ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅)) & ⊢ 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +𝑜 𝑧)), ∅) & ⊢ 𝑇 = seq𝜔((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅) & ⊢ 𝑀 = ((ω ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) & ⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑥))) & ⊢ 𝑊 = (𝐺‘∪ dom 𝐺) & ⊢ (𝜑 → ω ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝑊 ∈ (On ∖ 1𝑜)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |