Home | Metamath
Proof Explorer Theorem List (p. 91 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | wemaplem3 9001* | Lemma for wemapso 9004. Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝑃 ∈ (𝐵 ↑m 𝐴)) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m 𝐴)) & ⊢ (𝜑 → 𝑄 ∈ (𝐵 ↑m 𝐴)) & ⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝑆 Po 𝐵) & ⊢ (𝜑 → 𝑃𝑇𝑋) & ⊢ (𝜑 → 𝑋𝑇𝑄) ⇒ ⊢ (𝜑 → 𝑃𝑇𝑄) | ||
Theorem | wemappo 9002* |
Construct lexicographic order on a function space based on a
well-ordering of the indices and a total ordering of the values.
Without totality on the values or least differing indices, the best we can prove here is a partial order. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐵 ↑m 𝐴)) | ||
Theorem | wemapsolem 9003* | Lemma for wemapso 9004. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ 𝑈 ⊆ (𝐵 ↑m 𝐴) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝑆 Or 𝐵) & ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐) ⇒ ⊢ (𝜑 → 𝑇 Or 𝑈) | ||
Theorem | wemapso 9004* | Construct lexicographic order on a function space based on a well-ordering of the indices and a total ordering of the values. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Or (𝐵 ↑m 𝐴)) | ||
Theorem | wemapso2lem 9005* | Lemma for wemapso2 9006. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 1-Jul-2019.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ 𝑈 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍} ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) → 𝑇 Or 𝑈) | ||
Theorem | wemapso2 9006* | An alternative to having a well-order on 𝑅 in wemapso 9004 is to restrict the function set to finitely-supported functions. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 1-Jul-2019.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ 𝑈 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Or 𝑈) | ||
Theorem | card2on 9007* | The alternate definition of the cardinal of a set given in cardval2 9409 always gives a set, and indeed an ordinal. (Contributed by Mario Carneiro, 14-Jan-2013.) |
⊢ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ On | ||
Theorem | card2inf 9008* | The alternate definition of the cardinal of a set given in cardval2 9409 has the curious property that for non-numerable sets (for which ndmfv 6694 yields ∅), it still evaluates to a nonempty set, and indeed it contains ω. (Contributed by Mario Carneiro, 15-Jan-2013.) (Revised by Mario Carneiro, 27-Apr-2015.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (¬ ∃𝑦 ∈ On 𝑦 ≈ 𝐴 → ω ⊆ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴}) | ||
Syntax | char 9009 | Class symbol for the Hartogs/cardinal successor function. |
class har | ||
Syntax | cwdom 9010 | Class symbol for the weak dominance relation. |
class ≼* | ||
Definition | df-har 9011* |
Define the Hartogs function , which maps all sets to the smallest
ordinal that cannot be injected into the given set. In the important
special case where 𝑥 is an ordinal, this is the
cardinal successor
operation.
Traditionally, the Hartogs number of a set is written ℵ(𝑋) and the cardinal successor 𝑋 +; we use functional notation for this, and cannot use the aleph symbol because it is taken for the enumerating function of the infinite initial ordinals df-aleph 9358. Some authors define the Hartogs number of a set to be the least *infinite* ordinal which does not inject into it, thus causing the range to consist only of alephs. We use the simpler definition where the value can be any successor cardinal. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ har = (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦 ≼ 𝑥}) | ||
Definition | df-wdom 9012* | A set is weakly dominated by a "larger" set iff the "larger" set can be mapped onto the "smaller" set or the smaller set is empty; equivalently if the smaller set can be placed into bijection with some partition of the larger set. When choice is assumed (as fodom 9933), this coincides with the 1-1 definition df-dom 8500; however, it is not known whether this is a choice-equivalent or a strictly weaker form. Some discussion of this question can be found at http://boolesrings.org/asafk/2014/on-the-partition-principle/ 8500. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ ≼* = {〈𝑥, 𝑦〉 ∣ (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑥)} | ||
Theorem | harf 9013 | Functionality of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ har:V⟶On | ||
Theorem | harcl 9014 | Closure of the Hartogs function in the ordinals. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ (har‘𝑋) ∈ On | ||
Theorem | harval 9015* | Function value of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ (𝑋 ∈ 𝑉 → (har‘𝑋) = {𝑦 ∈ On ∣ 𝑦 ≼ 𝑋}) | ||
Theorem | elharval 9016 | The Hartogs number of a set is greater than all ordinals which inject into it. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 15-May-2015.) |
⊢ (𝑌 ∈ (har‘𝑋) ↔ (𝑌 ∈ On ∧ 𝑌 ≼ 𝑋)) | ||
Theorem | harndom 9017 | The Hartogs number of a set does not inject into that set. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 15-May-2015.) |
⊢ ¬ (har‘𝑋) ≼ 𝑋 | ||
Theorem | harword 9018 | Weak ordering property of the Hartogs function. (Contributed by Stefan O'Rear, 14-Feb-2015.) |
⊢ (𝑋 ≼ 𝑌 → (har‘𝑋) ⊆ (har‘𝑌)) | ||
Theorem | relwdom 9019 | Weak dominance is a relation. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ Rel ≼* | ||
Theorem | brwdom 9020* | Property of weak dominance (definitional form). (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ (𝑌 ∈ 𝑉 → (𝑋 ≼* 𝑌 ↔ (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋))) | ||
Theorem | brwdomi 9021* | Property of weak dominance, forward direction only. (Contributed by Mario Carneiro, 5-May-2015.) |
⊢ (𝑋 ≼* 𝑌 → (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋)) | ||
Theorem | brwdomn0 9022* | Weak dominance over nonempty sets. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ (𝑋 ≠ ∅ → (𝑋 ≼* 𝑌 ↔ ∃𝑧 𝑧:𝑌–onto→𝑋)) | ||
Theorem | 0wdom 9023 | Any set weakly dominates the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ (𝑋 ∈ 𝑉 → ∅ ≼* 𝑋) | ||
Theorem | fowdom 9024 | An onto function implies weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝑌–onto→𝑋) → 𝑋 ≼* 𝑌) | ||
Theorem | wdomref 9025 | Reflexivity of weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ (𝑋 ∈ 𝑉 → 𝑋 ≼* 𝑋) | ||
Theorem | brwdom2 9026* | Alternate characterization of the weak dominance predicate which does not require special treatment of the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ (𝑌 ∈ 𝑉 → (𝑋 ≼* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋)) | ||
Theorem | domwdom 9027 | Weak dominance is implied by dominance in the usual sense. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ (𝑋 ≼ 𝑌 → 𝑋 ≼* 𝑌) | ||
Theorem | wdomtr 9028 | Transitivity of weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ ((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) → 𝑋 ≼* 𝑍) | ||
Theorem | wdomen1 9029 | Equality-like theorem for equinumerosity and weak dominance. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≼* 𝐶 ↔ 𝐵 ≼* 𝐶)) | ||
Theorem | wdomen2 9030 | Equality-like theorem for equinumerosity and weak dominance. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≼* 𝐴 ↔ 𝐶 ≼* 𝐵)) | ||
Theorem | wdompwdom 9031 | Weak dominance strengthens to usual dominance on the power sets. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ (𝑋 ≼* 𝑌 → 𝒫 𝑋 ≼ 𝒫 𝑌) | ||
Theorem | canthwdom 9032 | Cantor's Theorem, stated using weak dominance (this is actually a stronger statement than canth2 8659, equivalent to canth 7100). (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ ¬ 𝒫 𝐴 ≼* 𝐴 | ||
Theorem | wdom2d 9033* | Deduce weak dominance from an implicit onto function (stated in a way which avoids ax-rep 5182). (Contributed by Stefan O'Rear, 13-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 𝑥 = 𝑋) ⇒ ⊢ (𝜑 → 𝐴 ≼* 𝐵) | ||
Theorem | wdomd 9034* | Deduce weak dominance from an implicit onto function. (Contributed by Stefan O'Rear, 13-Feb-2015.) |
⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 𝑥 = 𝑋) ⇒ ⊢ (𝜑 → 𝐴 ≼* 𝐵) | ||
Theorem | brwdom3 9035* | Condition for weak dominance with a condition reminiscent of wdomd 9034. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → (𝑋 ≼* 𝑌 ↔ ∃𝑓∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝑥 = (𝑓‘𝑦))) | ||
Theorem | brwdom3i 9036* | Weak dominance implies existence of a covering function. (Contributed by Stefan O'Rear, 13-Feb-2015.) |
⊢ (𝑋 ≼* 𝑌 → ∃𝑓∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝑥 = (𝑓‘𝑦)) | ||
Theorem | unwdomg 9037 | Weak dominance of a (disjoint) union. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
⊢ ((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷 ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 ∪ 𝐶) ≼* (𝐵 ∪ 𝐷)) | ||
Theorem | xpwdomg 9038 | Weak dominance of a Cartesian product. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
⊢ ((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷) → (𝐴 × 𝐶) ≼* (𝐵 × 𝐷)) | ||
Theorem | wdomima2g 9039 | A set is weakly dominant over its image under any function. This version of wdomimag 9040 is stated so as to avoid ax-rep 5182. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ 𝑉 ∧ (𝐹 “ 𝐴) ∈ 𝑊) → (𝐹 “ 𝐴) ≼* 𝐴) | ||
Theorem | wdomimag 9040 | A set is weakly dominant over its image under any function. (Contributed by Stefan O'Rear, 14-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ 𝑉) → (𝐹 “ 𝐴) ≼* 𝐴) | ||
Theorem | unxpwdom2 9041 | Lemma for unxpwdom 9042. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ ((𝐴 × 𝐴) ≈ (𝐵 ∪ 𝐶) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶)) | ||
Theorem | unxpwdom 9042 | If a Cartesian product is dominated by a union, then the base set is either weakly dominated by one factor of the union or dominated by the other. Extracted from Lemma 2.3 of [KanamoriPincus] p. 420. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ ((𝐴 × 𝐴) ≼ (𝐵 ∪ 𝐶) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶)) | ||
Theorem | harwdom 9043 | The Hartogs function is weakly dominated by 𝒫 (𝑋 × 𝑋). This follows from a more precise analysis of the bound used in hartogs 8997 to prove that (har‘𝑋) is a set. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (𝑋 ∈ 𝑉 → (har‘𝑋) ≼* 𝒫 (𝑋 × 𝑋)) | ||
Theorem | ixpiunwdom 9044* | Describe an onto function from the indexed cartesian product to the indexed union. Together with ixpssmapg 8481 this shows that ∪ 𝑥 ∈ 𝐴𝐵 and X𝑥 ∈ 𝐴𝐵 have closely linked cardinalities. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → ∪ 𝑥 ∈ 𝐴 𝐵 ≼* (X𝑥 ∈ 𝐴 𝐵 × 𝐴)) | ||
Axiom | ax-reg 9045* | Axiom of Regularity. An axiom of Zermelo-Fraenkel set theory. Also called the Axiom of Foundation. A rather non-intuitive axiom that denies more than it asserts, it states (in the form of zfreg 9048) that every nonempty set contains a set disjoint from itself. One consequence is that it denies the existence of a set containing itself (elirrv 9049). A stronger version that works for proper classes is proved as zfregs 9163. (Contributed by NM, 14-Aug-1993.) |
⊢ (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥))) | ||
Theorem | axreg2 9046* | Axiom of Regularity expressed more compactly. (Contributed by NM, 14-Aug-2003.) |
⊢ (𝑥 ∈ 𝑦 → ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦))) | ||
Theorem | zfregcl 9047* | The Axiom of Regularity with class variables. (Contributed by NM, 5-Aug-1994.) Replace sethood hypothesis with sethood antecedent. (Revised by BJ, 27-Apr-2021.) |
⊢ (𝐴 ∈ 𝑉 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴)) | ||
Theorem | zfreg 9048* | The Axiom of Regularity using abbreviations. Axiom 6 of [TakeutiZaring] p. 21. This is called the "weak form". Axiom Reg of [BellMachover] p. 480. There is also a "strong form", not requiring that 𝐴 be a set, that can be proved with more difficulty (see zfregs 9163). (Contributed by NM, 26-Nov-1995.) Replace sethood hypothesis with sethood antecedent. (Revised by BJ, 27-Apr-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅) | ||
Theorem | elirrv 9049 | 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 9057 and efrirr 5530, but this proof is direct from the Axiom of Regularity.) (Contributed by NM, 19-Aug-1993.) |
⊢ ¬ 𝑥 ∈ 𝑥 | ||
Theorem | elirr 9050 | 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 | elneq 9051 | A class is not equal to any of its elements. (Contributed by AV, 14-Jun-2022.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ≠ 𝐵) | ||
Theorem | nelaneq 9052 | A class is not an element of and equal to a class at the same time. Variant of elneq 9051 analogously to elnotel 9062 and en2lp 9058. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022.) |
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐴 = 𝐵) | ||
Theorem | epinid0 9053 | The membership (epsilon) relation and the identity relation are disjoint. Variable-free version of nelaneq 9052. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022.) |
⊢ ( E ∩ I ) = ∅ | ||
Theorem | sucprcreg 9054 | 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 9055 | 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 9056 | Alternate proof of ru 3770, simplified using (indirectly) the Axiom of Regularity ax-reg 9045. (Contributed by Alan Sare, 4-Oct-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} ∉ V | ||
Theorem | zfregfr 9057 | The membership relation is well-founded on any class. (Contributed by NM, 26-Nov-1995.) |
⊢ E Fr 𝐴 | ||
Theorem | en2lp 9058 | 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 | elnanel 9059 | Two classes are not elements of each other simultaneously. This is just a rewriting of en2lp 9058 and serves as an example in the context of Godel codes, see elnanelprv 32574. (Contributed by AV, 5-Nov-2023.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝐵 ⊼ 𝐵 ∈ 𝐴) | ||
Theorem | cnvepnep 9060 | The membership (epsilon) relation and its converse are disjoint, i.e., E is an asymmetric relation. Variable-free version of en2lp 9058. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 19-Jun-2022.) |
⊢ (◡ E ∩ E ) = ∅ | ||
Theorem | epnsym 9061 | The membership (epsilon) relation is not symmetric. (Contributed by AV, 18-Jun-2022.) |
⊢ ◡ E ≠ E | ||
Theorem | elnotel 9062 | A class cannot be an element of one of its elements. (Contributed by AV, 14-Jun-2022.) |
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ 𝐴) | ||
Theorem | elnel 9063 | A class cannot be an element of one of its elements. (Contributed by AV, 14-Jun-2022.) |
⊢ (𝐴 ∈ 𝐵 → 𝐵 ∉ 𝐴) | ||
Theorem | en3lplem1 9064* | Lemma for en3lp 9066. (Contributed by Alan Sare, 28-Oct-2011.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 = 𝐴 → (𝑥 ∩ {𝐴, 𝐵, 𝐶}) ≠ ∅)) | ||
Theorem | en3lplem2 9065* | Lemma for en3lp 9066. (Contributed by Alan Sare, 28-Oct-2011.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 ∈ {𝐴, 𝐵, 𝐶} → (𝑥 ∩ {𝐴, 𝐵, 𝐶}) ≠ ∅)) | ||
Theorem | en3lp 9066 | No class has 3-cycle membership loops. This proof was automatically generated from the virtual deduction proof en3lpVD 41059 using a translation program. (Contributed by Alan Sare, 24-Oct-2011.) |
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) | ||
Theorem | preleqg 9067 | Equality of two unordered pairs when one member of each pair contains the other member. Closed form of preleq 9068. (Contributed by AV, 15-Jun-2022.) |
⊢ (((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐷) ∧ {𝐴, 𝐵} = {𝐶, 𝐷}) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | preleq 9068 | Equality of two unordered pairs when one member of each pair contains the other member. (Contributed by NM, 16-Oct-1996.) (Revised by AV, 15-Jun-2022.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (((𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷) ∧ {𝐴, 𝐵} = {𝐶, 𝐷}) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | preleqALT 9069 | Alternate proof of preleq 9068, not based on preleqg 9067: Equality of two unordered pairs when one member of each pair contains the other member. (Contributed by NM, 16-Oct-1996.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (((𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷) ∧ {𝐴, 𝐵} = {𝐶, 𝐷}) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | opthreg 9070 | Theorem for alternate representation of ordered pairs, requiring the Axiom of Regularity ax-reg 9045 (via the preleq 9068 step). See df-op 4566 for a description of other ordered pair representations. Exercise 34 of [Enderton] p. 207. (Contributed by NM, 16-Oct-1996.) (Proof shortened by AV, 15-Jun-2022.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ ({𝐴, {𝐴, 𝐵}} = {𝐶, {𝐶, 𝐷}} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | suc11reg 9071 | 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 9072* | Assuming ax-reg 9045, an ordinal is a transitive class on which inclusion satisfies trichotomy. (Contributed by Scott Fenton, 27-Oct-2010.) |
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))) | ||
Theorem | inf0 9073* | 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 9090. (Contributed by NM, 15-Oct-1996.) |
⊢ ω ∈ V ⇒ ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))) | ||
Theorem | inf1 9074 | Variation of Axiom of Infinity (using zfinf 9091 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 9075* | Variation of Axiom of Infinity. There exists a nonempty set that is a subset of its union (using zfinf 9091 as a hypothesis). Abbreviated version of the Axiom of Infinity in [FreydScedrov] p. 283. (Contributed by NM, 28-Oct-1996.) |
⊢ ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))) ⇒ ⊢ ∃𝑥(𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) | ||
Theorem | inf3lema 9076* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9087 for detailed description. (Contributed by NM, 28-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ (𝐺‘𝐵) ↔ (𝐴 ∈ 𝑥 ∧ (𝐴 ∩ 𝑥) ⊆ 𝐵)) | ||
Theorem | inf3lemb 9077* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9087 for detailed description. (Contributed by NM, 28-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹‘∅) = ∅ | ||
Theorem | inf3lemc 9078* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9087 for detailed description. (Contributed by NM, 28-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ ω → (𝐹‘suc 𝐴) = (𝐺‘(𝐹‘𝐴))) | ||
Theorem | inf3lemd 9079* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9087 for detailed description. (Contributed by NM, 28-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ ω → (𝐹‘𝐴) ⊆ 𝑥) | ||
Theorem | inf3lem1 9080* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9087 for detailed description. (Contributed by NM, 28-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ ω → (𝐹‘𝐴) ⊆ (𝐹‘suc 𝐴)) | ||
Theorem | inf3lem2 9081* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9087 for detailed description. (Contributed by NM, 28-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ≠ 𝑥)) | ||
Theorem | inf3lem3 9082* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9087 for detailed description. In the proof, we invoke the Axiom of Regularity in the form of zfreg 9048. (Contributed by NM, 29-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ≠ (𝐹‘suc 𝐴))) | ||
Theorem | inf3lem4 9083* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9087 for detailed description. (Contributed by NM, 29-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ⊊ (𝐹‘suc 𝐴))) | ||
Theorem | inf3lem5 9084* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9087 for detailed description. (Contributed by NM, 29-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → (𝐹‘𝐵) ⊊ (𝐹‘𝐴))) | ||
Theorem | inf3lem6 9085* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9087 for detailed description. (Contributed by NM, 29-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → 𝐹:ω–1-1→𝒫 𝑥) | ||
Theorem | inf3lem7 9086* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9087 for detailed description. In the proof, we invoke the Axiom of Replacement in the form of f1dmex 7649. (Contributed by NM, 29-Oct-1996.) (Proof shortened by Mario Carneiro, 19-Jan-2013.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → ω ∈ V) | ||
Theorem | inf3 9087 |
Our Axiom of Infinity ax-inf 9090 implies the standard Axiom of Infinity.
The hypothesis is a variant of our Axiom of Infinity provided by
inf2 9075, 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 9092 and zfinf2 9094.) The main proof is provided by
inf3lema 9076 through inf3lem7 9086, and this final piece eliminates the
auxiliary hypothesis of inf3lem7 9086. 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 9077.) F_n+1 = {y<X | y^X subset F_n} (See inf3lemc 9078.) 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 9080.) 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 9081.) 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 9082.) 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 9083.) Proof: Lemmas 1 and 3. Lemma 5. F_m proper_subset F_n, m < n. (See inf3lem5 9084.) 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 9085.) 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 9086.) Q.E.D.(Contributed by NM, 29-Oct-1996.) |
⊢ ∃𝑥(𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) ⇒ ⊢ ω ∈ V | ||
Theorem | infeq5i 9088 | Half of infeq5 9089. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ (ω ∈ V → ∃𝑥 𝑥 ⊊ ∪ 𝑥) | ||
Theorem | infeq5 9089 | 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 9095.) 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 9090* |
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 9074 and inf2 9075). More
standard versions, which essentially state that there exists a set
containing all the natural numbers, are shown as zfinf2 9094 and omex 9095 and
are based on the (nontrivial) proof of inf3 9087.
This version has the
advantage that when expanded to primitives, it has fewer symbols than
the standard version ax-inf2 9093. Theorem inf0 9073
shows the reverse
derivation of our axiom from a standard one. Theorem inf5 9097
shows a
very short way to state this axiom.
The standard version of Infinity ax-inf2 9093 requires this axiom along with Regularity ax-reg 9045 for its derivation (as theorem axinf2 9092 below). In order to more easily identify the normal uses of Regularity, we will usually reference ax-inf2 9093 instead of this one. The derivation of this axiom from ax-inf2 9093 is shown by theorem axinf 9096. Proofs should normally use the standard version ax-inf2 9093 instead of this axiom. (New usage is discouraged.) (Contributed by NM, 16-Aug-1993.) |
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))) | ||
Theorem | zfinf 9091* | Axiom of Infinity expressed with the fewest number of different variables. (New usage is discouraged.) (Contributed by NM, 14-Aug-2003.) |
⊢ ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))) | ||
Theorem | axinf2 9092* |
A standard version of Axiom of Infinity, expanded to primitives, derived
from our version of Infinity ax-inf 9090 and Regularity ax-reg 9045.
This theorem should not be referenced in any proof. Instead, use ax-inf2 9093 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 9093* | 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 9094 shows it converted to abbreviations. This axiom was derived as theorem axinf2 9092 above, using our version of Infinity ax-inf 9090 and the Axiom of Regularity ax-reg 9045. We will reference ax-inf2 9093 instead of axinf2 9092 so that the ordinary uses of Regularity can be more easily identified. The reverse derivation of ax-inf 9090 from ax-inf2 9093 is shown by theorem axinf 9096. (Contributed by NM, 3-Nov-1996.) |
⊢ ∃𝑥(∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑧 ∈ 𝑥 ∧ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))))) | ||
Theorem | zfinf2 9094* | A standard version of the Axiom of Infinity, using definitions to abbreviate. Axiom Inf of [BellMachover] p. 472. (See ax-inf2 9093 for the unabbreviated version.) (Contributed by NM, 30-Aug-1993.) |
⊢ ∃𝑥(∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) | ||
Theorem | omex 9095 |
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 9073.
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 7579 and Fin = V (the universe of all sets) by fineqv 8722. 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 7589 through peano5 7593 (which many textbooks prove more easily assuming Infinity). (Contributed by NM, 6-Aug-1994.) |
⊢ ω ∈ V | ||
Theorem | axinf 9096* | The first version of the Axiom of Infinity ax-inf 9090 proved from the second version ax-inf2 9093. Note that we didn't use ax-reg 9045, unlike the other direction axinf2 9092. (Contributed by NM, 24-Apr-2009.) |
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))) | ||
Theorem | inf5 9097 | The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (see theorem infeq5 9089). 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 9098 | Omega is an ordinal number. (Contributed by NM, 10-May-1998.) (Revised by Mario Carneiro, 30-Jan-2013.) |
⊢ ω ∈ On | ||
Theorem | dfom3 9099* | The class of natural numbers ω can be defined as the intersection of all inductive sets (which is the smallest inductive set, since inductive sets are closed under intersection), 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 9100* | A simplification of elom 7571 assuming the Axiom of Infinity. (Contributed by NM, 30-May-2003.) |
⊢ (𝐴 ∈ ω ↔ ∀𝑥(Lim 𝑥 → 𝐴 ∈ 𝑥)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |