| Metamath
Proof Explorer Theorem List (p. 101 of 494) | < 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: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | ficardom 10001 | The cardinal number of a finite set is a finite ordinal. (Contributed by Paul Chapman, 11-Apr-2009.) (Revised by Mario Carneiro, 4-Feb-2013.) |
| ⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω) | ||
| Theorem | ficardid 10002 | A finite set is equinumerous to its cardinal number. (Contributed by Mario Carneiro, 21-Sep-2013.) |
| ⊢ (𝐴 ∈ Fin → (card‘𝐴) ≈ 𝐴) | ||
| Theorem | cardnn 10003 | The cardinality of a natural number is the number. Corollary 10.23 of [TakeutiZaring] p. 90. (Contributed by Mario Carneiro, 7-Jan-2013.) |
| ⊢ (𝐴 ∈ ω → (card‘𝐴) = 𝐴) | ||
| Theorem | cardnueq0 10004 | The empty set is the only numerable set with cardinality zero. (Contributed by Mario Carneiro, 7-Jan-2013.) |
| ⊢ (𝐴 ∈ dom card → ((card‘𝐴) = ∅ ↔ 𝐴 = ∅)) | ||
| Theorem | cardne 10005 | No member of a cardinal number of a set is equinumerous to the set. Proposition 10.6(2) of [TakeutiZaring] p. 85. (Contributed by Mario Carneiro, 9-Jan-2013.) |
| ⊢ (𝐴 ∈ (card‘𝐵) → ¬ 𝐴 ≈ 𝐵) | ||
| Theorem | carden2a 10006 | If two sets have equal nonzero cardinalities, then they are equinumerous. This assertion and carden2b 10007 are meant to replace carden 10591 in ZF without AC. (Contributed by Mario Carneiro, 9-Jan-2013.) |
| ⊢ (((card‘𝐴) = (card‘𝐵) ∧ (card‘𝐴) ≠ ∅) → 𝐴 ≈ 𝐵) | ||
| Theorem | carden2b 10007 | If two sets are equinumerous, then they have equal cardinalities. (This assertion and carden2a 10006 are meant to replace carden 10591 in ZF without AC.) (Contributed by Mario Carneiro, 9-Jan-2013.) (Proof shortened by Mario Carneiro, 27-Apr-2015.) |
| ⊢ (𝐴 ≈ 𝐵 → (card‘𝐴) = (card‘𝐵)) | ||
| Theorem | card1 10008* | A set has cardinality one iff it is a singleton. (Contributed by Mario Carneiro, 10-Jan-2013.) |
| ⊢ ((card‘𝐴) = 1o ↔ ∃𝑥 𝐴 = {𝑥}) | ||
| Theorem | cardsn 10009 | A singleton has cardinality one. (Contributed by Mario Carneiro, 10-Jan-2013.) |
| ⊢ (𝐴 ∈ 𝑉 → (card‘{𝐴}) = 1o) | ||
| Theorem | carddomi2 10010 | Two sets have the dominance relationship if their cardinalities have the subset relationship and one is numerable. See also carddom 10594, which uses AC. (Contributed by Mario Carneiro, 11-Jan-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
| ⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ 𝑉) → ((card‘𝐴) ⊆ (card‘𝐵) → 𝐴 ≼ 𝐵)) | ||
| Theorem | sdomsdomcardi 10011 | A set strictly dominates if its cardinal strictly dominates. (Contributed by Mario Carneiro, 13-Jan-2013.) |
| ⊢ (𝐴 ≺ (card‘𝐵) → 𝐴 ≺ 𝐵) | ||
| Theorem | cardlim 10012 | An infinite cardinal is a limit ordinal. Equivalent to Exercise 4 of [TakeutiZaring] p. 91. (Contributed by Mario Carneiro, 13-Jan-2013.) |
| ⊢ (ω ⊆ (card‘𝐴) ↔ Lim (card‘𝐴)) | ||
| Theorem | cardsdomelir 10013 | A cardinal strictly dominates its members. Equivalent to Proposition 10.37 of [TakeutiZaring] p. 93. This is half of the assertion cardsdomel 10014 and can be proven without the AC. (Contributed by Mario Carneiro, 15-Jan-2013.) |
| ⊢ (𝐴 ∈ (card‘𝐵) → 𝐴 ≺ 𝐵) | ||
| Theorem | cardsdomel 10014 | 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 10015* | Two ways to express the property of being a cardinal number. (Contributed by Mario Carneiro, 15-Jan-2013.) |
| ⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 𝑥 ≺ 𝐴)) | ||
| Theorem | iscard2 10016* | 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 10017 | Two numerable sets have the dominance relationship iff their cardinalities have the subset relationship. See also carddom 10594, 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 10018 | 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 10019* | Lemma for cardprc 10020. (Contributed by Mario Carneiro, 22-Jan-2013.) (Revised by Mario Carneiro, 15-May-2015.) |
| ⊢ 𝐴 = {𝑥 ∣ (card‘𝑥) = 𝑥} ⇒ ⊢ ¬ 𝐴 ∈ V | ||
| Theorem | cardprc 10020 | 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 10601 to ensure that there is always a cardinal larger than a given cardinal, but we can use Hartogs' construction hartogs 9584 to construct (effectively) (ℵ‘suc 𝐴) from (ℵ‘𝐴), which achieves the same thing. (Contributed by Mario Carneiro, 22-Jan-2013.) |
| ⊢ {𝑥 ∣ (card‘𝑥) = 𝑥} ∉ V | ||
| Theorem | carduni 10021* | 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 10022* | The indexed union of a set of cardinals is a cardinal. (Contributed by NM, 3-Nov-2003.) |
| ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (card‘𝐵) = 𝐵 → (card‘∪ 𝑥 ∈ 𝐴 𝐵) = ∪ 𝑥 ∈ 𝐴 𝐵)) | ||
| Theorem | cardennn 10023 | If 𝐴 is equinumerous to a natural number, then that number is its cardinal. (Contributed by Mario Carneiro, 11-Jan-2013.) |
| ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ ω) → (card‘𝐴) = 𝐵) | ||
| Theorem | cardsucinf 10024 | The cardinality of the successor of an infinite ordinal. (Contributed by Mario Carneiro, 11-Jan-2013.) |
| ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (card‘suc 𝐴) = (card‘𝐴)) | ||
| Theorem | cardsucnn 10025 | The cardinality of the successor of a finite ordinal (natural number). This theorem does not hold for infinite ordinals; see cardsucinf 10024. (Contributed by NM, 7-Nov-2008.) |
| ⊢ (𝐴 ∈ ω → (card‘suc 𝐴) = suc (card‘𝐴)) | ||
| Theorem | cardom 10026 | 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 10027 | Two numerable sets are equinumerous iff their cardinal numbers are equal. Unlike carden 10591, the Axiom of Choice is not required. (Contributed by Mario Carneiro, 22-Sep-2013.) |
| ⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((card‘𝐴) = (card‘𝐵) ↔ 𝐴 ≈ 𝐵)) | ||
| Theorem | cardsdom2 10028 | 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 10029 | Trichotomy of dominance for numerable sets (does not use AC). (Contributed by Mario Carneiro, 29-Apr-2015.) |
| ⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴)) | ||
| Theorem | nnsdomel 10030 | Strict dominance and elementhood are the same for finite ordinals. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ 𝐴 ≺ 𝐵)) | ||
| Theorem | cardval2 10031* | An alternate version of the value of the cardinal number of a set. Compare cardval 10586. This theorem could be used to give a simpler definition of card in place of df-card 9979. It apparently does not occur in the literature. (Contributed by NM, 7-Nov-2003.) |
| ⊢ (𝐴 ∈ dom card → (card‘𝐴) = {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴}) | ||
| Theorem | isinffi 10032* | An infinite set contains subsets equinumerous to every finite set. Extension of isinf 9296 from finite ordinals to all finite sets. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
| ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐵–1-1→𝐴) | ||
| Theorem | fidomtri 10033 | 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 10034 | 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 10035 | The Hartogs number of a well-orderable set strictly dominates the set. (Contributed by Mario Carneiro, 15-May-2015.) |
| ⊢ (𝐴 ∈ dom card → 𝐴 ≺ (har‘𝐴)) | ||
| Theorem | onsdom 10036* | 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 10037* | An alternate expression for the Hartogs number of a well-orderable set. (Contributed by Mario Carneiro, 15-May-2015.) |
| ⊢ (𝐴 ∈ dom card → (har‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝐴 ≺ 𝑥}) | ||
| Theorem | harsucnn 10038 | The next cardinal after a finite ordinal is the successor ordinal. (Contributed by RP, 5-Nov-2023.) |
| ⊢ (𝐴 ∈ ω → (har‘𝐴) = suc 𝐴) | ||
| Theorem | cardmin2 10039* | 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 10040* | 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 10008), 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 10041. (Contributed by NM, 4-Nov-2013.) |
| ⊢ (𝐴 ≈ 1o ↔ 𝐴 ∈ {𝑥 ∣ (card‘𝑥) = 1o}) | ||
| Theorem | pm54.43 10041 |
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 10008), so that their 𝐴 ∈ 1 means, in our notation, 𝐴 ∈ {𝑥 ∣ (card‘𝑥) = 1o} which is the same as 𝐴 ≈ 1o by pm54.43lem 10040. 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 10214 shows the derivation of 1+1=2 for cardinal numbers from this theorem. (Contributed by NM, 4-Apr-2007.) |
| ⊢ ((𝐴 ≈ 1o ∧ 𝐵 ≈ 1o) → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐴 ∪ 𝐵) ≈ 2o)) | ||
| Theorem | enpr2 10042 | An unordered pair with distinct elements is equinumerous to ordinal two. This is a closed-form version of enpr2d 9089. (Contributed by FL, 17-Aug-2008.) Avoid ax-pow 5365, ax-un 7755. (Revised by BTernaryTau, 30-Dec-2024.) |
| ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈ 2o) | ||
| Theorem | pr2nelemOLD 10043 | Obsolete version of enpr2 10042 as of 30-Dec-2024. (Contributed by FL, 17-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈ 2o) | ||
| Theorem | pr2ne 10044 | If an unordered pair has two elements, then they are different. (Contributed by FL, 14-Feb-2010.) Avoid ax-pow 5365, ax-un 7755. (Revised by BTernaryTau, 30-Dec-2024.) |
| ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2o ↔ 𝐴 ≠ 𝐵)) | ||
| Theorem | pr2neOLD 10045 | Obsolete version of pr2ne 10044 as of 30-Dec-2024. (Contributed by FL, 14-Feb-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2o ↔ 𝐴 ≠ 𝐵)) | ||
| Theorem | prdom2 10046 | An unordered pair has at most two elements. (Contributed by FL, 22-Feb-2011.) |
| ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴, 𝐵} ≼ 2o) | ||
| Theorem | en2eqpr 10047 | Building a set with two elements. (Contributed by FL, 11-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
| ⊢ ((𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 ≠ 𝐵 → 𝐶 = {𝐴, 𝐵})) | ||
| Theorem | en2eleq 10048 | 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 10049 | 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 10050 | 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 10051* | Lexicographical order is a well-ordering of On × On. Proposition 7.56(1) of [TakeutiZaring] p. 54. Note that unlike r0weon 10052, 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 10052* | 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 10053* | Lemma for infxpen 10054. (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 10054 | 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 10055 | 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 10056 | The cartesian product of two countable sets is countable. (Contributed by Thierry Arnoux, 24-Sep-2017.) |
| ⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 × 𝐵) ≼ ω) | ||
| Theorem | infxpidm2 10057 | Every infinite well-orderable set is equinumerous to its Cartesian square. This theorem provides the basis for infinite cardinal arithmetic. Proposition 10.40 of [TakeutiZaring] p. 95. See also infxpidm 10602. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
| ⊢ ((𝐴 ∈ dom card ∧ ω ≼ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴) | ||
| Theorem | infxpenc 10058* | A canonical version of infxpen 10054, by a completely different approach (although it uses infxpen 10054 via xpomen 10055). Using Cantor's normal form, we can show that 𝐴 ↑o 𝐵 respects equinumerosity (oef1o 9738), 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 9746.) (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 10059* | Lemma for infxpenc2 10062. (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 10060* | Lemma for infxpenc2 10062. (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 10061* | Lemma for infxpenc2 10062. (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 10062* | Existence form of infxpenc 10058. A "uniform" or "canonical" version of infxpen 10054, 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 10063* | The union ∪ 𝑛 ∈ 𝐶(𝐴 ↑m 𝑛) is a disjoint union. (Contributed by Mario Carneiro, 17-May-2015.) (Revised by NM, 16-Jun-2017.) |
| ⊢ ∃*𝑛 ∈ 𝐶 𝐵 ∈ (𝐴 ↑m 𝑛) | ||
| Theorem | fseqenlem1 10064* | Lemma for fseqen 10067. (Contributed by Mario Carneiro, 17-May-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴) & ⊢ 𝐺 = seqω((𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))), {〈∅, 𝐵〉}) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ ω) → (𝐺‘𝐶):(𝐴 ↑m 𝐶)–1-1→𝐴) | ||
| Theorem | fseqenlem2 10065* | Lemma for fseqen 10067. (Contributed by Mario Carneiro, 17-May-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴) & ⊢ 𝐺 = seqω((𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))), {〈∅, 𝐵〉}) & ⊢ 𝐾 = (𝑦 ∈ ∪ 𝑘 ∈ ω (𝐴 ↑m 𝑘) ↦ 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉) ⇒ ⊢ (𝜑 → 𝐾:∪ 𝑘 ∈ ω (𝐴 ↑m 𝑘)–1-1→(ω × 𝐴)) | ||
| Theorem | fseqdom 10066* | One half of fseqen 10067. (Contributed by Mario Carneiro, 18-Nov-2014.) |
| ⊢ (𝐴 ∈ 𝑉 → (ω × 𝐴) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) | ||
| Theorem | fseqen 10067* | 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 10068 | 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 10069* | Lemma for dfac8a 10070. 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 10070* | 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 10071* | 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 10072* | Lemma for dfac8c 10073. (Contributed by Mario Carneiro, 10-Jan-2013.) |
| ⊢ 𝐹 = (𝑠 ∈ (𝐴 ∖ {∅}) ↦ (℩𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ¬ 𝑏𝑟𝑎)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (∃𝑟 𝑟 We ∪ 𝐴 → ∃𝑓∀𝑧 ∈ 𝐴 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) | ||
| Theorem | dfac8c 10073* | 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 10074* | A proof of the well-ordering theorem weth 10535, 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 10075* | A set is numerable iff it can be well-ordered. (Contributed by Mario Carneiro, 5-Jan-2013.) |
| ⊢ (𝐴 ∈ dom card ↔ ∃𝑟 𝑟 We 𝐴) | ||
| Theorem | ac5num 10076* | A version of ac5b 10518 with the choice as a hypothesis. (Contributed by Mario Carneiro, 27-Aug-2015.) |
| ⊢ ((∪ 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴) → ∃𝑓(𝑓:𝐴⟶∪ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥)) | ||
| Theorem | ondomen 10077 | If a set is dominated by an ordinal, then it is numerable. (Contributed by Mario Carneiro, 5-Jan-2013.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ dom card) | ||
| Theorem | numdom 10078 | A set dominated by a numerable set is numerable. (Contributed by Mario Carneiro, 28-Apr-2015.) |
| ⊢ ((𝐴 ∈ dom card ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ dom card) | ||
| Theorem | ssnum 10079 | A subset of a numerable set is numerable. (Contributed by Mario Carneiro, 28-Apr-2015.) |
| ⊢ ((𝐴 ∈ dom card ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ dom card) | ||
| Theorem | onssnum 10080 | All subsets of the ordinals are numerable. (Contributed by Mario Carneiro, 12-Feb-2013.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ On) → 𝐴 ∈ dom card) | ||
| Theorem | indcardi 10081* | Indirect strong induction on the cardinality of a finite or numerable set. (Contributed by Stefan O'Rear, 24-Aug-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ dom card) & ⊢ ((𝜑 ∧ 𝑅 ≼ 𝑇 ∧ ∀𝑦(𝑆 ≺ 𝑅 → 𝜒)) → 𝜓) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = 𝑦 → 𝑅 = 𝑆) & ⊢ (𝑥 = 𝐴 → 𝑅 = 𝑇) ⇒ ⊢ (𝜑 → 𝜃) | ||
| Theorem | acnrcl 10082 | Reverse closure for the choice set predicate. (Contributed by Mario Carneiro, 31-Aug-2015.) |
| ⊢ (𝑋 ∈ AC 𝐴 → 𝐴 ∈ V) | ||
| Theorem | acneq 10083 | Equality theorem for the choice set function. (Contributed by Mario Carneiro, 31-Aug-2015.) |
| ⊢ (𝐴 = 𝐶 → AC 𝐴 = AC 𝐶) | ||
| Theorem | isacn 10084* | The property of being a choice set of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.) |
| ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑋 ∈ AC 𝐴 ↔ ∀𝑓 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥))) | ||
| Theorem | acni 10085* | The property of being a choice set of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.) |
| ⊢ ((𝑋 ∈ AC 𝐴 ∧ 𝐹:𝐴⟶(𝒫 𝑋 ∖ {∅})) → ∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥)) | ||
| Theorem | acni2 10086* | The property of being a choice set of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.) |
| ⊢ ((𝑋 ∈ AC 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅)) → ∃𝑔(𝑔:𝐴⟶𝑋 ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ 𝐵)) | ||
| Theorem | acni3 10087* | The property of being a choice set of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.) |
| ⊢ (𝑦 = (𝑔‘𝑥) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝑋 ∈ AC 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑋 𝜑) → ∃𝑔(𝑔:𝐴⟶𝑋 ∧ ∀𝑥 ∈ 𝐴 𝜓)) | ||
| Theorem | acnlem 10088* | Construct a mapping satisfying the consequent of isacn 10084. (Contributed by Mario Carneiro, 31-Aug-2015.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑓‘𝑥)) → ∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥)) | ||
| Theorem | numacn 10089 | A well-orderable set has choice sequences of every length. (Contributed by Mario Carneiro, 31-Aug-2015.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝑋 ∈ dom card → 𝑋 ∈ AC 𝐴)) | ||
| Theorem | finacn 10090 | Every set has finite choice sequences. (Contributed by Mario Carneiro, 31-Aug-2015.) |
| ⊢ (𝐴 ∈ Fin → AC 𝐴 = V) | ||
| Theorem | acndom 10091 | 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 10092 | 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 10093 | The class of choice sets of length 𝐴 is a cardinal invariant. (Contributed by Mario Carneiro, 31-Aug-2015.) |
| ⊢ (𝐴 ≈ 𝐵 → AC 𝐴 = AC 𝐵) | ||
| Theorem | acndom2 10094 | 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 10095 | The class of sets with choice sequences of length 𝐴 is a cardinal invariant. (Contributed by Mario Carneiro, 31-Aug-2015.) |
| ⊢ (𝑋 ≈ 𝑌 → (𝑋 ∈ AC 𝐴 ↔ 𝑌 ∈ AC 𝐴)) | ||
| Theorem | fodomacn 10096 | A version of fodom 10563 that doesn't require the Axiom of Choice ax-ac 10499. 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 10097 | A version of fodom 10563 that doesn't require the Axiom of Choice ax-ac 10499. (Contributed by Mario Carneiro, 28-Feb-2013.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ (𝐴 ∈ dom card → (𝐹:𝐴–onto→𝐵 → 𝐵 ≼ 𝐴)) | ||
| Theorem | fonum 10098 | A surjection maps numerable sets to numerable sets. (Contributed by Mario Carneiro, 30-Apr-2015.) |
| ⊢ ((𝐴 ∈ dom card ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ∈ dom card) | ||
| Theorem | numwdom 10099 | A surjection maps numerable sets to numerable sets. (Contributed by Mario Carneiro, 27-Aug-2015.) |
| ⊢ ((𝐴 ∈ dom card ∧ 𝐵 ≼* 𝐴) → 𝐵 ∈ dom card) | ||
| Theorem | fodomfi2 10100 | Onto functions define dominance when a finite number of choices need to be made. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |