Home | Metamath
Proof Explorer Theorem List (p. 95 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-28694) |
Hilbert Space Explorer
(28695-30217) |
Users' Mathboxes
(30218-44905) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cardsdomelir 9401 | A cardinal strictly dominates its members. Equivalent to Proposition 10.37 of [TakeutiZaring] p. 93. This is half of the assertion cardsdomel 9402 and can be proven without the AC. (Contributed by Mario Carneiro, 15-Jan-2013.) |
⊢ (𝐴 ∈ (card‘𝐵) → 𝐴 ≺ 𝐵) | ||
Theorem | cardsdomel 9402 | A cardinal strictly dominates its members. Equivalent to Proposition 10.37 of [TakeutiZaring] p. 93. (Contributed by Mario Carneiro, 15-Jan-2013.) (Revised by Mario Carneiro, 4-Jun-2015.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ dom card) → (𝐴 ≺ 𝐵 ↔ 𝐴 ∈ (card‘𝐵))) | ||
Theorem | iscard 9403* | Two ways to express the property of being a cardinal number. (Contributed by Mario Carneiro, 15-Jan-2013.) |
⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 𝑥 ≺ 𝐴)) | ||
Theorem | iscard2 9404* | Two ways to express the property of being a cardinal number. Definition 8 of [Suppes] p. 225. (Contributed by Mario Carneiro, 15-Jan-2013.) |
⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ On (𝐴 ≈ 𝑥 → 𝐴 ⊆ 𝑥))) | ||
Theorem | carddom2 9405 | Two numerable sets have the dominance relationship iff their cardinalities have the subset relationship. See also carddom 9975, which uses AC. (Contributed by Mario Carneiro, 11-Jan-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ 𝐴 ≼ 𝐵)) | ||
Theorem | harcard 9406 | The class of ordinal numbers dominated by a set is a cardinal number. Theorem 59 of [Suppes] p. 228. (Contributed by Mario Carneiro, 20-Jan-2013.) (Revised by Mario Carneiro, 15-May-2015.) |
⊢ (card‘(har‘𝐴)) = (har‘𝐴) | ||
Theorem | cardprclem 9407* | Lemma for cardprc 9408. (Contributed by Mario Carneiro, 22-Jan-2013.) (Revised by Mario Carneiro, 15-May-2015.) |
⊢ 𝐴 = {𝑥 ∣ (card‘𝑥) = 𝑥} ⇒ ⊢ ¬ 𝐴 ∈ V | ||
Theorem | cardprc 9408 | The class of all cardinal numbers is not a set (i.e. is a proper class). Theorem 19.8 of [Eisenberg] p. 310. In this proof (which does not use AC), we cannot use Cantor's construction canth3 9982 to ensure that there is always a cardinal larger than a given cardinal, but we can use Hartogs' construction hartogs 9007 to construct (effectively) (ℵ‘suc 𝐴) from (ℵ‘𝐴), which achieves the same thing. (Contributed by Mario Carneiro, 22-Jan-2013.) |
⊢ {𝑥 ∣ (card‘𝑥) = 𝑥} ∉ V | ||
Theorem | carduni 9409* | The union of a set of cardinals is a cardinal. Theorem 18.14 of [Monk1] p. 133. (Contributed by Mario Carneiro, 20-Jan-2013.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (card‘𝑥) = 𝑥 → (card‘∪ 𝐴) = ∪ 𝐴)) | ||
Theorem | cardiun 9410* | The indexed union of a set of cardinals is a cardinal. (Contributed by NM, 3-Nov-2003.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (card‘𝐵) = 𝐵 → (card‘∪ 𝑥 ∈ 𝐴 𝐵) = ∪ 𝑥 ∈ 𝐴 𝐵)) | ||
Theorem | cardennn 9411 | If 𝐴 is equinumerous to a natural number, then that number is its cardinal. (Contributed by Mario Carneiro, 11-Jan-2013.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ ω) → (card‘𝐴) = 𝐵) | ||
Theorem | cardsucinf 9412 | The cardinality of the successor of an infinite ordinal. (Contributed by Mario Carneiro, 11-Jan-2013.) |
⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (card‘suc 𝐴) = (card‘𝐴)) | ||
Theorem | cardsucnn 9413 | The cardinality of the successor of a finite ordinal (natural number). This theorem does not hold for infinite ordinals; see cardsucinf 9412. (Contributed by NM, 7-Nov-2008.) |
⊢ (𝐴 ∈ ω → (card‘suc 𝐴) = suc (card‘𝐴)) | ||
Theorem | cardom 9414 | The set of natural numbers is a cardinal number. Theorem 18.11 of [Monk1] p. 133. (Contributed by NM, 28-Oct-2003.) |
⊢ (card‘ω) = ω | ||
Theorem | carden2 9415 | Two numerable sets are equinumerous iff their cardinal numbers are equal. Unlike carden 9972, the Axiom of Choice is not required. (Contributed by Mario Carneiro, 22-Sep-2013.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((card‘𝐴) = (card‘𝐵) ↔ 𝐴 ≈ 𝐵)) | ||
Theorem | cardsdom2 9416 | A numerable set is strictly dominated by another iff their cardinalities are strictly ordered. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((card‘𝐴) ∈ (card‘𝐵) ↔ 𝐴 ≺ 𝐵)) | ||
Theorem | domtri2 9417 | Trichotomy of dominance for numerable sets (does not use AC). (Contributed by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴)) | ||
Theorem | nnsdomel 9418 | Strict dominance and elementhood are the same for finite ordinals. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ 𝐴 ≺ 𝐵)) | ||
Theorem | cardval2 9419* | An alternate version of the value of the cardinal number of a set. Compare cardval 9967. This theorem could be used to give a simpler definition of card in place of df-card 9367. It apparently does not occur in the literature. (Contributed by NM, 7-Nov-2003.) |
⊢ (𝐴 ∈ dom card → (card‘𝐴) = {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴}) | ||
Theorem | isinffi 9420* | An infinite set contains subsets equinumerous to every finite set. Extension of isinf 8730 from finite ordinals to all finite sets. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
⊢ ((¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐵–1-1→𝐴) | ||
Theorem | fidomtri 9421 | Trichotomy of dominance without AC when one set is finite. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 27-Apr-2015.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴)) | ||
Theorem | fidomtri2 9422 | Trichotomy of dominance without AC when one set is finite. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 7-May-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴)) | ||
Theorem | harsdom 9423 | The Hartogs number of a well-orderable set strictly dominates the set. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (𝐴 ∈ dom card → 𝐴 ≺ (har‘𝐴)) | ||
Theorem | onsdom 9424* | Any well-orderable set is strictly dominated by an ordinal number. (Contributed by Jeff Hankins, 22-Oct-2009.) (Proof shortened by Mario Carneiro, 15-May-2015.) |
⊢ (𝐴 ∈ dom card → ∃𝑥 ∈ On 𝐴 ≺ 𝑥) | ||
Theorem | harval2 9425* | An alternate expression for the Hartogs number of a well-orderable set. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (𝐴 ∈ dom card → (har‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝐴 ≺ 𝑥}) | ||
Theorem | cardmin2 9426* | The smallest ordinal that strictly dominates a set is a cardinal, if it exists. (Contributed by Mario Carneiro, 2-Feb-2013.) |
⊢ (∃𝑥 ∈ On 𝐴 ≺ 𝑥 ↔ (card‘∩ {𝑥 ∈ On ∣ 𝐴 ≺ 𝑥}) = ∩ {𝑥 ∈ On ∣ 𝐴 ≺ 𝑥}) | ||
Theorem | pm54.43lem 9427* | In Theorem *54.43 of [WhiteheadRussell] p. 360, the number 1 is defined as the collection of all sets with cardinality 1 (i.e. all singletons; see card1 9396), so that their 𝐴 ∈ 1 means, in our notation, 𝐴 ∈ {𝑥 ∣ (card‘𝑥) = 1o}. Here we show that this is equivalent to 𝐴 ≈ 1o so that we can use the latter more convenient notation in pm54.43 9428. (Contributed by NM, 4-Nov-2013.) |
⊢ (𝐴 ≈ 1o ↔ 𝐴 ∈ {𝑥 ∣ (card‘𝑥) = 1o}) | ||
Theorem | pm54.43 9428 |
Theorem *54.43 of [WhiteheadRussell]
p. 360. "From this proposition it
will follow, when arithmetical addition has been defined, that
1+1=2."
See http://en.wikipedia.org/wiki/Principia_Mathematica#Quotations.
This theorem states that two sets of cardinality 1 are disjoint iff
their union has cardinality 2.
Whitehead and Russell define 1 as the collection of all sets with cardinality 1 (i.e. all singletons; see card1 9396), so that their 𝐴 ∈ 1 means, in our notation, 𝐴 ∈ {𝑥 ∣ (card‘𝑥) = 1o} which is the same as 𝐴 ≈ 1o by pm54.43lem 9427. We do not have several of their earlier lemmas available (which would otherwise be unused by our different approach to arithmetic), so our proof is longer. (It is also longer because we must show every detail.) Theorem dju1p1e2 9598 shows the derivation of 1+1=2 for cardinal numbers from this theorem. (Contributed by NM, 4-Apr-2007.) |
⊢ ((𝐴 ≈ 1o ∧ 𝐵 ≈ 1o) → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐴 ∪ 𝐵) ≈ 2o)) | ||
Theorem | pr2nelem 9429 | Lemma for pr2ne 9430. (Contributed by FL, 17-Aug-2008.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈ 2o) | ||
Theorem | pr2ne 9430 | If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2o ↔ 𝐴 ≠ 𝐵)) | ||
Theorem | prdom2 9431 | An unordered pair has at most two elements. (Contributed by FL, 22-Feb-2011.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴, 𝐵} ≼ 2o) | ||
Theorem | en2eqpr 9432 | Building a set with two elements. (Contributed by FL, 11-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
⊢ ((𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 ≠ 𝐵 → 𝐶 = {𝐴, 𝐵})) | ||
Theorem | en2eleq 9433 | Express a set of pair cardinality as the unordered pair of a given element and the other element. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → 𝑃 = {𝑋, ∪ (𝑃 ∖ {𝑋})}) | ||
Theorem | en2other2 9434 | Taking the other element twice in a pair gets back to the original element. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → ∪ (𝑃 ∖ {∪ (𝑃 ∖ {𝑋})}) = 𝑋) | ||
Theorem | dif1card 9435 | The cardinality of a nonempty finite set is one greater than the cardinality of the set with one element removed. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 2-Feb-2013.) |
⊢ ((𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴) → (card‘𝐴) = suc (card‘(𝐴 ∖ {𝑋}))) | ||
Theorem | leweon 9436* | Lexicographical order is a well-ordering of On × On. Proposition 7.56(1) of [TakeutiZaring] p. 54. Note that unlike r0weon 9437, this order is not set-like, as the preimage of 〈1o, ∅〉 is the proper class ({∅} × On). (Contributed by Mario Carneiro, 9-Mar-2013.) |
⊢ 𝐿 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1st ‘𝑥) ∈ (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥) ∈ (2nd ‘𝑦))))} ⇒ ⊢ 𝐿 We (On × On) | ||
Theorem | r0weon 9437* | A set-like well-ordering of the class of ordinal pairs. Proposition 7.58(1) of [TakeutiZaring] p. 54. (Contributed by Mario Carneiro, 7-Mar-2013.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝐿 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1st ‘𝑥) ∈ (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥) ∈ (2nd ‘𝑦))))} & ⊢ 𝑅 = {〈𝑧, 𝑤〉 ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤)))} ⇒ ⊢ (𝑅 We (On × On) ∧ 𝑅 Se (On × On)) | ||
Theorem | infxpenlem 9438* | Lemma for infxpen 9439. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝐿 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1st ‘𝑥) ∈ (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥) ∈ (2nd ‘𝑦))))} & ⊢ 𝑅 = {〈𝑧, 𝑤〉 ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤)))} & ⊢ 𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) & ⊢ (𝜑 ↔ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎))) & ⊢ 𝑀 = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) & ⊢ 𝐽 = OrdIso(𝑄, (𝑎 × 𝑎)) ⇒ ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴) | ||
Theorem | infxpen 9439 | Every infinite ordinal is equinumerous to its Cartesian square. Proposition 10.39 of [TakeutiZaring] p. 94, whose proof we follow closely. The key idea is to show that the relation 𝑅 is a well-ordering of (On × On) with the additional property that 𝑅-initial segments of (𝑥 × 𝑥) (where 𝑥 is a limit ordinal) are of cardinality at most 𝑥. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴) | ||
Theorem | xpomen 9440 | The Cartesian product of omega (the set of ordinal natural numbers) with itself is equinumerous to omega. Exercise 1 of [Enderton] p. 133. (Contributed by NM, 23-Jul-2004.) (Revised by Mario Carneiro, 9-Mar-2013.) |
⊢ (ω × ω) ≈ ω | ||
Theorem | xpct 9441 | The cartesian product of two countable sets is countable. (Contributed by Thierry Arnoux, 24-Sep-2017.) |
⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 × 𝐵) ≼ ω) | ||
Theorem | infxpidm2 9442 | The Cartesian product of an infinite set with itself is idempotent. This theorem provides the basis for infinite cardinal arithmetic. Proposition 10.40 of [TakeutiZaring] p. 95. See also infxpidm 9983. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ ω ≼ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴) | ||
Theorem | infxpenc 9443* | A canonical version of infxpen 9439, by a completely different approach (although it uses infxpen 9439 via xpomen 9440). Using Cantor's normal form, we can show that 𝐴 ↑o 𝐵 respects equinumerosity (oef1o 9160), so that all the steps of (ω↑𝑊) · (ω↑𝑊) ≈ ω↑(2𝑊) ≈ (ω↑2)↑𝑊 ≈ ω↑𝑊 can be verified using bijections to do the ordinal commutations. (The assumption on 𝑁 can be satisfied using cnfcom3c 9168.) (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 7-Jul-2019.) |
⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → ω ⊆ 𝐴) & ⊢ (𝜑 → 𝑊 ∈ (On ∖ 1o)) & ⊢ (𝜑 → 𝐹:(ω ↑o 2o)–1-1-onto→ω) & ⊢ (𝜑 → (𝐹‘∅) = ∅) & ⊢ (𝜑 → 𝑁:𝐴–1-1-onto→(ω ↑o 𝑊)) & ⊢ 𝐾 = (𝑦 ∈ {𝑥 ∈ ((ω ↑o 2o) ↑m 𝑊) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡( I ↾ 𝑊)))) & ⊢ 𝐻 = (((ω CNF 𝑊) ∘ 𝐾) ∘ ◡((ω ↑o 2o) CNF 𝑊)) & ⊢ 𝐿 = (𝑦 ∈ {𝑥 ∈ (ω ↑m (𝑊 ·o 2o)) ∣ 𝑥 finSupp ∅} ↦ (( I ↾ ω) ∘ (𝑦 ∘ ◡(𝑌 ∘ ◡𝑋)))) & ⊢ 𝑋 = (𝑧 ∈ 2o, 𝑤 ∈ 𝑊 ↦ ((𝑊 ·o 𝑧) +o 𝑤)) & ⊢ 𝑌 = (𝑧 ∈ 2o, 𝑤 ∈ 𝑊 ↦ ((2o ·o 𝑤) +o 𝑧)) & ⊢ 𝐽 = (((ω CNF (2o ·o 𝑊)) ∘ 𝐿) ∘ ◡(ω CNF (𝑊 ·o 2o))) & ⊢ 𝑍 = (𝑥 ∈ (ω ↑o 𝑊), 𝑦 ∈ (ω ↑o 𝑊) ↦ (((ω ↑o 𝑊) ·o 𝑥) +o 𝑦)) & ⊢ 𝑇 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝑁‘𝑥), (𝑁‘𝑦)〉) & ⊢ 𝐺 = (◡𝑁 ∘ (((𝐻 ∘ 𝐽) ∘ 𝑍) ∘ 𝑇)) ⇒ ⊢ (𝜑 → 𝐺:(𝐴 × 𝐴)–1-1-onto→𝐴) | ||
Theorem | infxpenc2lem1 9444* | Lemma for infxpenc2 9447. (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) & ⊢ 𝑊 = (◡(𝑥 ∈ (On ∖ 1o) ↦ (ω ↑o 𝑥))‘ran (𝑛‘𝑏)) ⇒ ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → (𝑊 ∈ (On ∖ 1o) ∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑊))) | ||
Theorem | infxpenc2lem2 9445* | Lemma for infxpenc2 9447. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 7-Jul-2019.) |
⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) & ⊢ 𝑊 = (◡(𝑥 ∈ (On ∖ 1o) ↦ (ω ↑o 𝑥))‘ran (𝑛‘𝑏)) & ⊢ (𝜑 → 𝐹:(ω ↑o 2o)–1-1-onto→ω) & ⊢ (𝜑 → (𝐹‘∅) = ∅) & ⊢ 𝐾 = (𝑦 ∈ {𝑥 ∈ ((ω ↑o 2o) ↑m 𝑊) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡( I ↾ 𝑊)))) & ⊢ 𝐻 = (((ω CNF 𝑊) ∘ 𝐾) ∘ ◡((ω ↑o 2o) CNF 𝑊)) & ⊢ 𝐿 = (𝑦 ∈ {𝑥 ∈ (ω ↑m (𝑊 ·o 2o)) ∣ 𝑥 finSupp ∅} ↦ (( I ↾ ω) ∘ (𝑦 ∘ ◡(𝑌 ∘ ◡𝑋)))) & ⊢ 𝑋 = (𝑧 ∈ 2o, 𝑤 ∈ 𝑊 ↦ ((𝑊 ·o 𝑧) +o 𝑤)) & ⊢ 𝑌 = (𝑧 ∈ 2o, 𝑤 ∈ 𝑊 ↦ ((2o ·o 𝑤) +o 𝑧)) & ⊢ 𝐽 = (((ω CNF (2o ·o 𝑊)) ∘ 𝐿) ∘ ◡(ω CNF (𝑊 ·o 2o))) & ⊢ 𝑍 = (𝑥 ∈ (ω ↑o 𝑊), 𝑦 ∈ (ω ↑o 𝑊) ↦ (((ω ↑o 𝑊) ·o 𝑥) +o 𝑦)) & ⊢ 𝑇 = (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ 〈((𝑛‘𝑏)‘𝑥), ((𝑛‘𝑏)‘𝑦)〉) & ⊢ 𝐺 = (◡(𝑛‘𝑏) ∘ (((𝐻 ∘ 𝐽) ∘ 𝑍) ∘ 𝑇)) ⇒ ⊢ (𝜑 → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) | ||
Theorem | infxpenc2lem3 9446* | Lemma for infxpenc2 9447. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 7-Jul-2019.) |
⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) & ⊢ 𝑊 = (◡(𝑥 ∈ (On ∖ 1o) ↦ (ω ↑o 𝑥))‘ran (𝑛‘𝑏)) & ⊢ (𝜑 → 𝐹:(ω ↑o 2o)–1-1-onto→ω) & ⊢ (𝜑 → (𝐹‘∅) = ∅) ⇒ ⊢ (𝜑 → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) | ||
Theorem | infxpenc2 9447* | Existence form of infxpenc 9443. A "uniform" or "canonical" version of infxpen 9439, asserting the existence of a single function 𝑔 that simultaneously demonstrates product idempotence of all ordinals below a given bound. (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ (𝐴 ∈ On → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) | ||
Theorem | iunmapdisj 9448* | The union ∪ 𝑛 ∈ 𝐶(𝐴 ↑m 𝑛) is a disjoint union. (Contributed by Mario Carneiro, 17-May-2015.) (Revised by NM, 16-Jun-2017.) |
⊢ ∃*𝑛 ∈ 𝐶 𝐵 ∈ (𝐴 ↑m 𝑛) | ||
Theorem | fseqenlem1 9449* | Lemma for fseqen 9452. (Contributed by Mario Carneiro, 17-May-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴) & ⊢ 𝐺 = seqω((𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))), {〈∅, 𝐵〉}) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ ω) → (𝐺‘𝐶):(𝐴 ↑m 𝐶)–1-1→𝐴) | ||
Theorem | fseqenlem2 9450* | Lemma for fseqen 9452. (Contributed by Mario Carneiro, 17-May-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴) & ⊢ 𝐺 = seqω((𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))), {〈∅, 𝐵〉}) & ⊢ 𝐾 = (𝑦 ∈ ∪ 𝑘 ∈ ω (𝐴 ↑m 𝑘) ↦ 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉) ⇒ ⊢ (𝜑 → 𝐾:∪ 𝑘 ∈ ω (𝐴 ↑m 𝑘)–1-1→(ω × 𝐴)) | ||
Theorem | fseqdom 9451* | One half of fseqen 9452. (Contributed by Mario Carneiro, 18-Nov-2014.) |
⊢ (𝐴 ∈ 𝑉 → (ω × 𝐴) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) | ||
Theorem | fseqen 9452* | A set that is equinumerous to its Cartesian product is equinumerous to the set of finite sequences on it. (This can be proven more easily using some choice but this proof avoids it.) (Contributed by Mario Carneiro, 18-Nov-2014.) |
⊢ (((𝐴 × 𝐴) ≈ 𝐴 ∧ 𝐴 ≠ ∅) → ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) ≈ (ω × 𝐴)) | ||
Theorem | infpwfidom 9453 | The collection of finite subsets of a set dominates the set. (We use the weaker sethood assumption (𝒫 𝐴 ∩ Fin) ∈ V because this theorem also implies that 𝐴 is a set if 𝒫 𝐴 ∩ Fin is.) (Contributed by Mario Carneiro, 17-May-2015.) |
⊢ ((𝒫 𝐴 ∩ Fin) ∈ V → 𝐴 ≼ (𝒫 𝐴 ∩ Fin)) | ||
Theorem | dfac8alem 9454* | Lemma for dfac8a 9455. If the power set of a set has a choice function, then the set is numerable. (Contributed by NM, 10-Feb-1997.) (Revised by Mario Carneiro, 5-Jan-2013.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐺 = (𝑓 ∈ V ↦ (𝑔‘(𝐴 ∖ ran 𝑓))) ⇒ ⊢ (𝐴 ∈ 𝐶 → (∃𝑔∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) → 𝐴 ∈ dom card)) | ||
Theorem | dfac8a 9455* | Numeration theorem: every set with a choice function on its power set is numerable. With AC, this reduces to the statement that every set is numerable. Similar to Theorem 10.3 of [TakeutiZaring] p. 84. (Contributed by NM, 10-Feb-1997.) (Revised by Mario Carneiro, 5-Jan-2013.) |
⊢ (𝐴 ∈ 𝐵 → (∃ℎ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (ℎ‘𝑦) ∈ 𝑦) → 𝐴 ∈ dom card)) | ||
Theorem | dfac8b 9456* | The well-ordering theorem: every numerable set is well-orderable. (Contributed by Mario Carneiro, 5-Jan-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ∈ dom card → ∃𝑥 𝑥 We 𝐴) | ||
Theorem | dfac8clem 9457* | Lemma for dfac8c 9458. (Contributed by Mario Carneiro, 10-Jan-2013.) |
⊢ 𝐹 = (𝑠 ∈ (𝐴 ∖ {∅}) ↦ (℩𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ¬ 𝑏𝑟𝑎)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (∃𝑟 𝑟 We ∪ 𝐴 → ∃𝑓∀𝑧 ∈ 𝐴 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) | ||
Theorem | dfac8c 9458* | If the union of a set is well-orderable, then the set has a choice function. (Contributed by Mario Carneiro, 5-Jan-2013.) |
⊢ (𝐴 ∈ 𝐵 → (∃𝑟 𝑟 We ∪ 𝐴 → ∃𝑓∀𝑧 ∈ 𝐴 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) | ||
Theorem | ac10ct 9459* | A proof of the well-ordering theorem weth 9916, an Axiom of Choice equivalent, restricted to sets dominated by some ordinal (in particular finite sets and countable sets), proven in ZF without AC. (Contributed by Mario Carneiro, 5-Jan-2013.) |
⊢ (∃𝑦 ∈ On 𝐴 ≼ 𝑦 → ∃𝑥 𝑥 We 𝐴) | ||
Theorem | ween 9460* | A set is numerable iff it can be well-ordered. (Contributed by Mario Carneiro, 5-Jan-2013.) |
⊢ (𝐴 ∈ dom card ↔ ∃𝑟 𝑟 We 𝐴) | ||
Theorem | ac5num 9461* | A version of ac5b 9899 with the choice as a hypothesis. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ ((∪ 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴) → ∃𝑓(𝑓:𝐴⟶∪ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥)) | ||
Theorem | ondomen 9462 | If a set is dominated by an ordinal, then it is numerable. (Contributed by Mario Carneiro, 5-Jan-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ dom card) | ||
Theorem | numdom 9463 | A set dominated by a numerable set is numerable. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ dom card) | ||
Theorem | ssnum 9464 | A subset of a numerable set is numerable. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ dom card) | ||
Theorem | onssnum 9465 | All subsets of the ordinals are numerable. (Contributed by Mario Carneiro, 12-Feb-2013.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ On) → 𝐴 ∈ dom card) | ||
Theorem | indcardi 9466* | Indirect strong induction on the cardinality of a finite or numerable set. (Contributed by Stefan O'Rear, 24-Aug-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ dom card) & ⊢ ((𝜑 ∧ 𝑅 ≼ 𝑇 ∧ ∀𝑦(𝑆 ≺ 𝑅 → 𝜒)) → 𝜓) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = 𝑦 → 𝑅 = 𝑆) & ⊢ (𝑥 = 𝐴 → 𝑅 = 𝑇) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | acnrcl 9467 | Reverse closure for the choice set predicate. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝑋 ∈ AC 𝐴 → 𝐴 ∈ V) | ||
Theorem | acneq 9468 | Equality theorem for the choice set function. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 = 𝐶 → AC 𝐴 = AC 𝐶) | ||
Theorem | isacn 9469* | The property of being a choice set of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑋 ∈ AC 𝐴 ↔ ∀𝑓 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥))) | ||
Theorem | acni 9470* | The property of being a choice set of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ ((𝑋 ∈ AC 𝐴 ∧ 𝐹:𝐴⟶(𝒫 𝑋 ∖ {∅})) → ∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥)) | ||
Theorem | acni2 9471* | The property of being a choice set of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ ((𝑋 ∈ AC 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅)) → ∃𝑔(𝑔:𝐴⟶𝑋 ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ 𝐵)) | ||
Theorem | acni3 9472* | The property of being a choice set of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝑦 = (𝑔‘𝑥) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝑋 ∈ AC 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑋 𝜑) → ∃𝑔(𝑔:𝐴⟶𝑋 ∧ ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | acnlem 9473* | Construct a mapping satisfying the consequent of isacn 9469. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑓‘𝑥)) → ∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥)) | ||
Theorem | numacn 9474 | A well-orderable set has choice sequences of every length. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝑋 ∈ dom card → 𝑋 ∈ AC 𝐴)) | ||
Theorem | finacn 9475 | Every set has finite choice sequences. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 ∈ Fin → AC 𝐴 = V) | ||
Theorem | acndom 9476 | A set with long choice sequences also has shorter choice sequences, where "shorter" here means the new index set is dominated by the old index set. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 ≼ 𝐵 → (𝑋 ∈ AC 𝐵 → 𝑋 ∈ AC 𝐴)) | ||
Theorem | acnnum 9477 | A set 𝑋 which has choice sequences on it of length 𝒫 𝑋 is well-orderable (and hence has choice sequences of every length). (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝑋 ∈ AC 𝒫 𝑋 ↔ 𝑋 ∈ dom card) | ||
Theorem | acnen 9478 | The class of choice sets of length 𝐴 is a cardinal invariant. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 ≈ 𝐵 → AC 𝐴 = AC 𝐵) | ||
Theorem | acndom2 9479 | A set smaller than one with choice sequences of length 𝐴 also has choice sequences of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝑋 ≼ 𝑌 → (𝑌 ∈ AC 𝐴 → 𝑋 ∈ AC 𝐴)) | ||
Theorem | acnen2 9480 | The class of sets with choice sequences of length 𝐴 is a cardinal invariant. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝑋 ≈ 𝑌 → (𝑋 ∈ AC 𝐴 ↔ 𝑌 ∈ AC 𝐴)) | ||
Theorem | fodomacn 9481 | A version of fodom 9943 that doesn't require the Axiom of Choice ax-ac 9880. If 𝐴 has choice sequences of length 𝐵, then any surjection from 𝐴 to 𝐵 can be inverted to an injection the other way. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 ∈ AC 𝐵 → (𝐹:𝐴–onto→𝐵 → 𝐵 ≼ 𝐴)) | ||
Theorem | fodomnum 9482 | A version of fodom 9943 that doesn't require the Axiom of Choice ax-ac 9880. (Contributed by Mario Carneiro, 28-Feb-2013.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐴 ∈ dom card → (𝐹:𝐴–onto→𝐵 → 𝐵 ≼ 𝐴)) | ||
Theorem | fonum 9483 | A surjection maps numerable sets to numerable sets. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ∈ dom card) | ||
Theorem | numwdom 9484 | A surjection maps numerable sets to numerable sets. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ≼* 𝐴) → 𝐵 ∈ dom card) | ||
Theorem | fodomfi2 9485 | Onto functions define dominance when a finite number of choices need to be made. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴) | ||
Theorem | wdomfil 9486 | Weak dominance agrees with normal for finite left sets. (Contributed by Stefan O'Rear, 28-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ (𝑋 ∈ Fin → (𝑋 ≼* 𝑌 ↔ 𝑋 ≼ 𝑌)) | ||
Theorem | infpwfien 9487 | Any infinite well-orderable set is equinumerous to its set of finite subsets. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ ((𝐴 ∈ dom card ∧ ω ≼ 𝐴) → (𝒫 𝐴 ∩ Fin) ≈ 𝐴) | ||
Theorem | inffien 9488 | The set of finite intersections of an infinite well-orderable set is equinumerous to the set itself. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ ((𝐴 ∈ dom card ∧ ω ≼ 𝐴) → (fi‘𝐴) ≈ 𝐴) | ||
Theorem | wdomnumr 9489 | Weak dominance agrees with normal for numerable right sets. (Contributed by Stefan O'Rear, 28-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ (𝐵 ∈ dom card → (𝐴 ≼* 𝐵 ↔ 𝐴 ≼ 𝐵)) | ||
Theorem | alephfnon 9490 | The aleph function is a function on the class of ordinal numbers. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 13-Sep-2013.) |
⊢ ℵ Fn On | ||
Theorem | aleph0 9491 | The first infinite cardinal number, discovered by Georg Cantor in 1873, has the same size as the set of natural numbers ω (and under our particular definition is also equal to it). In the literature, the argument of the aleph function is often written as a subscript, and the first aleph is written ℵ0. Exercise 3 of [TakeutiZaring] p. 91. Also Definition 12(i) of [Suppes] p. 228. From Moshé Machover, Set Theory, Logic, and Their Limitations, p. 95: "Aleph...the first letter in the Hebrew alphabet...is also the first letter of the Hebrew word...(einsoph, meaning infinity), which is a cabbalistic appellation of the deity. The notation is due to Cantor, who was deeply interested in mysticism." (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 13-Sep-2013.) |
⊢ (ℵ‘∅) = ω | ||
Theorem | alephlim 9492* | Value of the aleph function at a limit ordinal. Definition 12(iii) of [Suppes] p. 91. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 13-Sep-2013.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → (ℵ‘𝐴) = ∪ 𝑥 ∈ 𝐴 (ℵ‘𝑥)) | ||
Theorem | alephsuc 9493 | Value of the aleph function at a successor ordinal. Definition 12(ii) of [Suppes] p. 91. Here we express the successor aleph in terms of the Hartogs function df-har 9021, which gives the smallest ordinal that strictly dominates its argument (or the supremum of all ordinals that are dominated by the argument). (Contributed by Mario Carneiro, 13-Sep-2013.) (Revised by Mario Carneiro, 15-May-2015.) |
⊢ (𝐴 ∈ On → (ℵ‘suc 𝐴) = (har‘(ℵ‘𝐴))) | ||
Theorem | alephon 9494 | An aleph is an ordinal number. (Contributed by NM, 10-Nov-2003.) (Revised by Mario Carneiro, 13-Sep-2013.) |
⊢ (ℵ‘𝐴) ∈ On | ||
Theorem | alephcard 9495 | Every aleph is a cardinal number. Theorem 65 of [Suppes] p. 229. (Contributed by NM, 25-Oct-2003.) (Revised by Mario Carneiro, 2-Feb-2013.) |
⊢ (card‘(ℵ‘𝐴)) = (ℵ‘𝐴) | ||
Theorem | alephnbtwn 9496 | No cardinal can be sandwiched between an aleph and its successor aleph. Theorem 67 of [Suppes] p. 229. (Contributed by NM, 10-Nov-2003.) (Revised by Mario Carneiro, 15-May-2015.) |
⊢ ((card‘𝐵) = 𝐵 → ¬ ((ℵ‘𝐴) ∈ 𝐵 ∧ 𝐵 ∈ (ℵ‘suc 𝐴))) | ||
Theorem | alephnbtwn2 9497 | No set has equinumerosity between an aleph and its successor aleph. (Contributed by NM, 3-Nov-2003.) (Revised by Mario Carneiro, 2-Feb-2013.) |
⊢ ¬ ((ℵ‘𝐴) ≺ 𝐵 ∧ 𝐵 ≺ (ℵ‘suc 𝐴)) | ||
Theorem | alephordilem1 9498 | Lemma for alephordi 9499. (Contributed by NM, 23-Oct-2009.) (Revised by Mario Carneiro, 15-May-2015.) |
⊢ (𝐴 ∈ On → (ℵ‘𝐴) ≺ (ℵ‘suc 𝐴)) | ||
Theorem | alephordi 9499 | Strict ordering property of the aleph function. (Contributed by Mario Carneiro, 2-Feb-2013.) |
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → (ℵ‘𝐴) ≺ (ℵ‘𝐵))) | ||
Theorem | alephord 9500 | Ordering property of the aleph function. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 9-Feb-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 ↔ (ℵ‘𝐴) ≺ (ℵ‘𝐵))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |