![]() |
Metamath
Proof Explorer Theorem List (p. 102 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | alephfplem3 10101* | Lemma for alephfp 10103. (Contributed by NM, 6-Nov-2004.) |
β’ π» = (rec(β΅, Ο) βΎ Ο) β β’ (π£ β Ο β (π»βπ£) β ran β΅) | ||
Theorem | alephfplem4 10102 | Lemma for alephfp 10103. (Contributed by NM, 5-Nov-2004.) |
β’ π» = (rec(β΅, Ο) βΎ Ο) β β’ βͺ (π» β Ο) β ran β΅ | ||
Theorem | alephfp 10103 | The aleph function has a fixed point. Similar to Proposition 11.18 of [TakeutiZaring] p. 104, except that we construct an actual example of a fixed point rather than just showing its existence. See alephfp2 10104 for an abbreviated version just showing existence. (Contributed by NM, 6-Nov-2004.) (Proof shortened by Mario Carneiro, 15-May-2015.) |
β’ π» = (rec(β΅, Ο) βΎ Ο) β β’ (β΅ββͺ (π» β Ο)) = βͺ (π» β Ο) | ||
Theorem | alephfp2 10104 | The aleph function has at least one fixed point. Proposition 11.18 of [TakeutiZaring] p. 104. See alephfp 10103 for an actual example of a fixed point. Compare the inequality alephle 10083 that holds in general. Note that if π₯ is a fixed point, then β΅ββ΅ββ΅β... β΅βπ₯ = π₯. (Contributed by NM, 6-Nov-2004.) (Revised by Mario Carneiro, 15-May-2015.) |
β’ βπ₯ β On (β΅βπ₯) = π₯ | ||
Theorem | alephval3 10105* | An alternate way to express the value of the aleph function: it is the least infinite cardinal different from all values at smaller arguments. Definition of aleph in [Enderton] p. 212 and definition of aleph in [BellMachover] p. 490 . (Contributed by NM, 16-Nov-2003.) |
β’ (π΄ β On β (β΅βπ΄) = β© {π₯ β£ ((cardβπ₯) = π₯ β§ Ο β π₯ β§ βπ¦ β π΄ Β¬ π₯ = (β΅βπ¦))}) | ||
Theorem | alephsucpw2 10106 | The power set of an aleph is not strictly dominated by the successor aleph. (The Generalized Continuum Hypothesis says they are equinumerous, see gch3 10671 or gchaleph2 10667.) The transposed form alephsucpw 10565 cannot be proven without the AC, and is in fact equivalent to it. (Contributed by Mario Carneiro, 2-Feb-2013.) |
β’ Β¬ π« (β΅βπ΄) βΊ (β΅βsuc π΄) | ||
Theorem | mappwen 10107 | Power rule for cardinal arithmetic. Theorem 11.21 of [TakeutiZaring] p. 106. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 27-Apr-2015.) |
β’ (((π΅ β dom card β§ Ο βΌ π΅) β§ (2o βΌ π΄ β§ π΄ βΌ π« π΅)) β (π΄ βm π΅) β π« π΅) | ||
Theorem | finnisoeu 10108* | A finite totally ordered set has a unique order isomorphism to a finite ordinal. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Proof shortened by Mario Carneiro, 26-Jun-2015.) |
β’ ((π Or π΄ β§ π΄ β Fin) β β!π π Isom E , π ((cardβπ΄), π΄)) | ||
Theorem | iunfictbso 10109 | Countability of a countable union of finite sets with a strict (not globally well) order fulfilling the choice role. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ ((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ π΄) β βͺ π΄ βΌ Ο) | ||
Syntax | wac 10110 | Wff for an abbreviation of the axiom of choice. |
wff CHOICE | ||
Definition | df-ac 10111* |
The expression CHOICE will be used as a
readable shorthand for any
form of the axiom of choice; all concrete forms are long, cryptic, have
dummy variables, or all three, making it useful to have a short name.
Similar to the Axiom of Choice (first form) of [Enderton] p. 49.
There is a slight problem with taking the exact form of ax-ac 10454 as our definition, because the equivalence to more standard forms (dfac2 10126) requires the Axiom of Regularity, which we often try to avoid. Thus, we take the first of the "textbook forms" as the definition and derive the form of ax-ac 10454 itself as dfac0 10128. (Contributed by Mario Carneiro, 22-Feb-2015.) |
β’ (CHOICE β βπ₯βπ(π β π₯ β§ π Fn dom π₯)) | ||
Theorem | aceq1 10112* | Equivalence of two versions of the Axiom of Choice ax-ac 10454. The proof uses neither AC nor the Axiom of Regularity. The right-hand side expresses our AC with the fewest number of different variables. (Contributed by NM, 5-Apr-2004.) |
β’ (βπ¦βπ§ β π₯ βπ€ β π§ β!π£ β π§ βπ’ β π¦ (π§ β π’ β§ π£ β π’) β βπ¦βπ§βπ€((π§ β π€ β§ π€ β π₯) β βπ₯βπ§(βπ₯((π§ β π€ β§ π€ β π₯) β§ (π§ β π₯ β§ π₯ β π¦)) β π§ = π₯))) | ||
Theorem | aceq0 10113* | Equivalence of two versions of the Axiom of Choice. The proof uses neither AC nor the Axiom of Regularity. The right-hand side is our original ax-ac 10454. (Contributed by NM, 5-Apr-2004.) |
β’ (βπ¦βπ§ β π₯ βπ€ β π§ β!π£ β π§ βπ’ β π¦ (π§ β π’ β§ π£ β π’) β βπ¦βπ§βπ€((π§ β π€ β§ π€ β π₯) β βπ£βπ’(βπ‘((π’ β π€ β§ π€ β π‘) β§ (π’ β π‘ β§ π‘ β π¦)) β π’ = π£))) | ||
Theorem | aceq2 10114* | Equivalence of two versions of the Axiom of Choice. The proof uses neither AC nor the Axiom of Regularity. (Contributed by NM, 5-Apr-2004.) |
β’ (βπ¦βπ§ β π₯ βπ€ β π§ β!π£ β π§ βπ’ β π¦ (π§ β π’ β§ π£ β π’) β βπ¦βπ§ β π₯ (π§ β β β β!π€ β π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£))) | ||
Theorem | aceq3lem 10115* | Lemma for dfac3 10116. (Contributed by NM, 2-Apr-2004.) (Revised by Mario Carneiro, 26-Jun-2015.) |
β’ πΉ = (π€ β dom π¦ β¦ (πβ{π’ β£ π€π¦π’})) β β’ (βπ₯βπβπ§ β π₯ (π§ β β β (πβπ§) β π§) β βπ(π β π¦ β§ π Fn dom π¦)) | ||
Theorem | dfac3 10116* | Equivalence of two versions of the Axiom of Choice. The left-hand side is defined as the Axiom of Choice (first form) of [Enderton] p. 49. The right-hand side is the Axiom of Choice of [TakeutiZaring] p. 83. The proof does not depend on AC. (Contributed by NM, 24-Mar-2004.) (Revised by Stefan O'Rear, 22-Feb-2015.) |
β’ (CHOICE β βπ₯βπβπ§ β π₯ (π§ β β β (πβπ§) β π§)) | ||
Theorem | dfac4 10117* | Equivalence of two versions of the Axiom of Choice. The right-hand side is Axiom AC of [BellMachover] p. 488. The proof does not depend on AC. (Contributed by NM, 24-Mar-2004.) (Revised by Mario Carneiro, 26-Jun-2015.) |
β’ (CHOICE β βπ₯βπ(π Fn π₯ β§ βπ§ β π₯ (π§ β β β (πβπ§) β π§))) | ||
Theorem | dfac5lem1 10118* | Lemma for dfac5 10123. (Contributed by NM, 12-Apr-2004.) |
β’ (β!π£ π£ β (({π€} Γ π€) β© π¦) β β!π(π β π€ β§ β¨π€, πβ© β π¦)) | ||
Theorem | dfac5lem2 10119* | Lemma for dfac5 10123. (Contributed by NM, 12-Apr-2004.) |
β’ π΄ = {π’ β£ (π’ β β β§ βπ‘ β β π’ = ({π‘} Γ π‘))} β β’ (β¨π€, πβ© β βͺ π΄ β (π€ β β β§ π β π€)) | ||
Theorem | dfac5lem3 10120* | Lemma for dfac5 10123. (Contributed by NM, 12-Apr-2004.) |
β’ π΄ = {π’ β£ (π’ β β β§ βπ‘ β β π’ = ({π‘} Γ π‘))} β β’ (({π€} Γ π€) β π΄ β (π€ β β β§ π€ β β)) | ||
Theorem | dfac5lem4 10121* | Lemma for dfac5 10123. (Contributed by NM, 11-Apr-2004.) |
β’ π΄ = {π’ β£ (π’ β β β§ βπ‘ β β π’ = ({π‘} Γ π‘))} & β’ π΅ = (βͺ π΄ β© π¦) & β’ (π β βπ₯((βπ§ β π₯ π§ β β β§ βπ§ β π₯ βπ€ β π₯ (π§ β π€ β (π§ β© π€) = β )) β βπ¦βπ§ β π₯ β!π£ π£ β (π§ β© π¦))) β β’ (π β βπ¦βπ§ β π΄ β!π£ π£ β (π§ β© π¦)) | ||
Theorem | dfac5lem5 10122* | Lemma for dfac5 10123. (Contributed by NM, 12-Apr-2004.) |
β’ π΄ = {π’ β£ (π’ β β β§ βπ‘ β β π’ = ({π‘} Γ π‘))} & β’ π΅ = (βͺ π΄ β© π¦) & β’ (π β βπ₯((βπ§ β π₯ π§ β β β§ βπ§ β π₯ βπ€ β π₯ (π§ β π€ β (π§ β© π€) = β )) β βπ¦βπ§ β π₯ β!π£ π£ β (π§ β© π¦))) β β’ (π β βπβπ€ β β (π€ β β β (πβπ€) β π€)) | ||
Theorem | dfac5 10123* | Equivalence of two versions of the Axiom of Choice. The right-hand side is Theorem 6M(4) of [Enderton] p. 151 and asserts that given a family of mutually disjoint nonempty sets, a set exists containing exactly one member from each set in the family. The proof does not depend on AC. (Contributed by NM, 11-Apr-2004.) (Revised by Mario Carneiro, 17-May-2015.) |
β’ (CHOICE β βπ₯((βπ§ β π₯ π§ β β β§ βπ§ β π₯ βπ€ β π₯ (π§ β π€ β (π§ β© π€) = β )) β βπ¦βπ§ β π₯ β!π£ π£ β (π§ β© π¦))) | ||
Theorem | dfac2a 10124* | Our Axiom of Choice (in the form of ac3 10457) implies the Axiom of Choice (first form) of [Enderton] p. 49. The proof uses neither AC nor the Axiom of Regularity. See dfac2b 10125 for the converse (which does use the Axiom of Regularity). (Contributed by NM, 5-Apr-2004.) (Revised by Mario Carneiro, 26-Jun-2015.) |
β’ (βπ₯βπ¦βπ§ β π₯ (π§ β β β β!π€ β π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£)) β CHOICE) | ||
Theorem | dfac2b 10125* | Axiom of Choice (first form) of [Enderton] p. 49 implies our Axiom of Choice (in the form of ac3 10457). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elneq 9593 and preleq 9611 that are referenced in the proof each make use of Regularity for their derivations. (The reverse implication can be derived without using Regularity; see dfac2a 10124.) (Contributed by NM, 5-Apr-2004.) (Revised by Mario Carneiro, 26-Jun-2015.) (Revised by AV, 16-Jun-2022.) |
β’ (CHOICE β βπ₯βπ¦βπ§ β π₯ (π§ β β β β!π€ β π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£))) | ||
Theorem | dfac2 10126* | Axiom of Choice (first form) of [Enderton] p. 49 corresponds to our Axiom of Choice (in the form of ac3 10457). The proof does not make use of AC, but the Axiom of Regularity is used (by applying dfac2b 10125). (Contributed by NM, 5-Apr-2004.) (Revised by Mario Carneiro, 26-Jun-2015.) (Revised by AV, 16-Jun-2022.) |
β’ (CHOICE β βπ₯βπ¦βπ§ β π₯ (π§ β β β β!π€ β π§ βπ£ β π¦ (π§ β π£ β§ π€ β π£))) | ||
Theorem | dfac7 10127* | Equivalence of the Axiom of Choice (first form) of [Enderton] p. 49 and our Axiom of Choice (in the form of ac2 10456). The proof does not depend on AC but does depend on the Axiom of Regularity. (Contributed by Mario Carneiro, 17-May-2015.) |
β’ (CHOICE β βπ₯βπ¦βπ§ β π₯ βπ€ β π§ β!π£ β π§ βπ’ β π¦ (π§ β π’ β§ π£ β π’)) | ||
Theorem | dfac0 10128* | Equivalence of two versions of the Axiom of Choice. The proof uses the Axiom of Regularity. The right-hand side is our original ax-ac 10454. (Contributed by Mario Carneiro, 17-May-2015.) |
β’ (CHOICE β βπ₯βπ¦βπ§βπ€((π§ β π€ β§ π€ β π₯) β βπ£βπ’(βπ‘((π’ β π€ β§ π€ β π‘) β§ (π’ β π‘ β§ π‘ β π¦)) β π’ = π£))) | ||
Theorem | dfac1 10129* | Equivalence of two versions of the Axiom of Choice ax-ac 10454. The proof uses the Axiom of Regularity. The right-hand side expresses our AC with the fewest number of different variables. (Contributed by Mario Carneiro, 17-May-2015.) |
β’ (CHOICE β βπ₯βπ¦βπ§βπ€((π§ β π€ β§ π€ β π₯) β βπ₯βπ§(βπ₯((π§ β π€ β§ π€ β π₯) β§ (π§ β π₯ β§ π₯ β π¦)) β π§ = π₯))) | ||
Theorem | dfac8 10130* | A proof of the equivalency of the well-ordering theorem weth 10490 and the axiom of choice ac7 10468. (Contributed by Mario Carneiro, 5-Jan-2013.) |
β’ (CHOICE β βπ₯βπ π We π₯) | ||
Theorem | dfac9 10131* | Equivalence of the axiom of choice with a statement related to ac9 10478; definition AC3 of [Schechter] p. 139. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ (CHOICE β βπ((Fun π β§ β β ran π) β Xπ₯ β dom π(πβπ₯) β β )) | ||
Theorem | dfac10 10132 | Axiom of Choice equivalent: the cardinality function measures every set. (Contributed by Mario Carneiro, 6-May-2015.) |
β’ (CHOICE β dom card = V) | ||
Theorem | dfac10c 10133* | Axiom of Choice equivalent: every set is equinumerous to an ordinal. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
β’ (CHOICE β βπ₯βπ¦ β On π¦ β π₯) | ||
Theorem | dfac10b 10134 | Axiom of Choice equivalent: every set is equinumerous to an ordinal (quantifier-free short cryptic version alluded to in df-ac 10111). (Contributed by Stefan O'Rear, 17-Jan-2015.) |
β’ (CHOICE β ( β β On) = V) | ||
Theorem | acacni 10135 | A choice equivalent: every set has choice sets of every length. (Contributed by Mario Carneiro, 31-Aug-2015.) |
β’ ((CHOICE β§ π΄ β π) β AC π΄ = V) | ||
Theorem | dfacacn 10136 | A choice equivalent: every set has choice sets of every length. (Contributed by Mario Carneiro, 31-Aug-2015.) |
β’ (CHOICE β βπ₯AC π₯ = V) | ||
Theorem | dfac13 10137 | The axiom of choice holds iff every set has choice sequences as long as itself. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (CHOICE β βπ₯ π₯ β AC π₯) | ||
Theorem | dfac12lem1 10138* | Lemma for dfac12 10144. (Contributed by Mario Carneiro, 29-May-2015.) |
β’ (π β π΄ β On) & β’ (π β πΉ:π« (harβ(π 1βπ΄))β1-1βOn) & β’ πΊ = recs((π₯ β V β¦ (π¦ β (π 1βdom π₯) β¦ if(dom π₯ = βͺ dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦)))))) & β’ (π β πΆ β On) & β’ π» = (β‘OrdIso( E , ran (πΊββͺ πΆ)) β (πΊββͺ πΆ)) β β’ (π β (πΊβπΆ) = (π¦ β (π 1βπΆ) β¦ if(πΆ = βͺ πΆ, ((suc βͺ ran βͺ (πΊ β πΆ) Β·o (rankβπ¦)) +o ((πΊβsuc (rankβπ¦))βπ¦)), (πΉβ(π» β π¦))))) | ||
Theorem | dfac12lem2 10139* | Lemma for dfac12 10144. (Contributed by Mario Carneiro, 29-May-2015.) |
β’ (π β π΄ β On) & β’ (π β πΉ:π« (harβ(π 1βπ΄))β1-1βOn) & β’ πΊ = recs((π₯ β V β¦ (π¦ β (π 1βdom π₯) β¦ if(dom π₯ = βͺ dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦)))))) & β’ (π β πΆ β On) & β’ π» = (β‘OrdIso( E , ran (πΊββͺ πΆ)) β (πΊββͺ πΆ)) & β’ (π β πΆ β π΄) & β’ (π β βπ§ β πΆ (πΊβπ§):(π 1βπ§)β1-1βOn) β β’ (π β (πΊβπΆ):(π 1βπΆ)β1-1βOn) | ||
Theorem | dfac12lem3 10140* | Lemma for dfac12 10144. (Contributed by Mario Carneiro, 29-May-2015.) |
β’ (π β π΄ β On) & β’ (π β πΉ:π« (harβ(π 1βπ΄))β1-1βOn) & β’ πΊ = recs((π₯ β V β¦ (π¦ β (π 1βdom π₯) β¦ if(dom π₯ = βͺ dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)), (πΉβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦)))))) β β’ (π β (π 1βπ΄) β dom card) | ||
Theorem | dfac12r 10141 | The axiom of choice holds iff every ordinal has a well-orderable powerset. This version of dfac12 10144 does not assume the Axiom of Regularity. (Contributed by Mario Carneiro, 29-May-2015.) |
β’ (βπ₯ β On π« π₯ β dom card β βͺ (π 1 β On) β dom card) | ||
Theorem | dfac12k 10142* | Equivalence of dfac12 10144 and dfac12a 10143, without using Regularity. (Contributed by Mario Carneiro, 21-May-2015.) |
β’ (βπ₯ β On π« π₯ β dom card β βπ¦ β On π« (β΅βπ¦) β dom card) | ||
Theorem | dfac12a 10143 | The axiom of choice holds iff every ordinal has a well-orderable powerset. (Contributed by Mario Carneiro, 29-May-2015.) |
β’ (CHOICE β βπ₯ β On π« π₯ β dom card) | ||
Theorem | dfac12 10144 | The axiom of choice holds iff every aleph has a well-orderable powerset. (Contributed by Mario Carneiro, 21-May-2015.) |
β’ (CHOICE β βπ₯ β On π« (β΅βπ₯) β dom card) | ||
Theorem | kmlem1 10145* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, 1 => 2. (Contributed by NM, 5-Apr-2004.) |
β’ (βπ₯((βπ§ β π₯ π§ β β β§ βπ§ β π₯ βπ€ β π₯ π) β βπ¦βπ§ β π₯ π) β βπ₯(βπ§ β π₯ βπ€ β π₯ π β βπ¦βπ§ β π₯ (π§ β β β π))) | ||
Theorem | kmlem2 10146* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004.) |
β’ (βπ¦βπ§ β π₯ (π β β!π€ π€ β (π§ β© π¦)) β βπ¦(Β¬ π¦ β π₯ β§ βπ§ β π₯ (π β β!π€ π€ β (π§ β© π¦)))) | ||
Theorem | kmlem3 10147* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. The right-hand side is part of the hypothesis of 4. (Contributed by NM, 25-Mar-2004.) |
β’ ((π§ β βͺ (π₯ β {π§})) β β β βπ£ β π§ βπ€ β π₯ (π§ β π€ β Β¬ π£ β (π§ β© π€))) | ||
Theorem | kmlem4 10148* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 26-Mar-2004.) |
β’ ((π€ β π₯ β§ π§ β π€) β ((π§ β βͺ (π₯ β {π§})) β© π€) = β ) | ||
Theorem | kmlem5 10149* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004.) |
β’ ((π€ β π₯ β§ π§ β π€) β ((π§ β βͺ (π₯ β {π§})) β© (π€ β βͺ (π₯ β {π€}))) = β ) | ||
Theorem | kmlem6 10150* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 4 => 1. (Contributed by NM, 26-Mar-2004.) |
β’ ((βπ§ β π₯ π§ β β β§ βπ§ β π₯ βπ€ β π₯ (π β π΄ = β )) β βπ§ β π₯ βπ£ β π§ βπ€ β π₯ (π β Β¬ π£ β π΄)) | ||
Theorem | kmlem7 10151* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 4 => 1. (Contributed by NM, 26-Mar-2004.) |
β’ ((βπ§ β π₯ π§ β β β§ βπ§ β π₯ βπ€ β π₯ (π§ β π€ β (π§ β© π€) = β )) β Β¬ βπ§ β π₯ βπ£ β π§ βπ€ β π₯ (π§ β π€ β§ π£ β (π§ β© π€))) | ||
Theorem | kmlem8 10152* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4 1 <=> 4. (Contributed by NM, 4-Apr-2004.) |
β’ ((Β¬ βπ§ β π’ βπ€ β π§ π β βπ¦βπ§ β π’ (π§ β β β β!π€ π€ β (π§ β© π¦))) β (βπ§ β π’ βπ€ β π§ π β¨ βπ¦(Β¬ π¦ β π’ β§ βπ§ β π’ β!π€ π€ β (π§ β© π¦)))) | ||
Theorem | kmlem9 10153* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004.) |
β’ π΄ = {π’ β£ βπ‘ β π₯ π’ = (π‘ β βͺ (π₯ β {π‘}))} β β’ βπ§ β π΄ βπ€ β π΄ (π§ β π€ β (π§ β© π€) = β ) | ||
Theorem | kmlem10 10154* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004.) |
β’ π΄ = {π’ β£ βπ‘ β π₯ π’ = (π‘ β βͺ (π₯ β {π‘}))} β β’ (ββ(βπ§ β β βπ€ β β (π§ β π€ β (π§ β© π€) = β ) β βπ¦βπ§ β β π) β βπ¦βπ§ β π΄ π) | ||
Theorem | kmlem11 10155* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 26-Mar-2004.) |
β’ π΄ = {π’ β£ βπ‘ β π₯ π’ = (π‘ β βͺ (π₯ β {π‘}))} β β’ (π§ β π₯ β (π§ β© βͺ π΄) = (π§ β βͺ (π₯ β {π§}))) | ||
Theorem | kmlem12 10156* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 27-Mar-2004.) |
β’ π΄ = {π’ β£ βπ‘ β π₯ π’ = (π‘ β βͺ (π₯ β {π‘}))} β β’ (βπ§ β π₯ (π§ β βͺ (π₯ β {π§})) β β β (βπ§ β π΄ (π§ β β β β!π£ π£ β (π§ β© π¦)) β βπ§ β π₯ (π§ β β β β!π£ π£ β (π§ β© (π¦ β© βͺ π΄))))) | ||
Theorem | kmlem13 10157* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4 1 <=> 4. (Contributed by NM, 5-Apr-2004.) |
β’ π΄ = {π’ β£ βπ‘ β π₯ π’ = (π‘ β βͺ (π₯ β {π‘}))} β β’ (βπ₯((βπ§ β π₯ π§ β β β§ βπ§ β π₯ βπ€ β π₯ (π§ β π€ β (π§ β© π€) = β )) β βπ¦βπ§ β π₯ β!π£ π£ β (π§ β© π¦)) β βπ₯(Β¬ βπ§ β π₯ βπ£ β π§ βπ€ β π₯ (π§ β π€ β§ π£ β (π§ β© π€)) β βπ¦βπ§ β π₯ (π§ β β β β!π£ π£ β (π§ β© π¦)))) | ||
Theorem | kmlem14 10158* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 5 <=> 4. (Contributed by NM, 4-Apr-2004.) |
β’ (π β (π§ β π¦ β ((π£ β π₯ β§ π¦ β π£) β§ π§ β π£))) & β’ (π β (π§ β π₯ β ((π£ β π§ β§ π£ β π¦) β§ ((π’ β π§ β§ π’ β π¦) β π’ = π£)))) & β’ (π β βπ§ β π₯ β!π£ π£ β (π§ β© π¦)) β β’ (βπ§ β π₯ βπ£ β π§ βπ€ β π₯ (π§ β π€ β§ π£ β (π§ β© π€)) β βπ¦βπ§βπ£βπ’(π¦ β π₯ β§ π)) | ||
Theorem | kmlem15 10159* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 5 <=> 4. (Contributed by NM, 4-Apr-2004.) |
β’ (π β (π§ β π¦ β ((π£ β π₯ β§ π¦ β π£) β§ π§ β π£))) & β’ (π β (π§ β π₯ β ((π£ β π§ β§ π£ β π¦) β§ ((π’ β π§ β§ π’ β π¦) β π’ = π£)))) & β’ (π β βπ§ β π₯ β!π£ π£ β (π§ β© π¦)) β β’ ((Β¬ π¦ β π₯ β§ π) β βπ§βπ£βπ’(Β¬ π¦ β π₯ β§ π)) | ||
Theorem | kmlem16 10160* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4 5 <=> 4. (Contributed by NM, 4-Apr-2004.) |
β’ (π β (π§ β π¦ β ((π£ β π₯ β§ π¦ β π£) β§ π§ β π£))) & β’ (π β (π§ β π₯ β ((π£ β π§ β§ π£ β π¦) β§ ((π’ β π§ β§ π’ β π¦) β π’ = π£)))) & β’ (π β βπ§ β π₯ β!π£ π£ β (π§ β© π¦)) β β’ ((βπ§ β π₯ βπ£ β π§ βπ€ β π₯ (π§ β π€ β§ π£ β (π§ β© π€)) β¨ βπ¦(Β¬ π¦ β π₯ β§ π)) β βπ¦βπ§βπ£βπ’((π¦ β π₯ β§ π) β¨ (Β¬ π¦ β π₯ β§ π))) | ||
Theorem | dfackm 10161* | Equivalence of the Axiom of Choice and Maes' AC ackm 10460. The proof consists of lemmas kmlem1 10145 through kmlem16 10160 and this final theorem. AC is not used for the proof. Note: bypassing the first step (i.e., replacing dfac5 10123 with biid 261) establishes the AC equivalence shown by Maes' writeup. The left-hand-side AC shown here was chosen because it is shorter to display. (Contributed by NM, 13-Apr-2004.) (Revised by Mario Carneiro, 17-May-2015.) |
β’ (CHOICE β βπ₯βπ¦βπ§βπ£βπ’((π¦ β π₯ β§ (π§ β π¦ β ((π£ β π₯ β§ Β¬ π¦ = π£) β§ π§ β π£))) β¨ (Β¬ π¦ β π₯ β§ (π§ β π₯ β ((π£ β π§ β§ π£ β π¦) β§ ((π’ β π§ β§ π’ β π¦) β π’ = π£)))))) | ||
For cardinal arithmetic, we follow [Mendelson] p. 258. Rather than defining operations restricted to cardinal numbers, we use disjoint union df-dju 9896 (β) for cardinal addition, Cartesian product df-xp 5683 (Γ) for cardinal multiplication, and set exponentiation df-map 8822 (βm) for cardinal exponentiation. Equinumerosity and dominance serve the roles of equality and ordering. If we wanted to, we could easily convert our theorems to actual cardinal number operations via carden 10546, carddom 10549, and cardsdom 10550. The advantage of Mendelson's approach is that we can directly use many equinumerosity theorems that we already have available. | ||
Theorem | undjudom 10162 | Cardinal addition dominates union. (Contributed by NM, 28-Sep-2004.) (Revised by Jim Kingdon, 15-Aug-2023.) |
β’ ((π΄ β π β§ π΅ β π) β (π΄ βͺ π΅) βΌ (π΄ β π΅)) | ||
Theorem | endjudisj 10163 | Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by NM, 5-Apr-2007.) |
β’ ((π΄ β π β§ π΅ β π β§ (π΄ β© π΅) = β ) β (π΄ β π΅) β (π΄ βͺ π΅)) | ||
Theorem | djuen 10164 | Disjoint unions of equinumerous sets are equinumerous. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
β’ ((π΄ β π΅ β§ πΆ β π·) β (π΄ β πΆ) β (π΅ β π·)) | ||
Theorem | djuenun 10165 | Disjoint union is equinumerous to union for disjoint sets. (Contributed by Mario Carneiro, 29-Apr-2015.) (Revised by Jim Kingdon, 19-Aug-2023.) |
β’ ((π΄ β π΅ β§ πΆ β π· β§ (π΅ β© π·) = β ) β (π΄ β πΆ) β (π΅ βͺ π·)) | ||
Theorem | dju1en 10166 | Cardinal addition with cardinal one (which is the same as ordinal one). Used in proof of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
β’ ((π΄ β π β§ Β¬ π΄ β π΄) β (π΄ β 1o) β suc π΄) | ||
Theorem | dju1dif 10167 | Adding and subtracting one gives back the original cardinality. Similar to pncan 11466 for cardinalities. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by Jim Kingdon, 20-Aug-2023.) |
β’ ((π΄ β π β§ π΅ β (π΄ β 1o)) β ((π΄ β 1o) β {π΅}) β π΄) | ||
Theorem | dju1p1e2 10168 | 1+1=2 for cardinal number addition, derived from pm54.43 9996 as promised. Theorem *110.643 of Principia Mathematica, vol. II, p. 86, which adds the remark, "The above proposition is occasionally useful." Whitehead and Russell define cardinal addition on collections of all sets equinumerous to 1 and 2 (which for us are proper classes unless we restrict them as in karden 9890), but after applying definitions, our theorem is equivalent. Because we use a disjoint union for cardinal addition (as explained in the comment at the top of this section), we use β instead of =. See dju1p1e2ALT 10169 for a shorter proof that doesn't use pm54.43 9996. (Contributed by NM, 5-Apr-2007.) (Proof modification is discouraged.) |
β’ (1o β 1o) β 2o | ||
Theorem | dju1p1e2ALT 10169 | Alternate proof of dju1p1e2 10168. (Contributed by Mario Carneiro, 29-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (1o β 1o) β 2o | ||
Theorem | dju0en 10170 | Cardinal addition with cardinal zero (the empty set). Part (a1) of proof of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
β’ (π΄ β π β (π΄ β β ) β π΄) | ||
Theorem | xp2dju 10171 | Two times a cardinal number. Exercise 4.56(g) of [Mendelson] p. 258. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
β’ (2o Γ π΄) = (π΄ β π΄) | ||
Theorem | djucomen 10172 | Commutative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258. (Contributed by NM, 24-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
β’ ((π΄ β π β§ π΅ β π) β (π΄ β π΅) β (π΅ β π΄)) | ||
Theorem | djuassen 10173 | Associative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258. (Contributed by NM, 26-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β ((π΄ β π΅) β πΆ) β (π΄ β (π΅ β πΆ))) | ||
Theorem | xpdjuen 10174 | Cardinal multiplication distributes over cardinal addition. Theorem 6I(3) of [Enderton] p. 142. (Contributed by NM, 26-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β (π΄ Γ (π΅ β πΆ)) β ((π΄ Γ π΅) β (π΄ Γ πΆ))) | ||
Theorem | mapdjuen 10175 | Sum of exponents law for cardinal arithmetic. Theorem 6I(4) of [Enderton] p. 142. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β (π΄ βm (π΅ β πΆ)) β ((π΄ βm π΅) Γ (π΄ βm πΆ))) | ||
Theorem | pwdjuen 10176 | Sum of exponents law for cardinal arithmetic. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ ((π΄ β π β§ π΅ β π) β π« (π΄ β π΅) β (π« π΄ Γ π« π΅)) | ||
Theorem | djudom1 10177 | Ordering law for cardinal addition. Exercise 4.56(f) of [Mendelson] p. 258. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) (Revised by Jim Kingdon, 1-Sep-2023.) |
β’ ((π΄ βΌ π΅ β§ πΆ β π) β (π΄ β πΆ) βΌ (π΅ β πΆ)) | ||
Theorem | djudom2 10178 | Ordering law for cardinal addition. Theorem 6L(a) of [Enderton] p. 149. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
β’ ((π΄ βΌ π΅ β§ πΆ β π) β (πΆ β π΄) βΌ (πΆ β π΅)) | ||
Theorem | djudoml 10179 | A set is dominated by its disjoint union with another. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
β’ ((π΄ β π β§ π΅ β π) β π΄ βΌ (π΄ β π΅)) | ||
Theorem | djuxpdom 10180 | Cartesian product dominates disjoint union for sets with cardinality greater than 1. Similar to Proposition 10.36 of [TakeutiZaring] p. 93. (Contributed by Mario Carneiro, 18-May-2015.) |
β’ ((1o βΊ π΄ β§ 1o βΊ π΅) β (π΄ β π΅) βΌ (π΄ Γ π΅)) | ||
Theorem | djufi 10181 | The disjoint union of two finite sets is finite. (Contributed by NM, 22-Oct-2004.) |
β’ ((π΄ βΊ Ο β§ π΅ βΊ Ο) β (π΄ β π΅) βΊ Ο) | ||
Theorem | cdainflem 10182 | Any partition of omega into two pieces (which may be disjoint) contains an infinite subset. (Contributed by Mario Carneiro, 11-Feb-2013.) |
β’ ((π΄ βͺ π΅) β Ο β (π΄ β Ο β¨ π΅ β Ο)) | ||
Theorem | djuinf 10183 | A set is infinite iff the cardinal sum with itself is infinite. (Contributed by NM, 22-Oct-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
β’ (Ο βΌ π΄ β Ο βΌ (π΄ β π΄)) | ||
Theorem | infdju1 10184 | An infinite set is equinumerous to itself added with one. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ (Ο βΌ π΄ β (π΄ β 1o) β π΄) | ||
Theorem | pwdju1 10185 | The sum of a powerset with itself is equipotent to the successor powerset. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ (π΄ β π β (π« π΄ β π« π΄) β π« (π΄ β 1o)) | ||
Theorem | pwdjuidm 10186 | If the natural numbers inject into π΄, then π« π΄ is idempotent under cardinal sum. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ (Ο βΌ π΄ β (π« π΄ β π« π΄) β π« π΄) | ||
Theorem | djulepw 10187 | If π΄ is idempotent under cardinal sum and π΅ is dominated by the power set of π΄, then so is the cardinal sum of π΄ and π΅. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ (((π΄ β π΄) β π΄ β§ π΅ βΌ π« π΄) β (π΄ β π΅) βΌ π« π΄) | ||
Theorem | onadju 10188 | The cardinal and ordinal sums are always equinumerous. (Contributed by Mario Carneiro, 6-Feb-2013.) (Revised by Jim Kingdon, 7-Sep-2023.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ +o π΅) β (π΄ β π΅)) | ||
Theorem | cardadju 10189 | The cardinal sum is equinumerous to an ordinal sum of the cardinals. (Contributed by Mario Carneiro, 6-Feb-2013.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ ((π΄ β dom card β§ π΅ β dom card) β (π΄ β π΅) β ((cardβπ΄) +o (cardβπ΅))) | ||
Theorem | djunum 10190 | The disjoint union of two numerable sets is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
β’ ((π΄ β dom card β§ π΅ β dom card) β (π΄ β π΅) β dom card) | ||
Theorem | unnum 10191 | The union of two numerable sets is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
β’ ((π΄ β dom card β§ π΅ β dom card) β (π΄ βͺ π΅) β dom card) | ||
Theorem | nnadju 10192 | The cardinal and ordinal sums of finite ordinals are equal. For a shorter proof using ax-rep 5286, see nnadjuALT 10193. (Contributed by Paul Chapman, 11-Apr-2009.) (Revised by Mario Carneiro, 6-Feb-2013.) Avoid ax-rep 5286. (Revised by BTernaryTau, 2-Jul-2024.) |
β’ ((π΄ β Ο β§ π΅ β Ο) β (cardβ(π΄ β π΅)) = (π΄ +o π΅)) | ||
Theorem | nnadjuALT 10193 | Shorter proof of nnadju 10192 using ax-rep 5286. (Contributed by Paul Chapman, 11-Apr-2009.) (Revised by Mario Carneiro, 6-Feb-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Ο β§ π΅ β Ο) β (cardβ(π΄ β π΅)) = (π΄ +o π΅)) | ||
Theorem | ficardadju 10194 | The disjoint union of finite sets is equinumerous to the ordinal sum of the cardinalities of those sets. (Contributed by BTernaryTau, 3-Jul-2024.) |
β’ ((π΄ β Fin β§ π΅ β Fin) β (π΄ β π΅) β ((cardβπ΄) +o (cardβπ΅))) | ||
Theorem | ficardun 10195 | The cardinality of the union of disjoint, finite sets is the ordinal sum of their cardinalities. (Contributed by Paul Chapman, 5-Jun-2009.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) Avoid ax-rep 5286. (Revised by BTernaryTau, 3-Jul-2024.) |
β’ ((π΄ β Fin β§ π΅ β Fin β§ (π΄ β© π΅) = β ) β (cardβ(π΄ βͺ π΅)) = ((cardβπ΄) +o (cardβπ΅))) | ||
Theorem | ficardunOLD 10196 | Obsolete version of ficardun 10195 as of 3-Jul-2024. (Contributed by Paul Chapman, 5-Jun-2009.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Fin β§ π΅ β Fin β§ (π΄ β© π΅) = β ) β (cardβ(π΄ βͺ π΅)) = ((cardβπ΄) +o (cardβπ΅))) | ||
Theorem | ficardun2 10197 | The cardinality of the union of finite sets is at most the ordinal sum of their cardinalities. (Contributed by Mario Carneiro, 5-Feb-2013.) Avoid ax-rep 5286. (Revised by BTernaryTau, 3-Jul-2024.) |
β’ ((π΄ β Fin β§ π΅ β Fin) β (cardβ(π΄ βͺ π΅)) β ((cardβπ΄) +o (cardβπ΅))) | ||
Theorem | ficardun2OLD 10198 | Obsolete version of ficardun2 10197 as of 3-Jul-2024. (Contributed by Mario Carneiro, 5-Feb-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β Fin β§ π΅ β Fin) β (cardβ(π΄ βͺ π΅)) β ((cardβπ΄) +o (cardβπ΅))) | ||
Theorem | pwsdompw 10199* | Lemma for domtriom 10438. This is the equinumerosity version of the algebraic identity Ξ£π β π(2βπ) = (2βπ) β 1. (Contributed by Mario Carneiro, 7-Feb-2013.) |
β’ ((π β Ο β§ βπ β suc π(π΅βπ) β π« π) β βͺ π β π (π΅βπ) βΊ (π΅βπ)) | ||
Theorem | unctb 10200 | The union of two countable sets is countable. (Contributed by FL, 25-Aug-2006.) (Proof shortened by Mario Carneiro, 30-Apr-2015.) |
β’ ((π΄ βΌ Ο β§ π΅ βΌ Ο) β (π΄ βͺ π΅) βΌ Ο) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |