![]() |
Metamath
Proof Explorer Theorem List (p. 426 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | jm3.1lem3 42501 | Lemma for jm3.1 42502. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
β’ (π β π΄ β (β€β₯β2)) & β’ (π β πΎ β (β€β₯β2)) & β’ (π β π β β) & β’ (π β (πΎ Yrm (π + 1)) β€ π΄) β β’ (π β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β β) | ||
Theorem | jm3.1 42502 | Diophantine expression for exponentiation. Lemma 3.1 of [JonesMatijasevic] p. 698. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
β’ (((π΄ β (β€β₯β2) β§ πΎ β (β€β₯β2) β§ π β β) β§ (πΎ Yrm (π + 1)) β€ π΄) β (πΎβπ) = (((π΄ Xrm π) β ((π΄ β πΎ) Β· (π΄ Yrm π))) mod ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1))) | ||
Theorem | expdiophlem1 42503* | Lemma for expdioph 42505. Fully expanded expression for exponential. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
β’ (πΆ β β0 β (((π΄ β (β€β₯β2) β§ π΅ β β) β§ πΆ = (π΄βπ΅)) β βπ β β0 βπ β β0 βπ β β0 ((π΄ β (β€β₯β2) β§ π΅ β β) β§ ((π΄ β (β€β₯β2) β§ π = (π΄ Yrm (π΅ + 1))) β§ ((π β (β€β₯β2) β§ π = (π Yrm π΅)) β§ ((π β (β€β₯β2) β§ π = (π Xrm π΅)) β§ (πΆ < ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β§ ((((2 Β· π) Β· π΄) β (π΄β2)) β 1) β₯ ((π β ((π β π΄) Β· π)) β πΆ)))))))) | ||
Theorem | expdiophlem2 42504 | Lemma for expdioph 42505. Exponentiation on a restricted domain is Diophantine. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
β’ {π β (β0 βm (1...3)) β£ (((πβ1) β (β€β₯β2) β§ (πβ2) β β) β§ (πβ3) = ((πβ1)β(πβ2)))} β (Diophβ3) | ||
Theorem | expdioph 42505 | The exponential function is Diophantine. This result completes and encapsulates our development using Pell equation solution sequences and is sometimes regarded as Matiyasevich's theorem properly. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
β’ {π β (β0 βm (1...3)) β£ (πβ3) = ((πβ1)β(πβ2))} β (Diophβ3) | ||
Theorem | setindtr 42506* | Set induction for sets contained in a transitive set. If we are allowed to assume Infinity, then all sets have a transitive closure and this reduces to setind 9752; however, this version is useful without Infinity. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
β’ (βπ₯(π₯ β π΄ β π₯ β π΄) β (βπ¦(Tr π¦ β§ π΅ β π¦) β π΅ β π΄)) | ||
Theorem | setindtrs 42507* | Set induction scheme without Infinity. See comments at setindtr 42506. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
β’ (βπ¦ β π₯ π β π) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = π΅ β (π β π)) β β’ (βπ§(Tr π§ β§ π΅ β π§) β π) | ||
Theorem | dford3lem1 42508* | Lemma for dford3 42510. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
β’ ((Tr π β§ βπ¦ β π Tr π¦) β βπ β π (Tr π β§ βπ¦ β π Tr π¦)) | ||
Theorem | dford3lem2 42509* | Lemma for dford3 42510. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
β’ ((Tr π₯ β§ βπ¦ β π₯ Tr π¦) β π₯ β On) | ||
Theorem | dford3 42510* | Ordinals are precisely the hereditarily transitive classes. Definition 1.2 of [Schloeder] p. 1. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
β’ (Ord π β (Tr π β§ βπ₯ β π Tr π₯)) | ||
Theorem | dford4 42511* | dford3 42510 expressed in primitives to demonstrate shortness. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
β’ (Ord π β βπβπβπ((π β π β§ π β π) β (π β π β§ (π β π β π β π)))) | ||
Theorem | wopprc 42512 | Unrelated: Wiener pairs treat proper classes symmetrically. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
β’ ((π΄ β V β§ π΅ β V) β Β¬ 1o β {{{π΄}, β }, {{π΅}}}) | ||
Theorem | rpnnen3lem 42513* | Lemma for rpnnen3 42514. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ (((π β β β§ π β β) β§ π < π) β {π β β β£ π < π} β {π β β β£ π < π}) | ||
Theorem | rpnnen3 42514 | Dedekind cut injection of β into π« β. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ β βΌ π« β | ||
Theorem | axac10 42515 | Characterization of choice similar to dffin1-5 10406. (Contributed by Stefan O'Rear, 6-Jan-2015.) |
β’ ( β β On) = V | ||
Theorem | harinf 42516 | The Hartogs number of an infinite set is at least Ο. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) |
β’ ((π β π β§ Β¬ π β Fin) β Ο β (harβπ)) | ||
Theorem | wdom2d2 42517* | Deduction for weak dominance by a Cartesian product. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ ((π β§ π₯ β π΄) β βπ¦ β π΅ βπ§ β πΆ π₯ = π) β β’ (π β π΄ βΌ* (π΅ Γ πΆ)) | ||
Theorem | ttac 42518 | Tarski's theorem about choice: infxpidm 10580 is equivalent to ax-ac 10477. (Contributed by Stefan O'Rear, 4-Nov-2014.) (Proof shortened by Stefan O'Rear, 10-Jul-2015.) |
β’ (CHOICE β βπ(Ο βΌ π β (π Γ π) β π)) | ||
Theorem | pw2f1ocnv 42519* | Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en 9097, which can be easily reproved in terms of this. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Stefan O'Rear, 9-Jul-2015.) |
β’ πΉ = (π₯ β (2o βm π΄) β¦ (β‘π₯ β {1o})) β β’ (π΄ β π β (πΉ:(2o βm π΄)β1-1-ontoβπ« π΄ β§ β‘πΉ = (π¦ β π« π΄ β¦ (π§ β π΄ β¦ if(π§ β π¦, 1o, β ))))) | ||
Theorem | pw2f1o2 42520* | Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en 9097, which can be easily reproved in terms of this. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ πΉ = (π₯ β (2o βm π΄) β¦ (β‘π₯ β {1o})) β β’ (π΄ β π β πΉ:(2o βm π΄)β1-1-ontoβπ« π΄) | ||
Theorem | pw2f1o2val 42521* | Function value of the pw2f1o2 42520 bijection. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.) |
β’ πΉ = (π₯ β (2o βm π΄) β¦ (β‘π₯ β {1o})) β β’ (π β (2o βm π΄) β (πΉβπ) = (β‘π β {1o})) | ||
Theorem | pw2f1o2val2 42522* | Membership in a mapped set under the pw2f1o2 42520 bijection. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.) |
β’ πΉ = (π₯ β (2o βm π΄) β¦ (β‘π₯ β {1o})) β β’ ((π β (2o βm π΄) β§ π β π΄) β (π β (πΉβπ) β (πβπ) = 1o)) | ||
Theorem | soeq12d 42523 | Equality deduction for total orderings. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
β’ (π β π = π) & β’ (π β π΄ = π΅) β β’ (π β (π Or π΄ β π Or π΅)) | ||
Theorem | freq12d 42524 | Equality deduction for founded relations. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
β’ (π β π = π) & β’ (π β π΄ = π΅) β β’ (π β (π Fr π΄ β π Fr π΅)) | ||
Theorem | weeq12d 42525 | Equality deduction for well-orders. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
β’ (π β π = π) & β’ (π β π΄ = π΅) β β’ (π β (π We π΄ β π We π΅)) | ||
Theorem | limsuc2 42526 | Limit ordinals in the sense inclusive of zero contain all successors of their members. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
β’ ((Ord π΄ β§ π΄ = βͺ π΄) β (π΅ β π΄ β suc π΅ β π΄)) | ||
Theorem | wepwsolem 42527* | Transfer an ordering on characteristic functions by isomorphism to the power set. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ π = {β¨π₯, π¦β© β£ βπ§ β π΄ ((π§ β π¦ β§ Β¬ π§ β π₯) β§ βπ€ β π΄ (π€π π§ β (π€ β π₯ β π€ β π¦)))} & β’ π = {β¨π₯, π¦β© β£ βπ§ β π΄ ((π₯βπ§) E (π¦βπ§) β§ βπ€ β π΄ (π€π π§ β (π₯βπ€) = (π¦βπ€)))} & β’ πΉ = (π β (2o βm π΄) β¦ (β‘π β {1o})) β β’ (π΄ β V β πΉ Isom π, π ((2o βm π΄), π« π΄)) | ||
Theorem | wepwso 42528* | A well-ordering induces a strict ordering on the power set. EDITORIAL: when well-orderings are set like, this can be strengthened to remove π΄ β π. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ π = {β¨π₯, π¦β© β£ βπ§ β π΄ ((π§ β π¦ β§ Β¬ π§ β π₯) β§ βπ€ β π΄ (π€π π§ β (π€ β π₯ β π€ β π¦)))} β β’ ((π΄ β π β§ π We π΄) β π Or π« π΄) | ||
Theorem | dnnumch1 42529* | Define an enumeration of a set from a choice function; second part, it restricts to a bijection. EDITORIAL: overlaps dfac8a 10048. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ πΉ = recs((π§ β V β¦ (πΊβ(π΄ β ran π§)))) & β’ (π β π΄ β π) & β’ (π β βπ¦ β π« π΄(π¦ β β β (πΊβπ¦) β π¦)) β β’ (π β βπ₯ β On (πΉ βΎ π₯):π₯β1-1-ontoβπ΄) | ||
Theorem | dnnumch2 42530* | Define an enumeration (weak dominance version) of a set from a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ πΉ = recs((π§ β V β¦ (πΊβ(π΄ β ran π§)))) & β’ (π β π΄ β π) & β’ (π β βπ¦ β π« π΄(π¦ β β β (πΊβπ¦) β π¦)) β β’ (π β π΄ β ran πΉ) | ||
Theorem | dnnumch3lem 42531* | Value of the ordinal injection function. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ πΉ = recs((π§ β V β¦ (πΊβ(π΄ β ran π§)))) & β’ (π β π΄ β π) & β’ (π β βπ¦ β π« π΄(π¦ β β β (πΊβπ¦) β π¦)) β β’ ((π β§ π€ β π΄) β ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€) = β© (β‘πΉ β {π€})) | ||
Theorem | dnnumch3 42532* | Define an injection from a set into the ordinals using a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ πΉ = recs((π§ β V β¦ (πΊβ(π΄ β ran π§)))) & β’ (π β π΄ β π) & β’ (π β βπ¦ β π« π΄(π¦ β β β (πΊβπ¦) β π¦)) β β’ (π β (π₯ β π΄ β¦ β© (β‘πΉ β {π₯})):π΄β1-1βOn) | ||
Theorem | dnwech 42533* | Define a well-ordering from a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ πΉ = recs((π§ β V β¦ (πΊβ(π΄ β ran π§)))) & β’ (π β π΄ β π) & β’ (π β βπ¦ β π« π΄(π¦ β β β (πΊβπ¦) β π¦)) & β’ π» = {β¨π£, π€β© β£ β© (β‘πΉ β {π£}) β β© (β‘πΉ β {π€})} β β’ (π β π» We π΄) | ||
Theorem | fnwe2val 42534* | Lemma for fnwe2 42538. Substitute variables. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
β’ (π§ = (πΉβπ₯) β π = π) & β’ π = {β¨π₯, π¦β© β£ ((πΉβπ₯)π (πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦))} β β’ (πππ β ((πΉβπ)π (πΉβπ) β¨ ((πΉβπ) = (πΉβπ) β§ πβ¦(πΉβπ) / π§β¦ππ))) | ||
Theorem | fnwe2lem1 42535* | Lemma for fnwe2 42538. Substitution in well-ordering hypothesis. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
β’ (π§ = (πΉβπ₯) β π = π) & β’ π = {β¨π₯, π¦β© β£ ((πΉβπ₯)π (πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦))} & β’ ((π β§ π₯ β π΄) β π We {π¦ β π΄ β£ (πΉβπ¦) = (πΉβπ₯)}) β β’ ((π β§ π β π΄) β β¦(πΉβπ) / π§β¦π We {π¦ β π΄ β£ (πΉβπ¦) = (πΉβπ)}) | ||
Theorem | fnwe2lem2 42536* | Lemma for fnwe2 42538. An element which is in a minimal fiber and minimal within its fiber is minimal globally; thus π is well-founded. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
β’ (π§ = (πΉβπ₯) β π = π) & β’ π = {β¨π₯, π¦β© β£ ((πΉβπ₯)π (πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦))} & β’ ((π β§ π₯ β π΄) β π We {π¦ β π΄ β£ (πΉβπ¦) = (πΉβπ₯)}) & β’ (π β (πΉ βΎ π΄):π΄βΆπ΅) & β’ (π β π We π΅) & β’ (π β π β π΄) & β’ (π β π β β ) β β’ (π β βπ β π βπ β π Β¬ πππ) | ||
Theorem | fnwe2lem3 42537* | Lemma for fnwe2 42538. Trichotomy. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
β’ (π§ = (πΉβπ₯) β π = π) & β’ π = {β¨π₯, π¦β© β£ ((πΉβπ₯)π (πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦))} & β’ ((π β§ π₯ β π΄) β π We {π¦ β π΄ β£ (πΉβπ¦) = (πΉβπ₯)}) & β’ (π β (πΉ βΎ π΄):π΄βΆπ΅) & β’ (π β π We π΅) & β’ (π β π β π΄) & β’ (π β π β π΄) β β’ (π β (πππ β¨ π = π β¨ πππ)) | ||
Theorem | fnwe2 42538* | A well-ordering can be constructed on a partitioned set by patching together well-orderings on each partition using a well-ordering on the partitions themselves. Similar to fnwe 8130 but does not require the within-partition ordering to be globally well. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
β’ (π§ = (πΉβπ₯) β π = π) & β’ π = {β¨π₯, π¦β© β£ ((πΉβπ₯)π (πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦))} & β’ ((π β§ π₯ β π΄) β π We {π¦ β π΄ β£ (πΉβπ¦) = (πΉβπ₯)}) & β’ (π β (πΉ βΎ π΄):π΄βΆπ΅) & β’ (π β π We π΅) β β’ (π β π We π΄) | ||
Theorem | aomclem1 42539* |
Lemma for dfac11 42547. This is the beginning of the proof that
multiple
choice is equivalent to choice. Our goal is to construct, by
transfinite recursion, a well-ordering of (π
1βπ΄). In what
follows, π΄ is the index of the rank we wish to
well-order, π§ is
the collection of well-orderings constructed so far, dom π§ is
the
set of ordinal indices of constructed ranks i.e. the next rank to
construct, and π¦ is a postulated multiple-choice
function.
Successor case 1, define a simple ordering from the well-ordered predecessor. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ π΅ = {β¨π, πβ© β£ βπ β (π 1ββͺ dom π§)((π β π β§ Β¬ π β π) β§ βπ β (π 1ββͺ dom π§)(π(π§ββͺ dom π§)π β (π β π β π β π)))} & β’ (π β dom π§ β On) & β’ (π β dom π§ = suc βͺ dom π§) & β’ (π β βπ β dom π§(π§βπ) We (π 1βπ)) β β’ (π β π΅ Or (π 1βdom π§)) | ||
Theorem | aomclem2 42540* | Lemma for dfac11 42547. Successor case 2, a choice function for subsets of (π 1βdom π§). (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ π΅ = {β¨π, πβ© β£ βπ β (π 1ββͺ dom π§)((π β π β§ Β¬ π β π) β§ βπ β (π 1ββͺ dom π§)(π(π§ββͺ dom π§)π β (π β π β π β π)))} & β’ πΆ = (π β V β¦ sup((π¦βπ), (π 1βdom π§), π΅)) & β’ (π β dom π§ β On) & β’ (π β dom π§ = suc βͺ dom π§) & β’ (π β βπ β dom π§(π§βπ) We (π 1βπ)) & β’ (π β π΄ β On) & β’ (π β dom π§ β π΄) & β’ (π β βπ β π« (π 1βπ΄)(π β β β (π¦βπ) β ((π« π β© Fin) β {β }))) β β’ (π β βπ β π« (π 1βdom π§)(π β β β (πΆβπ) β π)) | ||
Theorem | aomclem3 42541* | Lemma for dfac11 42547. Successor case 3, our required well-ordering. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
β’ π΅ = {β¨π, πβ© β£ βπ β (π 1ββͺ dom π§)((π β π β§ Β¬ π β π) β§ βπ β (π 1ββͺ dom π§)(π(π§ββͺ dom π§)π β (π β π β π β π)))} & β’ πΆ = (π β V β¦ sup((π¦βπ), (π 1βdom π§), π΅)) & β’ π· = recs((π β V β¦ (πΆβ((π 1βdom π§) β ran π)))) & β’ πΈ = {β¨π, πβ© β£ β© (β‘π· β {π}) β β© (β‘π· β {π})} & β’ (π β dom π§ β On) & β’ (π β dom π§ = suc βͺ dom π§) & β’ (π β βπ β dom π§(π§βπ) We (π 1βπ)) & β’ (π β π΄ β On) & β’ (π β dom π§ β π΄) & β’ (π β βπ β π« (π 1βπ΄)(π β β β (π¦βπ) β ((π« π β© Fin) β {β }))) β β’ (π β πΈ We (π 1βdom π§)) | ||
Theorem | aomclem4 42542* | Lemma for dfac11 42547. Limit case. Patch together well-orderings constructed so far using fnwe2 42538 to cover the limit rank. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
β’ πΉ = {β¨π, πβ© β£ ((rankβπ) E (rankβπ) β¨ ((rankβπ) = (rankβπ) β§ π(π§βsuc (rankβπ))π))} & β’ (π β dom π§ β On) & β’ (π β dom π§ = βͺ dom π§) & β’ (π β βπ β dom π§(π§βπ) We (π 1βπ)) β β’ (π β πΉ We (π 1βdom π§)) | ||
Theorem | aomclem5 42543* | Lemma for dfac11 42547. Combine the successor case with the limit case. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
β’ π΅ = {β¨π, πβ© β£ βπ β (π 1ββͺ dom π§)((π β π β§ Β¬ π β π) β§ βπ β (π 1ββͺ dom π§)(π(π§ββͺ dom π§)π β (π β π β π β π)))} & β’ πΆ = (π β V β¦ sup((π¦βπ), (π 1βdom π§), π΅)) & β’ π· = recs((π β V β¦ (πΆβ((π 1βdom π§) β ran π)))) & β’ πΈ = {β¨π, πβ© β£ β© (β‘π· β {π}) β β© (β‘π· β {π})} & β’ πΉ = {β¨π, πβ© β£ ((rankβπ) E (rankβπ) β¨ ((rankβπ) = (rankβπ) β§ π(π§βsuc (rankβπ))π))} & β’ πΊ = (if(dom π§ = βͺ dom π§, πΉ, πΈ) β© ((π 1βdom π§) Γ (π 1βdom π§))) & β’ (π β dom π§ β On) & β’ (π β βπ β dom π§(π§βπ) We (π 1βπ)) & β’ (π β π΄ β On) & β’ (π β dom π§ β π΄) & β’ (π β βπ β π« (π 1βπ΄)(π β β β (π¦βπ) β ((π« π β© Fin) β {β }))) β β’ (π β πΊ We (π 1βdom π§)) | ||
Theorem | aomclem6 42544* | Lemma for dfac11 42547. Transfinite induction, close over π§. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
β’ π΅ = {β¨π, πβ© β£ βπ β (π 1ββͺ dom π§)((π β π β§ Β¬ π β π) β§ βπ β (π 1ββͺ dom π§)(π(π§ββͺ dom π§)π β (π β π β π β π)))} & β’ πΆ = (π β V β¦ sup((π¦βπ), (π 1βdom π§), π΅)) & β’ π· = recs((π β V β¦ (πΆβ((π 1βdom π§) β ran π)))) & β’ πΈ = {β¨π, πβ© β£ β© (β‘π· β {π}) β β© (β‘π· β {π})} & β’ πΉ = {β¨π, πβ© β£ ((rankβπ) E (rankβπ) β¨ ((rankβπ) = (rankβπ) β§ π(π§βsuc (rankβπ))π))} & β’ πΊ = (if(dom π§ = βͺ dom π§, πΉ, πΈ) β© ((π 1βdom π§) Γ (π 1βdom π§))) & β’ π» = recs((π§ β V β¦ πΊ)) & β’ (π β π΄ β On) & β’ (π β βπ β π« (π 1βπ΄)(π β β β (π¦βπ) β ((π« π β© Fin) β {β }))) β β’ (π β (π»βπ΄) We (π 1βπ΄)) | ||
Theorem | aomclem7 42545* | Lemma for dfac11 42547. (π 1βπ΄) is well-orderable. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
β’ π΅ = {β¨π, πβ© β£ βπ β (π 1ββͺ dom π§)((π β π β§ Β¬ π β π) β§ βπ β (π 1ββͺ dom π§)(π(π§ββͺ dom π§)π β (π β π β π β π)))} & β’ πΆ = (π β V β¦ sup((π¦βπ), (π 1βdom π§), π΅)) & β’ π· = recs((π β V β¦ (πΆβ((π 1βdom π§) β ran π)))) & β’ πΈ = {β¨π, πβ© β£ β© (β‘π· β {π}) β β© (β‘π· β {π})} & β’ πΉ = {β¨π, πβ© β£ ((rankβπ) E (rankβπ) β¨ ((rankβπ) = (rankβπ) β§ π(π§βsuc (rankβπ))π))} & β’ πΊ = (if(dom π§ = βͺ dom π§, πΉ, πΈ) β© ((π 1βdom π§) Γ (π 1βdom π§))) & β’ π» = recs((π§ β V β¦ πΊ)) & β’ (π β π΄ β On) & β’ (π β βπ β π« (π 1βπ΄)(π β β β (π¦βπ) β ((π« π β© Fin) β {β }))) β β’ (π β βπ π We (π 1βπ΄)) | ||
Theorem | aomclem8 42546* | Lemma for dfac11 42547. Perform variable substitutions. This is the most we can say without invoking regularity. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
β’ (π β π΄ β On) & β’ (π β βπ β π« (π 1βπ΄)(π β β β (π¦βπ) β ((π« π β© Fin) β {β }))) β β’ (π β βπ π We (π 1βπ΄)) | ||
Theorem | dfac11 42547* |
The right-hand side of this theorem (compare with ac4 10493),
sometimes
known as the "axiom of multiple choice", is a choice
equivalent.
Curiously, this statement cannot be proved without ax-reg 9610, despite
not mentioning the cumulative hierarchy in any way as most consequences
of regularity do.
This is definition (MC) of [Schechter] p. 141. EDITORIAL: the proof is not original with me of course but I lost my reference sometime after writing it. A multiple choice function allows any total order to be extended to a choice function, which in turn defines a well-ordering. Since a well-ordering on a set defines a simple ordering of the power set, this allows the trivial well-ordering of the empty set to be transfinitely bootstrapped up the cumulative hierarchy to any desired level. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Stefan O'Rear, 1-Jun-2015.) |
β’ (CHOICE β βπ₯βπβπ§ β π₯ (π§ β β β (πβπ§) β ((π« π§ β© Fin) β {β }))) | ||
Theorem | kelac1 42548* | Kelley's choice, basic form: if a collection of sets can be cast as closed sets in the factors of a topology, and there is a definable element in each topology (which need not be in the closed set - if it were this would be trivial), then compactness (via finite intersection) guarantees that the final product is nonempty. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ ((π β§ π₯ β πΌ) β π β β ) & β’ ((π β§ π₯ β πΌ) β π½ β Top) & β’ ((π β§ π₯ β πΌ) β πΆ β (Clsdβπ½)) & β’ ((π β§ π₯ β πΌ) β π΅:πβ1-1-ontoβπΆ) & β’ ((π β§ π₯ β πΌ) β π β βͺ π½) & β’ (π β (βtβ(π₯ β πΌ β¦ π½)) β Comp) β β’ (π β Xπ₯ β πΌ π β β ) | ||
Theorem | kelac2lem 42549 | Lemma for kelac2 42550 and dfac21 42551: knob topologies are compact. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ (π β π β (topGenβ{π, {π« βͺ π}}) β Comp) | ||
Theorem | kelac2 42550* | Kelley's choice, most common form: compactness of a product of knob topologies recovers choice. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ ((π β§ π₯ β πΌ) β π β π) & β’ ((π β§ π₯ β πΌ) β π β β ) & β’ (π β (βtβ(π₯ β πΌ β¦ (topGenβ{π, {π« βͺ π}}))) β Comp) β β’ (π β Xπ₯ β πΌ π β β ) | ||
Theorem | dfac21 42551 | Tychonoff's theorem is a choice equivalent. Definition AC21 of Schechter p. 461. (Contributed by Stefan O'Rear, 22-Feb-2015.) (Revised by Mario Carneiro, 27-Aug-2015.) |
β’ (CHOICE β βπ(π:dom πβΆComp β (βtβπ) β Comp)) | ||
Syntax | clfig 42552 | Extend class notation with the class of finitely generated left modules. |
class LFinGen | ||
Definition | df-lfig 42553 | Define the class of finitely generated left modules. Finite generation of subspaces can be intepreted using βΎs. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ LFinGen = {π€ β LMod β£ (Baseβπ€) β ((LSpanβπ€) β (π« (Baseβπ€) β© Fin))} | ||
Theorem | islmodfg 42554* | Property of a finitely generated left module. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π΅ = (Baseβπ) & β’ π = (LSpanβπ) β β’ (π β LMod β (π β LFinGen β βπ β π« π΅(π β Fin β§ (πβπ) = π΅))) | ||
Theorem | islssfg 42555* | Property of a finitely generated left (sub)module. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (π β LFinGen β βπ β π« π(π β Fin β§ (πβπ) = π))) | ||
Theorem | islssfg2 42556* | Property of a finitely generated left (sub)module, with a relaxed constraint on the spanning vectors. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ π΅ = (Baseβπ) β β’ ((π β LMod β§ π β π) β (π β LFinGen β βπ β (π« π΅ β© Fin)(πβπ) = π)) | ||
Theorem | islssfgi 42557 | Finitely spanned subspaces are finitely generated. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (LSpanβπ) & β’ π = (Baseβπ) & β’ π = (π βΎs (πβπ΅)) β β’ ((π β LMod β§ π΅ β π β§ π΅ β Fin) β π β LFinGen) | ||
Theorem | fglmod 42558 | Finitely generated left modules are left modules. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ (π β LFinGen β π β LMod) | ||
Theorem | lsmfgcl 42559 | The sum of two finitely generated submodules is finitely generated. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π· = (π βΎs π΄) & β’ πΈ = (π βΎs π΅) & β’ πΉ = (π βΎs (π΄ β π΅)) & β’ (π β π β LMod) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π· β LFinGen) & β’ (π β πΈ β LFinGen) β β’ (π β πΉ β LFinGen) | ||
Syntax | clnm 42560 | Extend class notation with the class of Noetherian left modules. |
class LNoeM | ||
Definition | df-lnm 42561* | A left-module is Noetherian iff it is hereditarily finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
β’ LNoeM = {π€ β LMod β£ βπ β (LSubSpβπ€)(π€ βΎs π) β LFinGen} | ||
Theorem | islnm 42562* | Property of being a Noetherian left module. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
β’ π = (LSubSpβπ) β β’ (π β LNoeM β (π β LMod β§ βπ β π (π βΎs π) β LFinGen)) | ||
Theorem | islnm2 42563* | Property of being a Noetherian left module with finite generation expanded in terms of spans. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π΅ = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ (π β LNoeM β (π β LMod β§ βπ β π βπ β (π« π΅ β© Fin)π = (πβπ))) | ||
Theorem | lnmlmod 42564 | A Noetherian left module is a left module. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
β’ (π β LNoeM β π β LMod) | ||
Theorem | lnmlssfg 42565 | A submodule of Noetherian module is finitely generated. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ π = (π βΎs π) β β’ ((π β LNoeM β§ π β π) β π β LFinGen) | ||
Theorem | lnmlsslnm 42566 | All submodules of a Noetherian module are Noetherian. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ π = (π βΎs π) β β’ ((π β LNoeM β§ π β π) β π β LNoeM) | ||
Theorem | lnmfg 42567 | A Noetherian left module is finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
β’ (π β LNoeM β π β LFinGen) | ||
Theorem | kercvrlsm 42568 | The domain of a linear function is the subspace sum of the kernel and any subspace which covers the range. (Contributed by Stefan O'Rear, 24-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ 0 = (0gβπ) & β’ πΎ = (β‘πΉ β { 0 }) & β’ π΅ = (Baseβπ) & β’ (π β πΉ β (π LMHom π)) & β’ (π β π· β π) & β’ (π β (πΉ β π·) = ran πΉ) β β’ (π β (πΎ β π·) = π΅) | ||
Theorem | lmhmfgima 42569 | A homomorphism maps finitely generated submodules to finitely generated submodules. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βΎs (πΉ β π΄)) & β’ π = (π βΎs π΄) & β’ π = (LSubSpβπ) & β’ (π β π β LFinGen) & β’ (π β π΄ β π) & β’ (π β πΉ β (π LMHom π)) β β’ (π β π β LFinGen) | ||
Theorem | lnmepi 42570 | Epimorphic images of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π΅ = (Baseβπ) β β’ ((πΉ β (π LMHom π) β§ π β LNoeM β§ ran πΉ = π΅) β π β LNoeM) | ||
Theorem | lmhmfgsplit 42571 | If the kernel and range of a homomorphism of left modules are finitely generated, then so is the domain. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.) |
β’ 0 = (0gβπ) & β’ πΎ = (β‘πΉ β { 0 }) & β’ π = (π βΎs πΎ) & β’ π = (π βΎs ran πΉ) β β’ ((πΉ β (π LMHom π) β§ π β LFinGen β§ π β LFinGen) β π β LFinGen) | ||
Theorem | lmhmlnmsplit 42572 | If the kernel and range of a homomorphism of left modules are Noetherian, then so is the domain. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Revised by Stefan O'Rear, 12-Jun-2015.) |
β’ 0 = (0gβπ) & β’ πΎ = (β‘πΉ β { 0 }) & β’ π = (π βΎs πΎ) & β’ π = (π βΎs ran πΉ) β β’ ((πΉ β (π LMHom π) β§ π β LNoeM β§ π β LNoeM) β π β LNoeM) | ||
Theorem | lnmlmic 42573 | Noetherian is an invariant property of modules. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (π βπ π β (π β LNoeM β π β LNoeM)) | ||
Theorem | pwssplit4 42574* | Splitting for structure powers 4: maps isomorphically onto the other half. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ πΈ = (π βs (π΄ βͺ π΅)) & β’ πΊ = (BaseβπΈ) & β’ 0 = (0gβπ ) & β’ πΎ = {π¦ β πΊ β£ (π¦ βΎ π΄) = (π΄ Γ { 0 })} & β’ πΉ = (π₯ β πΎ β¦ (π₯ βΎ π΅)) & β’ πΆ = (π βs π΄) & β’ π· = (π βs π΅) & β’ πΏ = (πΈ βΎs πΎ) β β’ ((π β LMod β§ (π΄ βͺ π΅) β π β§ (π΄ β© π΅) = β ) β πΉ β (πΏ LMIso π·)) | ||
Theorem | filnm 42575 | Finite left modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π΅ = (Baseβπ) β β’ ((π β LMod β§ π΅ β Fin) β π β LNoeM) | ||
Theorem | pwslnmlem0 42576 | Zeroeth powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs β ) β β’ (π β LMod β π β LNoeM) | ||
Theorem | pwslnmlem1 42577* | First powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs {π}) β β’ (π β LNoeM β π β LNoeM) | ||
Theorem | pwslnmlem2 42578 | A sum of powers is Noetherian. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ π΄ β V & β’ π΅ β V & β’ π = (π βs π΄) & β’ π = (π βs π΅) & β’ π = (π βs (π΄ βͺ π΅)) & β’ (π β π β LMod) & β’ (π β (π΄ β© π΅) = β ) & β’ (π β π β LNoeM) & β’ (π β π β LNoeM) β β’ (π β π β LNoeM) | ||
Theorem | pwslnm 42579 | Finite powers of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs πΌ) β β’ ((π β LNoeM β§ πΌ β Fin) β π β LNoeM) | ||
Theorem | unxpwdom3 42580* | Weaker version of unxpwdom 9607 where a function is required only to be cancellative, not an injection. π· and π΅ are to be thought of as "large" "horizonal" sets, the others as "small". Because the operator is row-wise injective, but the whole row cannot inject into π΄, each row must hit an element of π΅; by column injectivity, each row can be identified in at least one way by the π΅ element that it hits and the column in which it is hit. (Contributed by Stefan O'Rear, 8-Jul-2015.) MOVABLE |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π· β π) & β’ ((π β§ π β πΆ β§ π β π·) β (π + π) β (π΄ βͺ π΅)) & β’ (((π β§ π β πΆ) β§ (π β π· β§ π β π·)) β ((π + π) = (π + π) β π = π)) & β’ (((π β§ π β π·) β§ (π β πΆ β§ π β πΆ)) β ((π + π) = (π + π) β π = π)) & β’ (π β Β¬ π· βΌ π΄) β β’ (π β πΆ βΌ* (π· Γ π΅)) | ||
Theorem | pwfi2f1o 42581* | The pw2f1o 9095 bijection relates finitely supported indicator functions on a two-element set to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) (Revised by AV, 14-Jun-2020.) |
β’ π = {π¦ β (2o βm π΄) β£ π¦ finSupp β } & β’ πΉ = (π₯ β π β¦ (β‘π₯ β {1o})) β β’ (π΄ β π β πΉ:πβ1-1-ontoβ(π« π΄ β© Fin)) | ||
Theorem | pwfi2en 42582* | Finitely supported indicator functions are equinumerous to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) (Revised by AV, 14-Jun-2020.) |
β’ π = {π¦ β (2o βm π΄) β£ π¦ finSupp β } β β’ (π΄ β π β π β (π« π΄ β© Fin)) | ||
Theorem | frlmpwfi 42583 | Formal linear combinations over Z/2Z are equivalent to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) (Proof shortened by AV, 14-Jun-2020.) |
β’ π = (β€/nβ€β2) & β’ π = (π freeLMod πΌ) & β’ π΅ = (Baseβπ) β β’ (πΌ β π β π΅ β (π« πΌ β© Fin)) | ||
Theorem | gicabl 42584 | Being Abelian is a group invariant. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.) |
β’ (πΊ βπ π» β (πΊ β Abel β π» β Abel)) | ||
Theorem | imasgim 42585 | A relabeling of the elements of a group induces an isomorphism to the relabeled group. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.) (Revised by Mario Carneiro, 11-Aug-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβ1-1-ontoβπ΅) & β’ (π β π β Grp) β β’ (π β πΉ β (π GrpIso π)) | ||
Theorem | isnumbasgrplem1 42586 | A set which is equipollent to the base set of a definable Abelian group is the base set of some (relabeled) Abelian group. (Contributed by Stefan O'Rear, 8-Jul-2015.) |
β’ π΅ = (Baseβπ ) β β’ ((π β Abel β§ πΆ β π΅) β πΆ β (Base β Abel)) | ||
Theorem | harn0 42587 | The Hartogs number of a set is never zero. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.) |
β’ (π β π β (harβπ) β β ) | ||
Theorem | numinfctb 42588 | A numerable infinite set contains a countable subset. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.) |
β’ ((π β dom card β§ Β¬ π β Fin) β Ο βΌ π) | ||
Theorem | isnumbasgrplem2 42589 | If the (to be thought of as disjoint, although the proof does not require this) union of a set and its Hartogs number supports a group structure (more generally, a cancellative magma), then the set must be numerable. (Contributed by Stefan O'Rear, 9-Jul-2015.) |
β’ ((π βͺ (harβπ)) β (Base β Grp) β π β dom card) | ||
Theorem | isnumbasgrplem3 42590 | Every nonempty numerable set can be given the structure of an Abelian group, either a finite cyclic group or a vector space over Z/2Z. (Contributed by Stefan O'Rear, 10-Jul-2015.) |
β’ ((π β dom card β§ π β β ) β π β (Base β Abel)) | ||
Theorem | isnumbasabl 42591 | A set is numerable iff it and its Hartogs number can be jointly given the structure of an Abelian group. (Contributed by Stefan O'Rear, 9-Jul-2015.) |
β’ (π β dom card β (π βͺ (harβπ)) β (Base β Abel)) | ||
Theorem | isnumbasgrp 42592 | A set is numerable iff it and its Hartogs number can be jointly given the structure of a group. (Contributed by Stefan O'Rear, 9-Jul-2015.) |
β’ (π β dom card β (π βͺ (harβπ)) β (Base β Grp)) | ||
Theorem | dfacbasgrp 42593 | A choice equivalent in abstract algebra: All nonempty sets admit a group structure. From http://mathoverflow.net/a/12988. (Contributed by Stefan O'Rear, 9-Jul-2015.) |
β’ (CHOICE β (Base β Grp) = (V β {β })) | ||
Syntax | clnr 42594 | Extend class notation with the class of left Noetherian rings. |
class LNoeR | ||
Definition | df-lnr 42595 | A ring is left-Noetherian iff it is Noetherian as a left module over itself. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ LNoeR = {π β Ring β£ (ringLModβπ) β LNoeM} | ||
Theorem | islnr 42596 | Property of a left-Noetherian ring. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ (π΄ β LNoeR β (π΄ β Ring β§ (ringLModβπ΄) β LNoeM)) | ||
Theorem | lnrring 42597 | Left-Noetherian rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ (π΄ β LNoeR β π΄ β Ring) | ||
Theorem | lnrlnm 42598 | Left-Noetherian rings have Noetherian associated modules. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ (π΄ β LNoeR β (ringLModβπ΄) β LNoeM) | ||
Theorem | islnr2 42599* | Property of being a left-Noetherian ring in terms of finite generation of ideals (the usual "pure ring theory" definition). (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π΅ = (Baseβπ ) & β’ π = (LIdealβπ ) & β’ π = (RSpanβπ ) β β’ (π β LNoeR β (π β Ring β§ βπ β π βπ β (π« π΅ β© Fin)π = (πβπ))) | ||
Theorem | islnr3 42600 | Relate left-Noetherian rings to Noetherian-type closure property of the left ideal system. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ π΅ = (Baseβπ ) & β’ π = (LIdealβπ ) β β’ (π β LNoeR β (π β Ring β§ π β (NoeACSβπ΅))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |