Home | Metamath
Proof Explorer Theorem List (p. 413 of 470) | < 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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | jm2.27dlem4 41201 | Lemma for rmydioph 41203. Infer β-hood of large numbers. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
β’ π΄ β β & β’ π΅ = (π΄ + 1) β β’ π΅ β β | ||
Theorem | jm2.27dlem5 41202 | Lemma for rmydioph 41203. Used with sselii 3939 to infer membership of midpoints of range; jm2.27dlem2 41199 is deprecated. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
β’ π΅ = (π΄ + 1) & β’ (1...π΅) β (1...πΆ) β β’ (1...π΄) β (1...πΆ) | ||
Theorem | rmydioph 41203 | jm2.27 41197 restated in terms of Diophantine sets. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.) |
β’ {π β (β0 βm (1...3)) β£ ((πβ1) β (β€β₯β2) β§ (πβ3) = ((πβ1) Yrm (πβ2)))} β (Diophβ3) | ||
Theorem | rmxdiophlem 41204* | X can be expressed in terms of Y, so it is also Diophantine. (Contributed by Stefan O'Rear, 15-Oct-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β0 β§ π β β0) β (π = (π΄ Xrm π) β βπ¦ β β0 (π¦ = (π΄ Yrm π) β§ ((πβ2) β (((π΄β2) β 1) Β· (π¦β2))) = 1))) | ||
Theorem | rmxdioph 41205 | X is a Diophantine function. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
β’ {π β (β0 βm (1...3)) β£ ((πβ1) β (β€β₯β2) β§ (πβ3) = ((πβ1) Xrm (πβ2)))} β (Diophβ3) | ||
Theorem | jm3.1lem1 41206 | Lemma for jm3.1 41209. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
β’ (π β π΄ β (β€β₯β2)) & β’ (π β πΎ β (β€β₯β2)) & β’ (π β π β β) & β’ (π β (πΎ Yrm (π + 1)) β€ π΄) β β’ (π β (πΎβπ) < π΄) | ||
Theorem | jm3.1lem2 41207 | Lemma for jm3.1 41209. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
β’ (π β π΄ β (β€β₯β2)) & β’ (π β πΎ β (β€β₯β2)) & β’ (π β π β β) & β’ (π β (πΎ Yrm (π + 1)) β€ π΄) β β’ (π β (πΎβπ) < ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1)) | ||
Theorem | jm3.1lem3 41208 | Lemma for jm3.1 41209. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
β’ (π β π΄ β (β€β₯β2)) & β’ (π β πΎ β (β€β₯β2)) & β’ (π β π β β) & β’ (π β (πΎ Yrm (π + 1)) β€ π΄) β β’ (π β ((((2 Β· π΄) Β· πΎ) β (πΎβ2)) β 1) β β) | ||
Theorem | jm3.1 41209 | 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 41210* | Lemma for expdioph 41212. 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 41211 | Lemma for expdioph 41212. 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 41212 | 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 41213* | 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 9603; however, this version is useful without Infinity. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
β’ (βπ₯(π₯ β π΄ β π₯ β π΄) β (βπ¦(Tr π¦ β§ π΅ β π¦) β π΅ β π΄)) | ||
Theorem | setindtrs 41214* | Set induction scheme without Infinity. See comments at setindtr 41213. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
β’ (βπ¦ β π₯ π β π) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = π΅ β (π β π)) β β’ (βπ§(Tr π§ β§ π΅ β π§) β π) | ||
Theorem | dford3lem1 41215* | Lemma for dford3 41217. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
β’ ((Tr π β§ βπ¦ β π Tr π¦) β βπ β π (Tr π β§ βπ¦ β π Tr π¦)) | ||
Theorem | dford3lem2 41216* | Lemma for dford3 41217. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
β’ ((Tr π₯ β§ βπ¦ β π₯ Tr π¦) β π₯ β On) | ||
Theorem | dford3 41217* | Ordinals are precisely the hereditarily transitive classes. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
β’ (Ord π β (Tr π β§ βπ₯ β π Tr π₯)) | ||
Theorem | dford4 41218* | dford3 41217 expressed in primitives to demonstrate shortness. (Contributed by Stefan O'Rear, 28-Oct-2014.) |
β’ (Ord π β βπβπβπ((π β π β§ π β π) β (π β π β§ (π β π β π β π)))) | ||
Theorem | wopprc 41219 | Unrelated: Wiener pairs treat proper classes symmetrically. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
β’ ((π΄ β V β§ π΅ β V) β Β¬ 1o β {{{π΄}, β }, {{π΅}}}) | ||
Theorem | rpnnen3lem 41220* | Lemma for rpnnen3 41221. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ (((π β β β§ π β β) β§ π < π) β {π β β β£ π < π} β {π β β β£ π < π}) | ||
Theorem | rpnnen3 41221 | Dedekind cut injection of β into π« β. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ β βΌ π« β | ||
Theorem | axac10 41222 | Characterization of choice similar to dffin1-5 10257. (Contributed by Stefan O'Rear, 6-Jan-2015.) |
β’ ( β β On) = V | ||
Theorem | harinf 41223 | The Hartogs number of an infinite set is at least Ο. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) |
β’ ((π β π β§ Β¬ π β Fin) β Ο β (harβπ)) | ||
Theorem | wdom2d2 41224* | Deduction for weak dominance by a Cartesian product. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ ((π β§ π₯ β π΄) β βπ¦ β π΅ βπ§ β πΆ π₯ = π) β β’ (π β π΄ βΌ* (π΅ Γ πΆ)) | ||
Theorem | ttac 41225 | Tarski's theorem about choice: infxpidm 10431 is equivalent to ax-ac 10328. (Contributed by Stefan O'Rear, 4-Nov-2014.) (Proof shortened by Stefan O'Rear, 10-Jul-2015.) |
β’ (CHOICE β βπ(Ο βΌ π β (π Γ π) β π)) | ||
Theorem | pw2f1ocnv 41226* | Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en 8956, 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 41227* | Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en 8956, 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 41228* | Function value of the pw2f1o2 41227 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 41229* | Membership in a mapped set under the pw2f1o2 41227 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 41230 | Equality deduction for total orderings. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
β’ (π β π = π) & β’ (π β π΄ = π΅) β β’ (π β (π Or π΄ β π Or π΅)) | ||
Theorem | freq12d 41231 | Equality deduction for founded relations. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
β’ (π β π = π) & β’ (π β π΄ = π΅) β β’ (π β (π Fr π΄ β π Fr π΅)) | ||
Theorem | weeq12d 41232 | Equality deduction for well-orders. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
β’ (π β π = π) & β’ (π β π΄ = π΅) β β’ (π β (π We π΄ β π We π΅)) | ||
Theorem | limsuc2 41233 | 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 41234* | 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 41235* | 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 41236* | Define an enumeration of a set from a choice function; second part, it restricts to a bijection. EDITORIAL: overlaps dfac8a 9899. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ πΉ = recs((π§ β V β¦ (πΊβ(π΄ β ran π§)))) & β’ (π β π΄ β π) & β’ (π β βπ¦ β π« π΄(π¦ β β β (πΊβπ¦) β π¦)) β β’ (π β βπ₯ β On (πΉ βΎ π₯):π₯β1-1-ontoβπ΄) | ||
Theorem | dnnumch2 41237* | 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 41238* | Value of the ordinal injection function. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ πΉ = recs((π§ β V β¦ (πΊβ(π΄ β ran π§)))) & β’ (π β π΄ β π) & β’ (π β βπ¦ β π« π΄(π¦ β β β (πΊβπ¦) β π¦)) β β’ ((π β§ π€ β π΄) β ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€) = β© (β‘πΉ β {π€})) | ||
Theorem | dnnumch3 41239* | 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 41240* | Define a well-ordering from a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
β’ πΉ = recs((π§ β V β¦ (πΊβ(π΄ β ran π§)))) & β’ (π β π΄ β π) & β’ (π β βπ¦ β π« π΄(π¦ β β β (πΊβπ¦) β π¦)) & β’ π» = {β¨π£, π€β© β£ β© (β‘πΉ β {π£}) β β© (β‘πΉ β {π€})} β β’ (π β π» We π΄) | ||
Theorem | fnwe2val 41241* | Lemma for fnwe2 41245. Substitute variables. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
β’ (π§ = (πΉβπ₯) β π = π) & β’ π = {β¨π₯, π¦β© β£ ((πΉβπ₯)π (πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦))} β β’ (πππ β ((πΉβπ)π (πΉβπ) β¨ ((πΉβπ) = (πΉβπ) β§ πβ¦(πΉβπ) / π§β¦ππ))) | ||
Theorem | fnwe2lem1 41242* | Lemma for fnwe2 41245. Substitution in well-ordering hypothesis. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
β’ (π§ = (πΉβπ₯) β π = π) & β’ π = {β¨π₯, π¦β© β£ ((πΉβπ₯)π (πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦))} & β’ ((π β§ π₯ β π΄) β π We {π¦ β π΄ β£ (πΉβπ¦) = (πΉβπ₯)}) β β’ ((π β§ π β π΄) β β¦(πΉβπ) / π§β¦π We {π¦ β π΄ β£ (πΉβπ¦) = (πΉβπ)}) | ||
Theorem | fnwe2lem2 41243* | Lemma for fnwe2 41245. 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 41244* | Lemma for fnwe2 41245. Trichotomy. (Contributed by Stefan O'Rear, 19-Jan-2015.) |
β’ (π§ = (πΉβπ₯) β π = π) & β’ π = {β¨π₯, π¦β© β£ ((πΉβπ₯)π (πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦))} & β’ ((π β§ π₯ β π΄) β π We {π¦ β π΄ β£ (πΉβπ¦) = (πΉβπ₯)}) & β’ (π β (πΉ βΎ π΄):π΄βΆπ΅) & β’ (π β π We π΅) & β’ (π β π β π΄) & β’ (π β π β π΄) β β’ (π β (πππ β¨ π = π β¨ πππ)) | ||
Theorem | fnwe2 41245* | 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 8052 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 41246* |
Lemma for dfac11 41254. 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 41247* | Lemma for dfac11 41254. 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 41248* | Lemma for dfac11 41254. 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 41249* | Lemma for dfac11 41254. Limit case. Patch together well-orderings constructed so far using fnwe2 41245 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 41250* | Lemma for dfac11 41254. 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 41251* | Lemma for dfac11 41254. 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 41252* | Lemma for dfac11 41254. (π 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 41253* | Lemma for dfac11 41254. 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 41254* |
The right-hand side of this theorem (compare with ac4 10344),
sometimes
known as the "axiom of multiple choice", is a choice
equivalent.
Curiously, this statement cannot be proved without ax-reg 9461, 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 41255* | 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 41256 | Lemma for kelac2 41257 and dfac21 41258: knob topologies are compact. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ (π β π β (topGenβ{π, {π« βͺ π}}) β Comp) | ||
Theorem | kelac2 41257* | 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 41258 | 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 41259 | Extend class notation with the class of finitely generated left modules. |
class LFinGen | ||
Definition | df-lfig 41260 | 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 41261* | Property of a finitely generated left module. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π΅ = (Baseβπ) & β’ π = (LSpanβπ) β β’ (π β LMod β (π β LFinGen β βπ β π« π΅(π β Fin β§ (πβπ) = π΅))) | ||
Theorem | islssfg 41262* | Property of a finitely generated left (sub)module. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (π β LFinGen β βπ β π« π(π β Fin β§ (πβπ) = π))) | ||
Theorem | islssfg2 41263* | 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 41264 | Finitely spanned subspaces are finitely generated. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (LSpanβπ) & β’ π = (Baseβπ) & β’ π = (π βΎs (πβπ΅)) β β’ ((π β LMod β§ π΅ β π β§ π΅ β Fin) β π β LFinGen) | ||
Theorem | fglmod 41265 | Finitely generated left modules are left modules. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ (π β LFinGen β π β LMod) | ||
Theorem | lsmfgcl 41266 | 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 41267 | Extend class notation with the class of Noetherian left modules. |
class LNoeM | ||
Definition | df-lnm 41268* | 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 41269* | Property of being a Noetherian left module. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
β’ π = (LSubSpβπ) β β’ (π β LNoeM β (π β LMod β§ βπ β π (π βΎs π) β LFinGen)) | ||
Theorem | islnm2 41270* | 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 41271 | A Noetherian left module is a left module. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
β’ (π β LNoeM β π β LMod) | ||
Theorem | lnmlssfg 41272 | A submodule of Noetherian module is finitely generated. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ π = (π βΎs π) β β’ ((π β LNoeM β§ π β π) β π β LFinGen) | ||
Theorem | lnmlsslnm 41273 | All submodules of a Noetherian module are Noetherian. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ π = (π βΎs π) β β’ ((π β LNoeM β§ π β π) β π β LNoeM) | ||
Theorem | lnmfg 41274 | A Noetherian left module is finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014.) |
β’ (π β LNoeM β π β LFinGen) | ||
Theorem | kercvrlsm 41275 | 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 41276 | 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 41277 | Epimorphic images of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π΅ = (Baseβπ) β β’ ((πΉ β (π LMHom π) β§ π β LNoeM β§ ran πΉ = π΅) β π β LNoeM) | ||
Theorem | lmhmfgsplit 41278 | 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 41279 | 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 41280 | Noetherian is an invariant property of modules. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (π βπ π β (π β LNoeM β π β LNoeM)) | ||
Theorem | pwssplit4 41281* | 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 41282 | Finite left modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π΅ = (Baseβπ) β β’ ((π β LMod β§ π΅ β Fin) β π β LNoeM) | ||
Theorem | pwslnmlem0 41283 | Zeroeth powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs β ) β β’ (π β LMod β π β LNoeM) | ||
Theorem | pwslnmlem1 41284* | First powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs {π}) β β’ (π β LNoeM β π β LNoeM) | ||
Theorem | pwslnmlem2 41285 | 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 41286 | Finite powers of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs πΌ) β β’ ((π β LNoeM β§ πΌ β Fin) β π β LNoeM) | ||
Theorem | unxpwdom3 41287* | Weaker version of unxpwdom 9458 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 41288* | The pw2f1o 8954 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 41289* | 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 41290 | 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 41291 | Being Abelian is a group invariant. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.) |
β’ (πΊ βπ π» β (πΊ β Abel β π» β Abel)) | ||
Theorem | imasgim 41292 | 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 41293 | 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 41294 | The Hartogs number of a set is never zero. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.) |
β’ (π β π β (harβπ) β β ) | ||
Theorem | numinfctb 41295 | A numerable infinite set contains a countable subset. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.) |
β’ ((π β dom card β§ Β¬ π β Fin) β Ο βΌ π) | ||
Theorem | isnumbasgrplem2 41296 | 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 41297 | 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 41298 | 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 41299 | 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 41300 | 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 β {β })) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |