![]() |
Metamath
Proof Explorer Theorem List (p. 363 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 | taupilemrplb 36201* | A set of positive reals has (in the reals) a lower bound. (Contributed by Jim Kingdon, 19-Feb-2019.) |
β’ βπ₯ β β βπ¦ β (β+ β© π΄)π₯ β€ π¦ | ||
Theorem | taupilem1 36202 | Lemma for taupi 36204. A positive real whose cosine is one is at least 2 Β· Ο. (Contributed by Jim Kingdon, 19-Feb-2019.) |
β’ ((π΄ β β+ β§ (cosβπ΄) = 1) β (2 Β· Ο) β€ π΄) | ||
Theorem | taupilem2 36203 | Lemma for taupi 36204. The smallest positive real whose cosine is one is at most 2 Β· Ο. (Contributed by Jim Kingdon, 19-Feb-2019.) (Revised by AV, 1-Oct-2020.) |
β’ Ο β€ (2 Β· Ο) | ||
Theorem | taupi 36204 | Relationship between Ο and Ο. This can be seen as connecting the ratio of a circle's circumference to its radius and the ratio of a circle's circumference to its diameter. (Contributed by Jim Kingdon, 19-Feb-2019.) (Revised by AV, 1-Oct-2020.) |
β’ Ο = (2 Β· Ο) | ||
Theorem | dfgcd3 36205* | Alternate definition of the gcd operator. (Contributed by Jim Kingdon, 31-Dec-2021.) |
β’ ((π β β€ β§ π β β€) β (π gcd π) = (β©π β β0 βπ§ β β€ (π§ β₯ π β (π§ β₯ π β§ π§ β₯ π)))) | ||
Theorem | irrdifflemf 36206 | Lemma for irrdiff 36207. The forward direction. (Contributed by Jim Kingdon, 20-May-2024.) |
β’ (π β π΄ β β) & β’ (π β Β¬ π΄ β β) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β π ) β β’ (π β (absβ(π΄ β π)) β (absβ(π΄ β π ))) | ||
Theorem | irrdiff 36207* | The irrationals are exactly those reals that are a different distance from every rational. (Contributed by Jim Kingdon, 19-May-2024.) |
β’ (π΄ β β β (Β¬ π΄ β β β βπ β β βπ β β (π β π β (absβ(π΄ β π)) β (absβ(π΄ β π))))) | ||
Theorem | iccioo01 36208 | The closed unit interval is equinumerous to the open unit interval. Based on a Mastodon post by Michael Kinyon. (Contributed by Jim Kingdon, 4-Jun-2024.) |
β’ (0[,]1) β (0(,)1) | ||
Theorem | csbrecsg 36209 | Move class substitution in and out of recs. (Contributed by ML, 25-Oct-2020.) |
β’ (π΄ β π β β¦π΄ / π₯β¦recs(πΉ) = recs(β¦π΄ / π₯β¦πΉ)) | ||
Theorem | csbrdgg 36210 | Move class substitution in and out of the recursive function generator. (Contributed by ML, 25-Oct-2020.) |
β’ (π΄ β π β β¦π΄ / π₯β¦rec(πΉ, πΌ) = rec(β¦π΄ / π₯β¦πΉ, β¦π΄ / π₯β¦πΌ)) | ||
Theorem | csboprabg 36211* | Move class substitution in and out of class abstractions of nested ordered pairs. (Contributed by ML, 25-Oct-2020.) |
β’ (π΄ β π β β¦π΄ / π₯β¦{β¨β¨π¦, π§β©, πβ© β£ π} = {β¨β¨π¦, π§β©, πβ© β£ [π΄ / π₯]π}) | ||
Theorem | csbmpo123 36212* | Move class substitution in and out of maps-to notation for operations. (Contributed by ML, 25-Oct-2020.) |
β’ (π΄ β π β β¦π΄ / π₯β¦(π¦ β π, π§ β π β¦ π·) = (π¦ β β¦π΄ / π₯β¦π, π§ β β¦π΄ / π₯β¦π β¦ β¦π΄ / π₯β¦π·)) | ||
Theorem | con1bii2 36213 | A contraposition inference. (Contributed by ML, 18-Oct-2020.) |
β’ (Β¬ π β π) β β’ (π β Β¬ π) | ||
Theorem | con2bii2 36214 | A contraposition inference. (Contributed by ML, 18-Oct-2020.) |
β’ (π β Β¬ π) β β’ (Β¬ π β π) | ||
Theorem | vtoclefex 36215* | Implicit substitution of a class for a setvar variable. (Contributed by ML, 17-Oct-2020.) |
β’ β²π₯π & β’ (π₯ = π΄ β π) β β’ (π΄ β π β π) | ||
Theorem | rnmptsn 36216* | The range of a function mapping to singletons. (Contributed by ML, 15-Jul-2020.) |
β’ ran (π₯ β π΄ β¦ {π₯}) = {π’ β£ βπ₯ β π΄ π’ = {π₯}} | ||
Theorem | f1omptsnlem 36217* | This is the core of the proof of f1omptsn 36218, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 15-Jul-2020.) |
β’ πΉ = (π₯ β π΄ β¦ {π₯}) & β’ π = {π’ β£ βπ₯ β π΄ π’ = {π₯}} β β’ πΉ:π΄β1-1-ontoβπ | ||
Theorem | f1omptsn 36218* | A function mapping to singletons is bijective onto a set of singletons. (Contributed by ML, 16-Jul-2020.) |
β’ πΉ = (π₯ β π΄ β¦ {π₯}) & β’ π = {π’ β£ βπ₯ β π΄ π’ = {π₯}} β β’ πΉ:π΄β1-1-ontoβπ | ||
Theorem | mptsnunlem 36219* | This is the core of the proof of mptsnun 36220, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 16-Jul-2020.) |
β’ πΉ = (π₯ β π΄ β¦ {π₯}) & β’ π = {π’ β£ βπ₯ β π΄ π’ = {π₯}} β β’ (π΅ β π΄ β π΅ = βͺ (πΉ β π΅)) | ||
Theorem | mptsnun 36220* | A class π΅ is equal to the union of the class of all singletons of elements of π΅. (Contributed by ML, 16-Jul-2020.) |
β’ πΉ = (π₯ β π΄ β¦ {π₯}) & β’ π = {π’ β£ βπ₯ β π΄ π’ = {π₯}} β β’ (π΅ β π΄ β π΅ = βͺ (πΉ β π΅)) | ||
Theorem | dissneqlem 36221* | This is the core of the proof of dissneq 36222, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 16-Jul-2020.) |
β’ πΆ = {π’ β£ βπ₯ β π΄ π’ = {π₯}} β β’ ((πΆ β π΅ β§ π΅ β (TopOnβπ΄)) β π΅ = π« π΄) | ||
Theorem | dissneq 36222* | Any topology that contains every single-point set is the discrete topology. (Contributed by ML, 16-Jul-2020.) |
β’ πΆ = {π’ β£ βπ₯ β π΄ π’ = {π₯}} β β’ ((πΆ β π΅ β§ π΅ β (TopOnβπ΄)) β π΅ = π« π΄) | ||
Theorem | exlimim 36223* | Closed form of exlimimd 36224. (Contributed by ML, 17-Jul-2020.) |
β’ ((βπ₯π β§ βπ₯(π β π)) β π) | ||
Theorem | exlimimd 36224* | Existential elimination rule of natural deduction. (Contributed by ML, 17-Jul-2020.) |
β’ (π β βπ₯π) & β’ (π β (π β π)) β β’ (π β π) | ||
Theorem | exellim 36225* | Closed form of exellimddv 36226. See also exlimim 36223 for a more general theorem. (Contributed by ML, 17-Jul-2020.) |
β’ ((βπ₯ π₯ β π΄ β§ βπ₯(π₯ β π΄ β π)) β π) | ||
Theorem | exellimddv 36226* | Eliminate an antecedent when the antecedent is elementhood, deduction version. See exellim 36225 for the closed form, which requires the use of a universal quantifier. (Contributed by ML, 17-Jul-2020.) |
β’ (π β βπ₯ π₯ β π΄) & β’ (π β (π₯ β π΄ β π)) β β’ (π β π) | ||
Theorem | topdifinfindis 36227* | Part of Exercise 3 of [Munkres] p. 83. The topology of all subsets π₯ of π΄ such that the complement of π₯ in π΄ is infinite, or π₯ is the empty set, or π₯ is all of π΄, is the trivial topology when π΄ is finite. (Contributed by ML, 14-Jul-2020.) |
β’ π = {π₯ β π« π΄ β£ (Β¬ (π΄ β π₯) β Fin β¨ (π₯ = β β¨ π₯ = π΄))} β β’ (π΄ β Fin β π = {β , π΄}) | ||
Theorem | topdifinffinlem 36228* | This is the core of the proof of topdifinffin 36229, but to avoid the distinct variables on the definition, we need to split this proof into two. (Contributed by ML, 17-Jul-2020.) |
β’ π = {π₯ β π« π΄ β£ (Β¬ (π΄ β π₯) β Fin β¨ (π₯ = β β¨ π₯ = π΄))} β β’ (π β (TopOnβπ΄) β π΄ β Fin) | ||
Theorem | topdifinffin 36229* | Part of Exercise 3 of [Munkres] p. 83. The topology of all subsets π₯ of π΄ such that the complement of π₯ in π΄ is infinite, or π₯ is the empty set, or π₯ is all of π΄, is a topology only if π΄ is finite. (Contributed by ML, 17-Jul-2020.) |
β’ π = {π₯ β π« π΄ β£ (Β¬ (π΄ β π₯) β Fin β¨ (π₯ = β β¨ π₯ = π΄))} β β’ (π β (TopOnβπ΄) β π΄ β Fin) | ||
Theorem | topdifinf 36230* | Part of Exercise 3 of [Munkres] p. 83. The topology of all subsets π₯ of π΄ such that the complement of π₯ in π΄ is infinite, or π₯ is the empty set, or π₯ is all of π΄, is a topology if and only if π΄ is finite, in which case it is the trivial topology. (Contributed by ML, 17-Jul-2020.) |
β’ π = {π₯ β π« π΄ β£ (Β¬ (π΄ β π₯) β Fin β¨ (π₯ = β β¨ π₯ = π΄))} β β’ ((π β (TopOnβπ΄) β π΄ β Fin) β§ (π β (TopOnβπ΄) β π = {β , π΄})) | ||
Theorem | topdifinfeq 36231* | Two different ways of defining the collection from Exercise 3 of [Munkres] p. 83. (Contributed by ML, 18-Jul-2020.) |
β’ {π₯ β π« π΄ β£ (Β¬ (π΄ β π₯) β Fin β¨ ((π΄ β π₯) = β β¨ (π΄ β π₯) = π΄))} = {π₯ β π« π΄ β£ (Β¬ (π΄ β π₯) β Fin β¨ (π₯ = β β¨ π₯ = π΄))} | ||
Theorem | icorempo 36232* | Closed-below, open-above intervals of reals. (Contributed by ML, 26-Jul-2020.) |
β’ πΉ = ([,) βΎ (β Γ β)) β β’ πΉ = (π₯ β β, π¦ β β β¦ {π§ β β β£ (π₯ β€ π§ β§ π§ < π¦)}) | ||
Theorem | icoreresf 36233 | Closed-below, open-above intervals of reals map to subsets of reals. (Contributed by ML, 25-Jul-2020.) |
β’ ([,) βΎ (β Γ β)):(β Γ β)βΆπ« β | ||
Theorem | icoreval 36234* | Value of the closed-below, open-above interval function on reals. (Contributed by ML, 26-Jul-2020.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄[,)π΅) = {π§ β β β£ (π΄ β€ π§ β§ π§ < π΅)}) | ||
Theorem | icoreelrnab 36235* | Elementhood in the set of closed-below, open-above intervals of reals. (Contributed by ML, 27-Jul-2020.) |
β’ πΌ = ([,) β (β Γ β)) β β’ (π β πΌ β βπ β β βπ β β π = {π§ β β β£ (π β€ π§ β§ π§ < π)}) | ||
Theorem | isbasisrelowllem1 36236* | Lemma for isbasisrelowl 36239. (Contributed by ML, 27-Jul-2020.) |
β’ πΌ = ([,) β (β Γ β)) β β’ ((((π β β β§ π β β β§ π₯ = {π§ β β β£ (π β€ π§ β§ π§ < π)}) β§ (π β β β§ π β β β§ π¦ = {π§ β β β£ (π β€ π§ β§ π§ < π)})) β§ (π β€ π β§ π β€ π)) β (π₯ β© π¦) β πΌ) | ||
Theorem | isbasisrelowllem2 36237* | Lemma for isbasisrelowl 36239. (Contributed by ML, 27-Jul-2020.) |
β’ πΌ = ([,) β (β Γ β)) β β’ ((((π β β β§ π β β β§ π₯ = {π§ β β β£ (π β€ π§ β§ π§ < π)}) β§ (π β β β§ π β β β§ π¦ = {π§ β β β£ (π β€ π§ β§ π§ < π)})) β§ (π β€ π β§ π β€ π)) β (π₯ β© π¦) β πΌ) | ||
Theorem | icoreclin 36238* | The set of closed-below, open-above intervals of reals is closed under finite intersection. (Contributed by ML, 27-Jul-2020.) |
β’ πΌ = ([,) β (β Γ β)) β β’ ((π₯ β πΌ β§ π¦ β πΌ) β (π₯ β© π¦) β πΌ) | ||
Theorem | isbasisrelowl 36239 | The set of all closed-below, open-above intervals of reals form a basis. (Contributed by ML, 27-Jul-2020.) |
β’ πΌ = ([,) β (β Γ β)) β β’ πΌ β TopBases | ||
Theorem | icoreunrn 36240 | The union of all closed-below, open-above intervals of reals is the set of reals. (Contributed by ML, 27-Jul-2020.) |
β’ πΌ = ([,) β (β Γ β)) β β’ β = βͺ πΌ | ||
Theorem | istoprelowl 36241 | The set of all closed-below, open-above intervals of reals generate a topology on the reals. (Contributed by ML, 27-Jul-2020.) |
β’ πΌ = ([,) β (β Γ β)) β β’ (topGenβπΌ) β (TopOnββ) | ||
Theorem | icoreelrn 36242* | A class abstraction which is an element of the set of closed-below, open-above intervals of reals. (Contributed by ML, 1-Aug-2020.) |
β’ πΌ = ([,) β (β Γ β)) β β’ ((π΄ β β β§ π΅ β β) β {π§ β β β£ (π΄ β€ π§ β§ π§ < π΅)} β πΌ) | ||
Theorem | iooelexlt 36243* | An element of an open interval is not its smallest element. (Contributed by ML, 2-Aug-2020.) |
β’ (π β (π΄(,)π΅) β βπ¦ β (π΄(,)π΅)π¦ < π) | ||
Theorem | relowlssretop 36244 | The lower limit topology on the reals is finer than the standard topology. (Contributed by ML, 1-Aug-2020.) |
β’ πΌ = ([,) β (β Γ β)) β β’ (topGenβran (,)) β (topGenβπΌ) | ||
Theorem | relowlpssretop 36245 | The lower limit topology on the reals is strictly finer than the standard topology. (Contributed by ML, 2-Aug-2020.) |
β’ πΌ = ([,) β (β Γ β)) β β’ (topGenβran (,)) β (topGenβπΌ) | ||
Theorem | sucneqond 36246 | Inequality of an ordinal set with its successor. Does not use the axiom of regularity. (Contributed by ML, 18-Oct-2020.) |
β’ (π β π = suc π) & β’ (π β π β On) β β’ (π β π β π) | ||
Theorem | sucneqoni 36247 | Inequality of an ordinal set with its successor. Does not use the axiom of regularity. (Contributed by ML, 18-Oct-2020.) |
β’ π = suc π & β’ π β On β β’ π β π | ||
Theorem | onsucuni3 36248 | If an ordinal number has a predecessor, then it is successor of that predecessor. (Contributed by ML, 17-Oct-2020.) |
β’ ((π΅ β On β§ π΅ β β β§ Β¬ Lim π΅) β π΅ = suc βͺ π΅) | ||
Theorem | 1oequni2o 36249 | The ordinal number 1o is the predecessor of the ordinal number 2o. (Contributed by ML, 19-Oct-2020.) |
β’ 1o = βͺ 2o | ||
Theorem | rdgsucuni 36250 | If an ordinal number has a predecessor, the value of the recursive definition generator at that number in terms of its predecessor. (Contributed by ML, 17-Oct-2020.) |
β’ ((π΅ β On β§ π΅ β β β§ Β¬ Lim π΅) β (rec(πΉ, πΌ)βπ΅) = (πΉβ(rec(πΉ, πΌ)ββͺ π΅))) | ||
Theorem | rdgeqoa 36251 | If a recursive function with an initial value π΄ at step π is equal to itself with an initial value π΅ at step π, then every finite number of successor steps will also be equal. (Contributed by ML, 21-Oct-2020.) |
β’ ((π β On β§ π β On β§ π β Ο) β ((rec(πΉ, π΄)βπ) = (rec(πΉ, π΅)βπ) β (rec(πΉ, π΄)β(π +o π)) = (rec(πΉ, π΅)β(π +o π)))) | ||
Theorem | elxp8 36252 | Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp7 8010. (Contributed by ML, 19-Oct-2020.) |
β’ (π΄ β (π΅ Γ πΆ) β ((1st βπ΄) β π΅ β§ π΄ β (V Γ πΆ))) | ||
Theorem | cbveud 36253* | Deduction used to change bound variables in an existential uniqueness quantifier, using implicit substitution. (Contributed by ML, 27-Mar-2021.) |
β’ β²π₯π & β’ β²π¦π & β’ (π β β²π¦π) & β’ (π β β²π₯π) & β’ (π β (π₯ = π¦ β (π β π))) β β’ (π β (β!π₯π β β!π¦π)) | ||
Theorem | cbvreud 36254* | Deduction used to change bound variables in a restricted existential uniqueness quantifier. (Contributed by ML, 27-Mar-2021.) |
β’ β²π₯π & β’ β²π¦π & β’ (π β β²π¦π) & β’ (π β β²π₯π) & β’ (π β (π₯ = π¦ β (π β π))) β β’ (π β (β!π₯ β π΄ π β β!π¦ β π΄ π)) | ||
Theorem | difunieq 36255 | The difference of unions is a subset of the union of the difference. (Contributed by ML, 29-Mar-2021.) |
β’ (βͺ π΄ β βͺ π΅) β βͺ (π΄ β π΅) | ||
Theorem | inunissunidif 36256 | Theorem about subsets of the difference of unions. (Contributed by ML, 29-Mar-2021.) |
β’ ((π΄ β© βͺ πΆ) = β β (π΄ β βͺ π΅ β π΄ β βͺ (π΅ β πΆ))) | ||
Theorem | rdgellim 36257 | Elementhood in a recursive definition at a limit ordinal. (Contributed by ML, 30-Mar-2022.) |
β’ (((π΅ β On β§ Lim π΅) β§ πΆ β π΅) β (π β (rec(πΉ, π΄)βπΆ) β π β (rec(πΉ, π΄)βπ΅))) | ||
Theorem | rdglimss 36258 | A recursive definition at a limit ordinal is a superset of itself at any smaller ordinal. (Contributed by ML, 30-Mar-2022.) |
β’ (((π΅ β On β§ Lim π΅) β§ πΆ β π΅) β (rec(πΉ, π΄)βπΆ) β (rec(πΉ, π΄)βπ΅)) | ||
Theorem | rdgssun 36259* | In a recursive definition where each step expands on the previous one using a union, every previous step is a subset of every later step. (Contributed by ML, 1-Apr-2022.) |
β’ πΉ = (π€ β V β¦ (π€ βͺ π΅)) & β’ π΅ β V β β’ ((π β On β§ π β π) β (rec(πΉ, π΄)βπ) β (rec(πΉ, π΄)βπ)) | ||
Theorem | exrecfnlem 36260* | Lemma for exrecfn 36261. (Contributed by ML, 30-Mar-2022.) |
β’ πΉ = (π§ β V β¦ (π§ βͺ ran (π¦ β π§ β¦ π΅))) β β’ ((π΄ β π β§ βπ¦ π΅ β π) β βπ₯(π΄ β π₯ β§ βπ¦ β π₯ π΅ β π₯)) | ||
Theorem | exrecfn 36261* | Theorem about the existence of infinite recursive sets. π¦ should usually be free in π΅. (Contributed by ML, 30-Mar-2022.) |
β’ ((π΄ β π β§ βπ¦ π΅ β π) β βπ₯(π΄ β π₯ β§ βπ¦ β π₯ π΅ β π₯)) | ||
Theorem | exrecfnpw 36262* | For any base set, a set which contains the powerset of all of its own elements exists. (Contributed by ML, 30-Mar-2022.) |
β’ (π΄ β π β βπ₯(π΄ β π₯ β§ βπ¦ β π₯ π« π¦ β π₯)) | ||
Theorem | finorwe 36263 | If the Axiom of Infinity is denied, every total order is a well-order. The notion of a well-order cannot be usefully expressed without the Axiom of Infinity due to the inability to quantify over proper classes. (Contributed by ML, 5-Oct-2023.) |
β’ (Β¬ Ο β V β ( < Or π΄ β < We π΄)) | ||
Syntax | cfinxp 36264 | Extend the definition of a class to include Cartesian exponentiation. |
class (πββπ) | ||
Definition | df-finxp 36265* |
Define Cartesian exponentiation on a class.
Note that this definition is limited to finite exponents, since it is defined using nested ordered pairs. If tuples of infinite length are needed, or if they might be needed in the future, use df-ixp 8892 or df-map 8822 instead. The main advantage of this definition is that it integrates better with functions and relations. For example if π is a subset of (π΄ββ2o), then df-br 5150 can be used on it, and df-fv 6552 can also be used, and so on. It's also worth keeping in mind that ((πββπ) Γ (πββπ)) is generally not equal to (πββ(π +o π)). This definition is technical. Use finxp1o 36273 and finxpsuc 36279 for a more standard recursive experience. (Contributed by ML, 16-Oct-2020.) |
β’ (πββπ) = {π¦ β£ (π β Ο β§ β = (rec((π β Ο, π₯ β V β¦ if((π = 1o β§ π₯ β π), β , if(π₯ β (V Γ π), β¨βͺ π, (1st βπ₯)β©, β¨π, π₯β©))), β¨π, π¦β©)βπ))} | ||
Theorem | dffinxpf 36266* | This theorem is the same as Definition df-finxp 36265, except that the large function is replaced by a class variable for brevity. (Contributed by ML, 24-Oct-2020.) |
β’ πΉ = (π β Ο, π₯ β V β¦ if((π = 1o β§ π₯ β π), β , if(π₯ β (V Γ π), β¨βͺ π, (1st βπ₯)β©, β¨π, π₯β©))) β β’ (πββπ) = {π¦ β£ (π β Ο β§ β = (rec(πΉ, β¨π, π¦β©)βπ))} | ||
Theorem | finxpeq1 36267 | Equality theorem for Cartesian exponentiation. (Contributed by ML, 19-Oct-2020.) |
β’ (π = π β (πββπ) = (πββπ)) | ||
Theorem | finxpeq2 36268 | Equality theorem for Cartesian exponentiation. (Contributed by ML, 19-Oct-2020.) |
β’ (π = π β (πββπ) = (πββπ)) | ||
Theorem | csbfinxpg 36269* | Distribute proper substitution through Cartesian exponentiation. (Contributed by ML, 25-Oct-2020.) |
β’ (π΄ β π β β¦π΄ / π₯β¦(πββπ) = (β¦π΄ / π₯β¦πβββ¦π΄ / π₯β¦π)) | ||
Theorem | finxpreclem1 36270* | Lemma for ββ recursion theorems. (Contributed by ML, 17-Oct-2020.) |
β’ (π β π β β = ((π β Ο, π₯ β V β¦ if((π = 1o β§ π₯ β π), β , if(π₯ β (V Γ π), β¨βͺ π, (1st βπ₯)β©, β¨π, π₯β©)))ββ¨1o, πβ©)) | ||
Theorem | finxpreclem2 36271* | Lemma for ββ recursion theorems. (Contributed by ML, 17-Oct-2020.) |
β’ ((π β V β§ Β¬ π β π) β Β¬ β = ((π β Ο, π₯ β V β¦ if((π = 1o β§ π₯ β π), β , if(π₯ β (V Γ π), β¨βͺ π, (1st βπ₯)β©, β¨π, π₯β©)))ββ¨1o, πβ©)) | ||
Theorem | finxp0 36272 | The value of Cartesian exponentiation at zero. (Contributed by ML, 24-Oct-2020.) |
β’ (πβββ ) = β | ||
Theorem | finxp1o 36273 | The value of Cartesian exponentiation at one. (Contributed by ML, 17-Oct-2020.) |
β’ (πββ1o) = π | ||
Theorem | finxpreclem3 36274* | Lemma for ββ recursion theorems. (Contributed by ML, 20-Oct-2020.) |
β’ πΉ = (π β Ο, π₯ β V β¦ if((π = 1o β§ π₯ β π), β , if(π₯ β (V Γ π), β¨βͺ π, (1st βπ₯)β©, β¨π, π₯β©))) β β’ (((π β Ο β§ 2o β π) β§ π β (V Γ π)) β β¨βͺ π, (1st βπ)β© = (πΉββ¨π, πβ©)) | ||
Theorem | finxpreclem4 36275* | Lemma for ββ recursion theorems. (Contributed by ML, 23-Oct-2020.) |
β’ πΉ = (π β Ο, π₯ β V β¦ if((π = 1o β§ π₯ β π), β , if(π₯ β (V Γ π), β¨βͺ π, (1st βπ₯)β©, β¨π, π₯β©))) β β’ (((π β Ο β§ 2o β π) β§ π¦ β (V Γ π)) β (rec(πΉ, β¨π, π¦β©)βπ) = (rec(πΉ, β¨βͺ π, (1st βπ¦)β©)ββͺ π)) | ||
Theorem | finxpreclem5 36276* | Lemma for ββ recursion theorems. (Contributed by ML, 24-Oct-2020.) |
β’ πΉ = (π β Ο, π₯ β V β¦ if((π = 1o β§ π₯ β π), β , if(π₯ β (V Γ π), β¨βͺ π, (1st βπ₯)β©, β¨π, π₯β©))) β β’ ((π β Ο β§ 1o β π) β (Β¬ π₯ β (V Γ π) β (πΉββ¨π, π₯β©) = β¨π, π₯β©)) | ||
Theorem | finxpreclem6 36277* | Lemma for ββ recursion theorems. (Contributed by ML, 24-Oct-2020.) |
β’ πΉ = (π β Ο, π₯ β V β¦ if((π = 1o β§ π₯ β π), β , if(π₯ β (V Γ π), β¨βͺ π, (1st βπ₯)β©, β¨π, π₯β©))) β β’ ((π β Ο β§ 1o β π) β (πββπ) β (V Γ π)) | ||
Theorem | finxpsuclem 36278* | Lemma for finxpsuc 36279. (Contributed by ML, 24-Oct-2020.) |
β’ πΉ = (π β Ο, π₯ β V β¦ if((π = 1o β§ π₯ β π), β , if(π₯ β (V Γ π), β¨βͺ π, (1st βπ₯)β©, β¨π, π₯β©))) β β’ ((π β Ο β§ 1o β π) β (πββsuc π) = ((πββπ) Γ π)) | ||
Theorem | finxpsuc 36279 | The value of Cartesian exponentiation at a successor. (Contributed by ML, 24-Oct-2020.) |
β’ ((π β Ο β§ π β β ) β (πββsuc π) = ((πββπ) Γ π)) | ||
Theorem | finxp2o 36280 | The value of Cartesian exponentiation at two. (Contributed by ML, 19-Oct-2020.) |
β’ (πββ2o) = (π Γ π) | ||
Theorem | finxp3o 36281 | The value of Cartesian exponentiation at three. (Contributed by ML, 24-Oct-2020.) |
β’ (πββ3o) = ((π Γ π) Γ π) | ||
Theorem | finxpnom 36282 | Cartesian exponentiation when the exponent is not a natural number defaults to the empty set. (Contributed by ML, 24-Oct-2020.) |
β’ (Β¬ π β Ο β (πββπ) = β ) | ||
Theorem | finxp00 36283 | Cartesian exponentiation of the empty set to any power is the empty set. (Contributed by ML, 24-Oct-2020.) |
β’ (β ββπ) = β | ||
Theorem | iunctb2 36284 | Using the axiom of countable choice ax-cc 10430, the countable union of countable sets is countable. See iunctb 10569 for a somewhat more general theorem. (Contributed by ML, 10-Dec-2020.) |
β’ (βπ₯ β Ο π΅ βΌ Ο β βͺ π₯ β Ο π΅ βΌ Ο) | ||
Theorem | domalom 36285* | A class which dominates every natural number is not finite. (Contributed by ML, 14-Dec-2020.) |
β’ (βπ β Ο π βΌ π΄ β Β¬ π΄ β Fin) | ||
Theorem | isinf2 36286* | The converse of isinf 9260. Any set that is not finite is literally infinite, in the sense that it contains subsets of arbitrarily large finite cardinality. (It cannot be proven that the set has countably infinite subsets unless AC is invoked.) The proof does not require the Axiom of Infinity. (Contributed by ML, 14-Dec-2020.) |
β’ (βπ β Ο βπ₯(π₯ β π΄ β§ π₯ β π) β Β¬ π΄ β Fin) | ||
Theorem | ctbssinf 36287* | Using the axiom of choice, any infinite class has a countable subset. (Contributed by ML, 14-Dec-2020.) |
β’ (Β¬ π΄ β Fin β βπ₯(π₯ β π΄ β§ π₯ β Ο)) | ||
Theorem | ralssiun 36288* | The index set of an indexed union is a subset of the union when each π΅ contains its index. (Contributed by ML, 16-Dec-2020.) |
β’ (βπ₯ β π΄ π₯ β π΅ β π΄ β βͺ π₯ β π΄ π΅) | ||
Theorem | nlpineqsn 36289* | For every point π of a subset π΄ of π with no limit points, there exists an open set π that intersects π΄ only at π. (Contributed by ML, 23-Mar-2021.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π β§ ((limPtβπ½)βπ΄) = β ) β βπ β π΄ βπ β π½ (π β π β§ (π β© π΄) = {π})) | ||
Theorem | nlpfvineqsn 36290* | Given a subset π΄ of π with no limit points, there exists a function from each point π of π΄ to an open set intersecting π΄ only at π. This proof uses the axiom of choice. (Contributed by ML, 23-Mar-2021.) |
β’ π = βͺ π½ β β’ (π΄ β π β ((π½ β Top β§ π΄ β π β§ ((limPtβπ½)βπ΄) = β ) β βπ(π:π΄βΆπ½ β§ βπ β π΄ ((πβπ) β© π΄) = {π}))) | ||
Theorem | fvineqsnf1 36291* | A theorem about functions where the image of every point intersects the domain only at that point. If π½ is a topology and π΄ is a set with no limit points, then there exists an πΉ such that this antecedent is true. See nlpfvineqsn 36290 for a proof of this fact. (Contributed by ML, 23-Mar-2021.) |
β’ ((πΉ:π΄βΆπ½ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β πΉ:π΄β1-1βπ½) | ||
Theorem | fvineqsneu 36292* | A theorem about functions where the image of every point intersects the domain only at that point. (Contributed by ML, 27-Mar-2021.) |
β’ ((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β βπ β π΄ β!π₯ β ran πΉ π β π₯) | ||
Theorem | fvineqsneq 36293* | A theorem about functions where the image of every point intersects the domain only at that point. (Contributed by ML, 28-Mar-2021.) |
β’ (((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β§ (π β ran πΉ β§ π΄ β βͺ π)) β π = ran πΉ) | ||
This section contains a few proofs of theorems found in the pi-base database. The pi-base site can be found at <https://topology.pi-base.org/>. Definitions of topological properties are theorems labeled pibpN, where N is the property number in pi-base. For example, pibp19 36295 defines countably compact topologies. Proofs of theorems are similarly labeled pibtN, for example pibt2 36298. | ||
Theorem | pibp16 36294* | Property P000016 of pi-base. The class of compact topologies. A space π is compact if every open cover of π has a finite subcover. This theorem is just a relabeled copy of iscmp 22892. (Contributed by ML, 8-Dec-2020.) |
β’ π = βͺ π½ β β’ (π½ β Comp β (π½ β Top β§ βπ¦ β π« π½(π = βͺ π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§))) | ||
Theorem | pibp19 36295* | Property P000019 of pi-base. The class of countably compact topologies. A space π is countably compact if every countable open cover of π has a finite subcover. (Contributed by ML, 8-Dec-2020.) |
β’ π = βͺ π½ & β’ πΆ = {π₯ β Top β£ βπ¦ β π« π₯((βͺ π₯ = βͺ π¦ β§ π¦ βΌ Ο) β βπ§ β (π« π¦ β© Fin)βͺ π₯ = βͺ π§)} β β’ (π½ β πΆ β (π½ β Top β§ βπ¦ β π« π½((π = βͺ π¦ β§ π¦ βΌ Ο) β βπ§ β (π« π¦ β© Fin)π = βͺ π§))) | ||
Theorem | pibp21 36296* | Property P000021 of pi-base. The class of weakly countably compact topologies, or limit point compact topologies. A space π is weakly countably compact if every infinite subset of π has a limit point. (Contributed by ML, 9-Dec-2020.) |
β’ π = βͺ π½ & β’ π = {π₯ β Top β£ βπ¦ β (π« βͺ π₯ β Fin)βπ§ β βͺ π₯π§ β ((limPtβπ₯)βπ¦)} β β’ (π½ β π β (π½ β Top β§ βπ¦ β (π« π β Fin)βπ§ β π π§ β ((limPtβπ½)βπ¦))) | ||
Theorem | pibt1 36297* | Theorem T000001 of pi-base. A compact topology is also countably compact. See pibp16 36294 and pibp19 36295 for the definitions of the relevant properties. (Contributed by ML, 8-Dec-2020.) |
β’ πΆ = {π₯ β Top β£ βπ¦ β π« π₯((βͺ π₯ = βͺ π¦ β§ π¦ βΌ Ο) β βπ§ β (π« π¦ β© Fin)βͺ π₯ = βͺ π§)} β β’ (π½ β Comp β π½ β πΆ) | ||
Theorem | pibt2 36298* | Theorem T000002 of pi-base, a countably compact topology is also weakly countably compact. See pibp19 36295 and pibp21 36296 for the definitions of the relevant properties. This proof uses the axiom of choice. (Contributed by ML, 30-Mar-2021.) |
β’ π = βͺ π½ & β’ πΆ = {π₯ β Top β£ βπ¦ β π« π₯((βͺ π₯ = βͺ π¦ β§ π¦ βΌ Ο) β βπ§ β (π« π¦ β© Fin)βͺ π₯ = βͺ π§)} & β’ π = {π₯ β Top β£ βπ¦ β (π« βͺ π₯ β Fin)βπ§ β βͺ π₯π§ β ((limPtβπ₯)βπ¦)} β β’ (π½ β πΆ β π½ β π) | ||
Theorem | wl-section-prop 36299 |
Intuitionistic logic is now developed separately, so we need not first
focus on intuitionally valid axioms ax-1 6 and
ax-2 7
any longer.
Alternatively, I start from Jan Lukasiewicz's axiom system here, i.e., ax-mp 5, ax-luk1 36300, ax-luk2 36301 and ax-luk3 36302. I rather copy this system than use luk-1 1658 to luk-3 1660, since the latter are theorems, while we need axioms here. (Contributed by Wolf Lammen, 23-Feb-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π β β’ π | ||
Axiom | ax-luk1 36300 |
1 of 3 axioms for propositional calculus due to Lukasiewicz. Copy of
luk-1 1658 and imim1 83, but introduced as an axiom. It
focuses on a basic
property of a valid implication, namely that the consequent has to be true
whenever the antecedent is. So if π and π are somehow
parametrized expressions, then π β π states that π strengthen
π, in that π holds only for a (often
proper) subset of those
parameters making π true. We easily accept, that when
π is
stronger than π and, at the same time π is
stronger than
π, then π must be stronger than
π.
This transitivity is
expressed in this axiom.
A particular result of this strengthening property comes into play if the antecedent holds unconditionally. Then the consequent must hold unconditionally as well. This specialization is the foundational idea behind logical conclusion. Such conclusion is best expressed in so-called immediate versions of this axiom like imim1i 63 or syl 17. Note that these forms are weaker replacements (i.e. just frequent specialization) of the closed form presented here, hence a mere convenience. We can identify in this axiom up to three antecedents, followed by a consequent. The number of antecedents is not really fixed; the fewer we are willing to "see", the more complex the consequent grows. On the other side, since π is a variable capable of assuming an implication itself, we might find even more antecedents after some substitution of π. This shows that the ideas of antecedent and consequent in expressions like this depends on, and can adapt to, our current interpretation of the whole expression. In this axiom, up to two antecedents happen to be of complex nature themselves, i.e. are an embedded implication. Logically, this axiom is a compact notion of simpler expressions, which I will later coin implication chains. Herein all antecedents and the consequent appear as simple variables, or their negation. Any propositional expression is equivalent to a set of such chains. This axiom, for example, is dissected into following chains, from which it can be recovered losslessly: (π β (π β (π β π))); (Β¬ π β (π β (π β π))); (π β (Β¬ π β (π β π))); (Β¬ π β (Β¬ π β (π β π))). (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) |
β’ ((π β π) β ((π β π) β (π β π))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |