Home | Metamath
Proof Explorer Theorem List (p. 91 of 450) | < 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-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | oiexg 9001 | The order isomorphism on a set is a set. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ 𝐹 = OrdIso(𝑅, 𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹 ∈ V) | ||
Theorem | oion 9002 | The order type of the well-order 𝑅 on 𝐴 is an ordinal. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 23-May-2015.) |
⊢ 𝐹 = OrdIso(𝑅, 𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → dom 𝐹 ∈ On) | ||
Theorem | oiiso 9003 | The order isomorphism of the well-order 𝑅 on 𝐴 is an isomorphism. (Contributed by Mario Carneiro, 23-May-2015.) |
⊢ 𝐹 = OrdIso(𝑅, 𝐴) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴)) | ||
Theorem | oien 9004 | The order type of a well-ordered set is equinumerous to the set. (Contributed by Mario Carneiro, 23-May-2015.) |
⊢ 𝐹 = OrdIso(𝑅, 𝐴) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴) → dom 𝐹 ≈ 𝐴) | ||
Theorem | oieu 9005 | Uniqueness of the unique ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
⊢ 𝐹 = OrdIso(𝑅, 𝐴) ⇒ ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ((Ord 𝐵 ∧ 𝐺 Isom E , 𝑅 (𝐵, 𝐴)) ↔ (𝐵 = dom 𝐹 ∧ 𝐺 = 𝐹))) | ||
Theorem | oismo 9006 | When 𝐴 is a subclass of On, 𝐹 is a strictly monotone ordinal functions, and it is also complete (it is an isomorphism onto all of 𝐴). The proof avoids ax-rep 5192 (the second statement is trivial under ax-rep 5192). (Contributed by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝐹 = OrdIso( E , 𝐴) ⇒ ⊢ (𝐴 ⊆ On → (Smo 𝐹 ∧ ran 𝐹 = 𝐴)) | ||
Theorem | oiid 9007 | The order type of an ordinal under the ∈ order is itself, and the order isomorphism is the identity function. (Contributed by Mario Carneiro, 26-Jun-2015.) |
⊢ (Ord 𝐴 → OrdIso( E , 𝐴) = ( I ↾ 𝐴)) | ||
Theorem | hartogslem1 9008* | Lemma for hartogs 9010. (Contributed by Mario Carneiro, 14-Jan-2013.) (Revised by Mario Carneiro, 15-May-2015.) |
⊢ 𝐹 = {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} & ⊢ 𝑅 = {〈𝑠, 𝑡〉 ∣ ∃𝑤 ∈ 𝑦 ∃𝑧 ∈ 𝑦 ((𝑠 = (𝑓‘𝑤) ∧ 𝑡 = (𝑓‘𝑧)) ∧ 𝑤 E 𝑧)} ⇒ ⊢ (dom 𝐹 ⊆ 𝒫 (𝐴 × 𝐴) ∧ Fun 𝐹 ∧ (𝐴 ∈ 𝑉 → ran 𝐹 = {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴})) | ||
Theorem | hartogslem2 9009* | Lemma for hartogs 9010. (Contributed by Mario Carneiro, 14-Jan-2013.) |
⊢ 𝐹 = {〈𝑟, 𝑦〉 ∣ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))} & ⊢ 𝑅 = {〈𝑠, 𝑡〉 ∣ ∃𝑤 ∈ 𝑦 ∃𝑧 ∈ 𝑦 ((𝑠 = (𝑓‘𝑤) ∧ 𝑡 = (𝑓‘𝑧)) ∧ 𝑤 E 𝑧)} ⇒ ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ V) | ||
Theorem | hartogs 9010* | Given any set, the Hartogs number of the set is the least ordinal not dominated by that set. This theorem proves that there is always an ordinal which satisfies this. (This theorem can be proven trivially using the AC - see theorem ondomon 9987- but this proof works in ZF.) (Contributed by Jeff Hankins, 22-Oct-2009.) (Revised by Mario Carneiro, 15-May-2015.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ On) | ||
Theorem | wofib 9011 | The only sets which are well-ordered forwards and backwards are finite sets. (Contributed by Mario Carneiro, 30-Jan-2014.) (Revised by Mario Carneiro, 23-May-2015.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) ↔ (𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴)) | ||
Theorem | wemaplem1 9012* | Value of the lexicographic order on a sequence space. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} ⇒ ⊢ ((𝑃 ∈ 𝑉 ∧ 𝑄 ∈ 𝑊) → (𝑃𝑇𝑄 ↔ ∃𝑎 ∈ 𝐴 ((𝑃‘𝑎)𝑆(𝑄‘𝑎) ∧ ∀𝑏 ∈ 𝐴 (𝑏𝑅𝑎 → (𝑃‘𝑏) = (𝑄‘𝑏))))) | ||
Theorem | wemaplem2 9013* | Lemma for wemapso 9017. Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝑃 ∈ (𝐵 ↑m 𝐴)) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m 𝐴)) & ⊢ (𝜑 → 𝑄 ∈ (𝐵 ↑m 𝐴)) & ⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝑆 Po 𝐵) & ⊢ (𝜑 → 𝑎 ∈ 𝐴) & ⊢ (𝜑 → (𝑃‘𝑎)𝑆(𝑋‘𝑎)) & ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑎 → (𝑃‘𝑐) = (𝑋‘𝑐))) & ⊢ (𝜑 → 𝑏 ∈ 𝐴) & ⊢ (𝜑 → (𝑋‘𝑏)𝑆(𝑄‘𝑏)) & ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝑋‘𝑐) = (𝑄‘𝑐))) ⇒ ⊢ (𝜑 → 𝑃𝑇𝑄) | ||
Theorem | wemaplem3 9014* | Lemma for wemapso 9017. Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝑃 ∈ (𝐵 ↑m 𝐴)) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m 𝐴)) & ⊢ (𝜑 → 𝑄 ∈ (𝐵 ↑m 𝐴)) & ⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝑆 Po 𝐵) & ⊢ (𝜑 → 𝑃𝑇𝑋) & ⊢ (𝜑 → 𝑋𝑇𝑄) ⇒ ⊢ (𝜑 → 𝑃𝑇𝑄) | ||
Theorem | wemappo 9015* |
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 9016* | Lemma for wemapso 9017. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ 𝑈 ⊆ (𝐵 ↑m 𝐴) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝑆 Or 𝐵) & ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐) ⇒ ⊢ (𝜑 → 𝑇 Or 𝑈) | ||
Theorem | wemapso 9017* | 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 9018* | Lemma for wemapso2 9019. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 1-Jul-2019.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} & ⊢ 𝑈 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍} ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) → 𝑇 Or 𝑈) | ||
Theorem | wemapso2 9019* | An alternative to having a well-order on 𝑅 in wemapso 9017 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 9020* | The alternate definition of the cardinal of a set given in cardval2 9422 always gives a set, and indeed an ordinal. (Contributed by Mario Carneiro, 14-Jan-2013.) |
⊢ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ On | ||
Theorem | card2inf 9021* | The alternate definition of the cardinal of a set given in cardval2 9422 has the curious property that for non-numerable sets (for which ndmfv 6702 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 9022 | Class symbol for the Hartogs/cardinal successor function. |
class har | ||
Syntax | cwdom 9023 | Class symbol for the weak dominance relation. |
class ≼* | ||
Definition | df-har 9024* |
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 9371. 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 9025* | 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 9946), this coincides with the 1-1 definition df-dom 8513; 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/ 8513. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ ≼* = {〈𝑥, 𝑦〉 ∣ (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑥)} | ||
Theorem | harf 9026 | Functionality of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ har:V⟶On | ||
Theorem | harcl 9027 | Closure of the Hartogs function in the ordinals. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ (har‘𝑋) ∈ On | ||
Theorem | harval 9028* | Function value of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ (𝑋 ∈ 𝑉 → (har‘𝑋) = {𝑦 ∈ On ∣ 𝑦 ≼ 𝑋}) | ||
Theorem | elharval 9029 | 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 9030 | 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 9031 | Weak ordering property of the Hartogs function. (Contributed by Stefan O'Rear, 14-Feb-2015.) |
⊢ (𝑋 ≼ 𝑌 → (har‘𝑋) ⊆ (har‘𝑌)) | ||
Theorem | relwdom 9032 | Weak dominance is a relation. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ Rel ≼* | ||
Theorem | brwdom 9033* | Property of weak dominance (definitional form). (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ (𝑌 ∈ 𝑉 → (𝑋 ≼* 𝑌 ↔ (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋))) | ||
Theorem | brwdomi 9034* | Property of weak dominance, forward direction only. (Contributed by Mario Carneiro, 5-May-2015.) |
⊢ (𝑋 ≼* 𝑌 → (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋)) | ||
Theorem | brwdomn0 9035* | Weak dominance over nonempty sets. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ (𝑋 ≠ ∅ → (𝑋 ≼* 𝑌 ↔ ∃𝑧 𝑧:𝑌–onto→𝑋)) | ||
Theorem | 0wdom 9036 | Any set weakly dominates the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ (𝑋 ∈ 𝑉 → ∅ ≼* 𝑋) | ||
Theorem | fowdom 9037 | An onto function implies weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝑌–onto→𝑋) → 𝑋 ≼* 𝑌) | ||
Theorem | wdomref 9038 | Reflexivity of weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ (𝑋 ∈ 𝑉 → 𝑋 ≼* 𝑋) | ||
Theorem | brwdom2 9039* | 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 9040 | Weak dominance is implied by dominance in the usual sense. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ (𝑋 ≼ 𝑌 → 𝑋 ≼* 𝑌) | ||
Theorem | wdomtr 9041 | Transitivity of weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ ((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) → 𝑋 ≼* 𝑍) | ||
Theorem | wdomen1 9042 | Equality-like theorem for equinumerosity and weak dominance. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≼* 𝐶 ↔ 𝐵 ≼* 𝐶)) | ||
Theorem | wdomen2 9043 | Equality-like theorem for equinumerosity and weak dominance. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≼* 𝐴 ↔ 𝐶 ≼* 𝐵)) | ||
Theorem | wdompwdom 9044 | 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 9045 | Cantor's Theorem, stated using weak dominance (this is actually a stronger statement than canth2 8672, equivalent to canth 7113). (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ ¬ 𝒫 𝐴 ≼* 𝐴 | ||
Theorem | wdom2d 9046* | Deduce weak dominance from an implicit onto function (stated in a way which avoids ax-rep 5192). (Contributed by Stefan O'Rear, 13-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 𝑥 = 𝑋) ⇒ ⊢ (𝜑 → 𝐴 ≼* 𝐵) | ||
Theorem | wdomd 9047* | Deduce weak dominance from an implicit onto function. (Contributed by Stefan O'Rear, 13-Feb-2015.) |
⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 𝑥 = 𝑋) ⇒ ⊢ (𝜑 → 𝐴 ≼* 𝐵) | ||
Theorem | brwdom3 9048* | Condition for weak dominance with a condition reminiscent of wdomd 9047. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → (𝑋 ≼* 𝑌 ↔ ∃𝑓∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝑥 = (𝑓‘𝑦))) | ||
Theorem | brwdom3i 9049* | Weak dominance implies existence of a covering function. (Contributed by Stefan O'Rear, 13-Feb-2015.) |
⊢ (𝑋 ≼* 𝑌 → ∃𝑓∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝑥 = (𝑓‘𝑦)) | ||
Theorem | unwdomg 9050 | Weak dominance of a (disjoint) union. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
⊢ ((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷 ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 ∪ 𝐶) ≼* (𝐵 ∪ 𝐷)) | ||
Theorem | xpwdomg 9051 | Weak dominance of a Cartesian product. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.) |
⊢ ((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷) → (𝐴 × 𝐶) ≼* (𝐵 × 𝐷)) | ||
Theorem | wdomima2g 9052 | A set is weakly dominant over its image under any function. This version of wdomimag 9053 is stated so as to avoid ax-rep 5192. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ 𝑉 ∧ (𝐹 “ 𝐴) ∈ 𝑊) → (𝐹 “ 𝐴) ≼* 𝐴) | ||
Theorem | wdomimag 9053 | 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 9054 | Lemma for unxpwdom 9055. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ ((𝐴 × 𝐴) ≈ (𝐵 ∪ 𝐶) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶)) | ||
Theorem | unxpwdom 9055 | 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 9056 | The Hartogs function is weakly dominated by 𝒫 (𝑋 × 𝑋). This follows from a more precise analysis of the bound used in hartogs 9010 to prove that (har‘𝑋) is a set. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (𝑋 ∈ 𝑉 → (har‘𝑋) ≼* 𝒫 (𝑋 × 𝑋)) | ||
Theorem | ixpiunwdom 9057* | Describe an onto function from the indexed cartesian product to the indexed union. Together with ixpssmapg 8494 this shows that ∪ 𝑥 ∈ 𝐴𝐵 and X𝑥 ∈ 𝐴𝐵 have closely linked cardinalities. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → ∪ 𝑥 ∈ 𝐴 𝐵 ≼* (X𝑥 ∈ 𝐴 𝐵 × 𝐴)) | ||
Axiom | ax-reg 9058* | 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 9061) that every nonempty set contains a set disjoint from itself. One consequence is that it denies the existence of a set containing itself (elirrv 9062). A stronger version that works for proper classes is proved as zfregs 9176. (Contributed by NM, 14-Aug-1993.) |
⊢ (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥))) | ||
Theorem | axreg2 9059* | Axiom of Regularity expressed more compactly. (Contributed by NM, 14-Aug-2003.) |
⊢ (𝑥 ∈ 𝑦 → ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦))) | ||
Theorem | zfregcl 9060* | 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 9061* | 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 9176). (Contributed by NM, 26-Nov-1995.) Replace sethood hypothesis with sethood antecedent. (Revised by BJ, 27-Apr-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅) | ||
Theorem | elirrv 9062 | 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 9070 and efrirr 5538, but this proof is direct from the Axiom of Regularity.) (Contributed by NM, 19-Aug-1993.) |
⊢ ¬ 𝑥 ∈ 𝑥 | ||
Theorem | elirr 9063 | 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 9064 | A class is not equal to any of its elements. (Contributed by AV, 14-Jun-2022.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ≠ 𝐵) | ||
Theorem | nelaneq 9065 | A class is not an element of and equal to a class at the same time. Variant of elneq 9064 analogously to elnotel 9075 and en2lp 9071. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022.) |
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐴 = 𝐵) | ||
Theorem | epinid0 9066 | The membership (epsilon) relation and the identity relation are disjoint. Variable-free version of nelaneq 9065. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022.) |
⊢ ( E ∩ I ) = ∅ | ||
Theorem | sucprcreg 9067 | 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 9068 | 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 9069 | Alternate proof of ru 3773, simplified using (indirectly) the Axiom of Regularity ax-reg 9058. (Contributed by Alan Sare, 4-Oct-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} ∉ V | ||
Theorem | zfregfr 9070 | The membership relation is well-founded on any class. (Contributed by NM, 26-Nov-1995.) |
⊢ E Fr 𝐴 | ||
Theorem | en2lp 9071 | 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 9072 | Two classes are not elements of each other simultaneously. This is just a rewriting of en2lp 9071 and serves as an example in the context of Godel codes, see elnanelprv 32678. (Contributed by AV, 5-Nov-2023.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝐵 ⊼ 𝐵 ∈ 𝐴) | ||
Theorem | cnvepnep 9073 | The membership (epsilon) relation and its converse are disjoint, i.e., E is an asymmetric relation. Variable-free version of en2lp 9071. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 19-Jun-2022.) |
⊢ (◡ E ∩ E ) = ∅ | ||
Theorem | epnsym 9074 | The membership (epsilon) relation is not symmetric. (Contributed by AV, 18-Jun-2022.) |
⊢ ◡ E ≠ E | ||
Theorem | elnotel 9075 | A class cannot be an element of one of its elements. (Contributed by AV, 14-Jun-2022.) |
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ 𝐴) | ||
Theorem | elnel 9076 | A class cannot be an element of one of its elements. (Contributed by AV, 14-Jun-2022.) |
⊢ (𝐴 ∈ 𝐵 → 𝐵 ∉ 𝐴) | ||
Theorem | en3lplem1 9077* | Lemma for en3lp 9079. (Contributed by Alan Sare, 28-Oct-2011.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 = 𝐴 → (𝑥 ∩ {𝐴, 𝐵, 𝐶}) ≠ ∅)) | ||
Theorem | en3lplem2 9078* | Lemma for en3lp 9079. (Contributed by Alan Sare, 28-Oct-2011.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 ∈ {𝐴, 𝐵, 𝐶} → (𝑥 ∩ {𝐴, 𝐵, 𝐶}) ≠ ∅)) | ||
Theorem | en3lp 9079 | No class has 3-cycle membership loops. This proof was automatically generated from the virtual deduction proof en3lpVD 41186 using a translation program. (Contributed by Alan Sare, 24-Oct-2011.) |
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) | ||
Theorem | preleqg 9080 | Equality of two unordered pairs when one member of each pair contains the other member. Closed form of preleq 9081. (Contributed by AV, 15-Jun-2022.) |
⊢ (((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐷) ∧ {𝐴, 𝐵} = {𝐶, 𝐷}) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | preleq 9081 | 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 9082 | Alternate proof of preleq 9081, not based on preleqg 9080: 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 9083 | Theorem for alternate representation of ordered pairs, requiring the Axiom of Regularity ax-reg 9058 (via the preleq 9081 step). See df-op 4576 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 9084 | 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 9085* | Assuming ax-reg 9058, an ordinal is a transitive class on which inclusion satisfies trichotomy. (Contributed by Scott Fenton, 27-Oct-2010.) |
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))) | ||
Theorem | inf0 9086* | 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 9103. (Contributed by NM, 15-Oct-1996.) |
⊢ ω ∈ V ⇒ ⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))) | ||
Theorem | inf1 9087 | Variation of Axiom of Infinity (using zfinf 9104 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 9088* | Variation of Axiom of Infinity. There exists a nonempty set that is a subset of its union (using zfinf 9104 as a hypothesis). Abbreviated version of the Axiom of Infinity in [FreydScedrov] p. 283. (Contributed by NM, 28-Oct-1996.) |
⊢ ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))) ⇒ ⊢ ∃𝑥(𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) | ||
Theorem | inf3lema 9089* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9100 for detailed description. (Contributed by NM, 28-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ (𝐺‘𝐵) ↔ (𝐴 ∈ 𝑥 ∧ (𝐴 ∩ 𝑥) ⊆ 𝐵)) | ||
Theorem | inf3lemb 9090* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9100 for detailed description. (Contributed by NM, 28-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹‘∅) = ∅ | ||
Theorem | inf3lemc 9091* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9100 for detailed description. (Contributed by NM, 28-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ ω → (𝐹‘suc 𝐴) = (𝐺‘(𝐹‘𝐴))) | ||
Theorem | inf3lemd 9092* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9100 for detailed description. (Contributed by NM, 28-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ ω → (𝐹‘𝐴) ⊆ 𝑥) | ||
Theorem | inf3lem1 9093* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9100 for detailed description. (Contributed by NM, 28-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ ω → (𝐹‘𝐴) ⊆ (𝐹‘suc 𝐴)) | ||
Theorem | inf3lem2 9094* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9100 for detailed description. (Contributed by NM, 28-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ≠ 𝑥)) | ||
Theorem | inf3lem3 9095* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9100 for detailed description. In the proof, we invoke the Axiom of Regularity in the form of zfreg 9061. (Contributed by NM, 29-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ≠ (𝐹‘suc 𝐴))) | ||
Theorem | inf3lem4 9096* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9100 for detailed description. (Contributed by NM, 29-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ⊊ (𝐹‘suc 𝐴))) | ||
Theorem | inf3lem5 9097* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9100 for detailed description. (Contributed by NM, 29-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → (𝐹‘𝐵) ⊊ (𝐹‘𝐴))) | ||
Theorem | inf3lem6 9098* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9100 for detailed description. (Contributed by NM, 29-Oct-1996.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → 𝐹:ω–1-1→𝒫 𝑥) | ||
Theorem | inf3lem7 9099* | Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9100 for detailed description. In the proof, we invoke the Axiom of Replacement in the form of f1dmex 7660. (Contributed by NM, 29-Oct-1996.) (Proof shortened by Mario Carneiro, 19-Jan-2013.) |
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦}) & ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → ω ∈ V) | ||
Theorem | inf3 9100 |
Our Axiom of Infinity ax-inf 9103 implies the standard Axiom of Infinity.
The hypothesis is a variant of our Axiom of Infinity provided by
inf2 9088, 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 9105 and zfinf2 9107.) The main proof is provided by
inf3lema 9089 through inf3lem7 9099, and this final piece eliminates the
auxiliary hypothesis of inf3lem7 9099. 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 9090.) F_n+1 = {y<X | y^X subset F_n} (See inf3lemc 9091.) 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 9093.) 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 9094.) 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 9095.) 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 9096.) Proof: Lemmas 1 and 3. Lemma 5. F_m proper_subset F_n, m < n. (See inf3lem5 9097.) 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 9098.) 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 9099.) Q.E.D.(Contributed by NM, 29-Oct-1996.) |
⊢ ∃𝑥(𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) ⇒ ⊢ ω ∈ V |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |