![]() |
Metamath
Proof Explorer Theorem List (p. 366 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bj-endcomp 36501 | Composition law of the monoid of endomorphisms on an object of a category. (Contributed by BJ, 5-Apr-2024.) (Proof modification is discouraged.) |
β’ (π β πΆ β Cat) & β’ (π β π β (BaseβπΆ)) β β’ (π β (+gβ((End βπΆ)βπ)) = (β¨π, πβ©(compβπΆ)π)) | ||
Theorem | bj-endmnd 36502 | The monoid of endomorphisms on an object of a category is a monoid. (Contributed by BJ, 5-Apr-2024.) (Proof modification is discouraged.) |
β’ (π β πΆ β Cat) & β’ (π β π β (BaseβπΆ)) β β’ (π β ((End βπΆ)βπ) β Mnd) | ||
Theorem | taupilem3 36503 | Lemma for tau-related theorems. (Contributed by Jim Kingdon, 16-Feb-2019.) |
β’ (π΄ β (β+ β© (β‘cos β {1})) β (π΄ β β+ β§ (cosβπ΄) = 1)) | ||
Theorem | taupilemrplb 36504* | A set of positive reals has (in the reals) a lower bound. (Contributed by Jim Kingdon, 19-Feb-2019.) |
β’ βπ₯ β β βπ¦ β (β+ β© π΄)π₯ β€ π¦ | ||
Theorem | taupilem1 36505 | Lemma for taupi 36507. A positive real whose cosine is one is at least 2 Β· Ο. (Contributed by Jim Kingdon, 19-Feb-2019.) |
β’ ((π΄ β β+ β§ (cosβπ΄) = 1) β (2 Β· Ο) β€ π΄) | ||
Theorem | taupilem2 36506 | Lemma for taupi 36507. 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 36507 | 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 36508* | Alternate definition of the gcd operator. (Contributed by Jim Kingdon, 31-Dec-2021.) |
β’ ((π β β€ β§ π β β€) β (π gcd π) = (β©π β β0 βπ§ β β€ (π§ β₯ π β (π§ β₯ π β§ π§ β₯ π)))) | ||
Theorem | irrdifflemf 36509 | Lemma for irrdiff 36510. The forward direction. (Contributed by Jim Kingdon, 20-May-2024.) |
β’ (π β π΄ β β) & β’ (π β Β¬ π΄ β β) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β π ) β β’ (π β (absβ(π΄ β π)) β (absβ(π΄ β π ))) | ||
Theorem | irrdiff 36510* | 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 36511 | 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 36512 | Move class substitution in and out of recs. (Contributed by ML, 25-Oct-2020.) |
β’ (π΄ β π β β¦π΄ / π₯β¦recs(πΉ) = recs(β¦π΄ / π₯β¦πΉ)) | ||
Theorem | csbrdgg 36513 | Move class substitution in and out of the recursive function generator. (Contributed by ML, 25-Oct-2020.) |
β’ (π΄ β π β β¦π΄ / π₯β¦rec(πΉ, πΌ) = rec(β¦π΄ / π₯β¦πΉ, β¦π΄ / π₯β¦πΌ)) | ||
Theorem | csboprabg 36514* | Move class substitution in and out of class abstractions of nested ordered pairs. (Contributed by ML, 25-Oct-2020.) |
β’ (π΄ β π β β¦π΄ / π₯β¦{β¨β¨π¦, π§β©, πβ© β£ π} = {β¨β¨π¦, π§β©, πβ© β£ [π΄ / π₯]π}) | ||
Theorem | csbmpo123 36515* | Move class substitution in and out of maps-to notation for operations. (Contributed by ML, 25-Oct-2020.) |
β’ (π΄ β π β β¦π΄ / π₯β¦(π¦ β π, π§ β π β¦ π·) = (π¦ β β¦π΄ / π₯β¦π, π§ β β¦π΄ / π₯β¦π β¦ β¦π΄ / π₯β¦π·)) | ||
Theorem | con1bii2 36516 | A contraposition inference. (Contributed by ML, 18-Oct-2020.) |
β’ (Β¬ π β π) β β’ (π β Β¬ π) | ||
Theorem | con2bii2 36517 | A contraposition inference. (Contributed by ML, 18-Oct-2020.) |
β’ (π β Β¬ π) β β’ (Β¬ π β π) | ||
Theorem | vtoclefex 36518* | Implicit substitution of a class for a setvar variable. (Contributed by ML, 17-Oct-2020.) |
β’ β²π₯π & β’ (π₯ = π΄ β π) β β’ (π΄ β π β π) | ||
Theorem | rnmptsn 36519* | The range of a function mapping to singletons. (Contributed by ML, 15-Jul-2020.) |
β’ ran (π₯ β π΄ β¦ {π₯}) = {π’ β£ βπ₯ β π΄ π’ = {π₯}} | ||
Theorem | f1omptsnlem 36520* | This is the core of the proof of f1omptsn 36521, 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 36521* | A function mapping to singletons is bijective onto a set of singletons. (Contributed by ML, 16-Jul-2020.) |
β’ πΉ = (π₯ β π΄ β¦ {π₯}) & β’ π = {π’ β£ βπ₯ β π΄ π’ = {π₯}} β β’ πΉ:π΄β1-1-ontoβπ | ||
Theorem | mptsnunlem 36522* | This is the core of the proof of mptsnun 36523, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 16-Jul-2020.) |
β’ πΉ = (π₯ β π΄ β¦ {π₯}) & β’ π = {π’ β£ βπ₯ β π΄ π’ = {π₯}} β β’ (π΅ β π΄ β π΅ = βͺ (πΉ β π΅)) | ||
Theorem | mptsnun 36523* | A class π΅ is equal to the union of the class of all singletons of elements of π΅. (Contributed by ML, 16-Jul-2020.) |
β’ πΉ = (π₯ β π΄ β¦ {π₯}) & β’ π = {π’ β£ βπ₯ β π΄ π’ = {π₯}} β β’ (π΅ β π΄ β π΅ = βͺ (πΉ β π΅)) | ||
Theorem | dissneqlem 36524* | This is the core of the proof of dissneq 36525, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 16-Jul-2020.) |
β’ πΆ = {π’ β£ βπ₯ β π΄ π’ = {π₯}} β β’ ((πΆ β π΅ β§ π΅ β (TopOnβπ΄)) β π΅ = π« π΄) | ||
Theorem | dissneq 36525* | Any topology that contains every single-point set is the discrete topology. (Contributed by ML, 16-Jul-2020.) |
β’ πΆ = {π’ β£ βπ₯ β π΄ π’ = {π₯}} β β’ ((πΆ β π΅ β§ π΅ β (TopOnβπ΄)) β π΅ = π« π΄) | ||
Theorem | exlimim 36526* | Closed form of exlimimd 36527. (Contributed by ML, 17-Jul-2020.) |
β’ ((βπ₯π β§ βπ₯(π β π)) β π) | ||
Theorem | exlimimd 36527* | Existential elimination rule of natural deduction. (Contributed by ML, 17-Jul-2020.) |
β’ (π β βπ₯π) & β’ (π β (π β π)) β β’ (π β π) | ||
Theorem | exellim 36528* | Closed form of exellimddv 36529. See also exlimim 36526 for a more general theorem. (Contributed by ML, 17-Jul-2020.) |
β’ ((βπ₯ π₯ β π΄ β§ βπ₯(π₯ β π΄ β π)) β π) | ||
Theorem | exellimddv 36529* | Eliminate an antecedent when the antecedent is elementhood, deduction version. See exellim 36528 for the closed form, which requires the use of a universal quantifier. (Contributed by ML, 17-Jul-2020.) |
β’ (π β βπ₯ π₯ β π΄) & β’ (π β (π₯ β π΄ β π)) β β’ (π β π) | ||
Theorem | topdifinfindis 36530* | 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 36531* | This is the core of the proof of topdifinffin 36532, 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 36532* | 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 36533* | 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 36534* | Two different ways of defining the collection from Exercise 3 of [Munkres] p. 83. (Contributed by ML, 18-Jul-2020.) |
β’ {π₯ β π« π΄ β£ (Β¬ (π΄ β π₯) β Fin β¨ ((π΄ β π₯) = β β¨ (π΄ β π₯) = π΄))} = {π₯ β π« π΄ β£ (Β¬ (π΄ β π₯) β Fin β¨ (π₯ = β β¨ π₯ = π΄))} | ||
Theorem | icorempo 36535* | Closed-below, open-above intervals of reals. (Contributed by ML, 26-Jul-2020.) |
β’ πΉ = ([,) βΎ (β Γ β)) β β’ πΉ = (π₯ β β, π¦ β β β¦ {π§ β β β£ (π₯ β€ π§ β§ π§ < π¦)}) | ||
Theorem | icoreresf 36536 | Closed-below, open-above intervals of reals map to subsets of reals. (Contributed by ML, 25-Jul-2020.) |
β’ ([,) βΎ (β Γ β)):(β Γ β)βΆπ« β | ||
Theorem | icoreval 36537* | Value of the closed-below, open-above interval function on reals. (Contributed by ML, 26-Jul-2020.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄[,)π΅) = {π§ β β β£ (π΄ β€ π§ β§ π§ < π΅)}) | ||
Theorem | icoreelrnab 36538* | Elementhood in the set of closed-below, open-above intervals of reals. (Contributed by ML, 27-Jul-2020.) |
β’ πΌ = ([,) β (β Γ β)) β β’ (π β πΌ β βπ β β βπ β β π = {π§ β β β£ (π β€ π§ β§ π§ < π)}) | ||
Theorem | isbasisrelowllem1 36539* | Lemma for isbasisrelowl 36542. (Contributed by ML, 27-Jul-2020.) |
β’ πΌ = ([,) β (β Γ β)) β β’ ((((π β β β§ π β β β§ π₯ = {π§ β β β£ (π β€ π§ β§ π§ < π)}) β§ (π β β β§ π β β β§ π¦ = {π§ β β β£ (π β€ π§ β§ π§ < π)})) β§ (π β€ π β§ π β€ π)) β (π₯ β© π¦) β πΌ) | ||
Theorem | isbasisrelowllem2 36540* | Lemma for isbasisrelowl 36542. (Contributed by ML, 27-Jul-2020.) |
β’ πΌ = ([,) β (β Γ β)) β β’ ((((π β β β§ π β β β§ π₯ = {π§ β β β£ (π β€ π§ β§ π§ < π)}) β§ (π β β β§ π β β β§ π¦ = {π§ β β β£ (π β€ π§ β§ π§ < π)})) β§ (π β€ π β§ π β€ π)) β (π₯ β© π¦) β πΌ) | ||
Theorem | icoreclin 36541* | The set of closed-below, open-above intervals of reals is closed under finite intersection. (Contributed by ML, 27-Jul-2020.) |
β’ πΌ = ([,) β (β Γ β)) β β’ ((π₯ β πΌ β§ π¦ β πΌ) β (π₯ β© π¦) β πΌ) | ||
Theorem | isbasisrelowl 36542 | The set of all closed-below, open-above intervals of reals form a basis. (Contributed by ML, 27-Jul-2020.) |
β’ πΌ = ([,) β (β Γ β)) β β’ πΌ β TopBases | ||
Theorem | icoreunrn 36543 | The union of all closed-below, open-above intervals of reals is the set of reals. (Contributed by ML, 27-Jul-2020.) |
β’ πΌ = ([,) β (β Γ β)) β β’ β = βͺ πΌ | ||
Theorem | istoprelowl 36544 | 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 36545* | 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 36546* | An element of an open interval is not its smallest element. (Contributed by ML, 2-Aug-2020.) |
β’ (π β (π΄(,)π΅) β βπ¦ β (π΄(,)π΅)π¦ < π) | ||
Theorem | relowlssretop 36547 | The lower limit topology on the reals is finer than the standard topology. (Contributed by ML, 1-Aug-2020.) |
β’ πΌ = ([,) β (β Γ β)) β β’ (topGenβran (,)) β (topGenβπΌ) | ||
Theorem | relowlpssretop 36548 | 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 36549 | 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 36550 | 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 36551 | 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 36552 | The ordinal number 1o is the predecessor of the ordinal number 2o. (Contributed by ML, 19-Oct-2020.) |
β’ 1o = βͺ 2o | ||
Theorem | rdgsucuni 36553 | 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 36554 | 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 36555 | Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp7 8012. (Contributed by ML, 19-Oct-2020.) |
β’ (π΄ β (π΅ Γ πΆ) β ((1st βπ΄) β π΅ β§ π΄ β (V Γ πΆ))) | ||
Theorem | cbveud 36556* | Deduction used to change bound variables in an existential uniqueness quantifier, using implicit substitution. (Contributed by ML, 27-Mar-2021.) |
β’ β²π₯π & β’ β²π¦π & β’ (π β β²π¦π) & β’ (π β β²π₯π) & β’ (π β (π₯ = π¦ β (π β π))) β β’ (π β (β!π₯π β β!π¦π)) | ||
Theorem | cbvreud 36557* | Deduction used to change bound variables in a restricted existential uniqueness quantifier. (Contributed by ML, 27-Mar-2021.) |
β’ β²π₯π & β’ β²π¦π & β’ (π β β²π¦π) & β’ (π β β²π₯π) & β’ (π β (π₯ = π¦ β (π β π))) β β’ (π β (β!π₯ β π΄ π β β!π¦ β π΄ π)) | ||
Theorem | difunieq 36558 | The difference of unions is a subset of the union of the difference. (Contributed by ML, 29-Mar-2021.) |
β’ (βͺ π΄ β βͺ π΅) β βͺ (π΄ β π΅) | ||
Theorem | inunissunidif 36559 | Theorem about subsets of the difference of unions. (Contributed by ML, 29-Mar-2021.) |
β’ ((π΄ β© βͺ πΆ) = β β (π΄ β βͺ π΅ β π΄ β βͺ (π΅ β πΆ))) | ||
Theorem | rdgellim 36560 | Elementhood in a recursive definition at a limit ordinal. (Contributed by ML, 30-Mar-2022.) |
β’ (((π΅ β On β§ Lim π΅) β§ πΆ β π΅) β (π β (rec(πΉ, π΄)βπΆ) β π β (rec(πΉ, π΄)βπ΅))) | ||
Theorem | rdglimss 36561 | 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 36562* | 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 36563* | Lemma for exrecfn 36564. (Contributed by ML, 30-Mar-2022.) |
β’ πΉ = (π§ β V β¦ (π§ βͺ ran (π¦ β π§ β¦ π΅))) β β’ ((π΄ β π β§ βπ¦ π΅ β π) β βπ₯(π΄ β π₯ β§ βπ¦ β π₯ π΅ β π₯)) | ||
Theorem | exrecfn 36564* | Theorem about the existence of infinite recursive sets. π¦ should usually be free in π΅. (Contributed by ML, 30-Mar-2022.) |
β’ ((π΄ β π β§ βπ¦ π΅ β π) β βπ₯(π΄ β π₯ β§ βπ¦ β π₯ π΅ β π₯)) | ||
Theorem | exrecfnpw 36565* | 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 36566 | 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 36567 | Extend the definition of a class to include Cartesian exponentiation. |
class (πββπ) | ||
Definition | df-finxp 36568* |
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 8894 or df-map 8824 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 5148 can be used on it, and df-fv 6550 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 36576 and finxpsuc 36582 for a more standard recursive experience. (Contributed by ML, 16-Oct-2020.) |
β’ (πββπ) = {π¦ β£ (π β Ο β§ β = (rec((π β Ο, π₯ β V β¦ if((π = 1o β§ π₯ β π), β , if(π₯ β (V Γ π), β¨βͺ π, (1st βπ₯)β©, β¨π, π₯β©))), β¨π, π¦β©)βπ))} | ||
Theorem | dffinxpf 36569* | This theorem is the same as Definition df-finxp 36568, 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 36570 | Equality theorem for Cartesian exponentiation. (Contributed by ML, 19-Oct-2020.) |
β’ (π = π β (πββπ) = (πββπ)) | ||
Theorem | finxpeq2 36571 | Equality theorem for Cartesian exponentiation. (Contributed by ML, 19-Oct-2020.) |
β’ (π = π β (πββπ) = (πββπ)) | ||
Theorem | csbfinxpg 36572* | Distribute proper substitution through Cartesian exponentiation. (Contributed by ML, 25-Oct-2020.) |
β’ (π΄ β π β β¦π΄ / π₯β¦(πββπ) = (β¦π΄ / π₯β¦πβββ¦π΄ / π₯β¦π)) | ||
Theorem | finxpreclem1 36573* | Lemma for ββ recursion theorems. (Contributed by ML, 17-Oct-2020.) |
β’ (π β π β β = ((π β Ο, π₯ β V β¦ if((π = 1o β§ π₯ β π), β , if(π₯ β (V Γ π), β¨βͺ π, (1st βπ₯)β©, β¨π, π₯β©)))ββ¨1o, πβ©)) | ||
Theorem | finxpreclem2 36574* | Lemma for ββ recursion theorems. (Contributed by ML, 17-Oct-2020.) |
β’ ((π β V β§ Β¬ π β π) β Β¬ β = ((π β Ο, π₯ β V β¦ if((π = 1o β§ π₯ β π), β , if(π₯ β (V Γ π), β¨βͺ π, (1st βπ₯)β©, β¨π, π₯β©)))ββ¨1o, πβ©)) | ||
Theorem | finxp0 36575 | The value of Cartesian exponentiation at zero. (Contributed by ML, 24-Oct-2020.) |
β’ (πβββ ) = β | ||
Theorem | finxp1o 36576 | The value of Cartesian exponentiation at one. (Contributed by ML, 17-Oct-2020.) |
β’ (πββ1o) = π | ||
Theorem | finxpreclem3 36577* | Lemma for ββ recursion theorems. (Contributed by ML, 20-Oct-2020.) |
β’ πΉ = (π β Ο, π₯ β V β¦ if((π = 1o β§ π₯ β π), β , if(π₯ β (V Γ π), β¨βͺ π, (1st βπ₯)β©, β¨π, π₯β©))) β β’ (((π β Ο β§ 2o β π) β§ π β (V Γ π)) β β¨βͺ π, (1st βπ)β© = (πΉββ¨π, πβ©)) | ||
Theorem | finxpreclem4 36578* | Lemma for ββ recursion theorems. (Contributed by ML, 23-Oct-2020.) |
β’ πΉ = (π β Ο, π₯ β V β¦ if((π = 1o β§ π₯ β π), β , if(π₯ β (V Γ π), β¨βͺ π, (1st βπ₯)β©, β¨π, π₯β©))) β β’ (((π β Ο β§ 2o β π) β§ π¦ β (V Γ π)) β (rec(πΉ, β¨π, π¦β©)βπ) = (rec(πΉ, β¨βͺ π, (1st βπ¦)β©)ββͺ π)) | ||
Theorem | finxpreclem5 36579* | Lemma for ββ recursion theorems. (Contributed by ML, 24-Oct-2020.) |
β’ πΉ = (π β Ο, π₯ β V β¦ if((π = 1o β§ π₯ β π), β , if(π₯ β (V Γ π), β¨βͺ π, (1st βπ₯)β©, β¨π, π₯β©))) β β’ ((π β Ο β§ 1o β π) β (Β¬ π₯ β (V Γ π) β (πΉββ¨π, π₯β©) = β¨π, π₯β©)) | ||
Theorem | finxpreclem6 36580* | Lemma for ββ recursion theorems. (Contributed by ML, 24-Oct-2020.) |
β’ πΉ = (π β Ο, π₯ β V β¦ if((π = 1o β§ π₯ β π), β , if(π₯ β (V Γ π), β¨βͺ π, (1st βπ₯)β©, β¨π, π₯β©))) β β’ ((π β Ο β§ 1o β π) β (πββπ) β (V Γ π)) | ||
Theorem | finxpsuclem 36581* | Lemma for finxpsuc 36582. (Contributed by ML, 24-Oct-2020.) |
β’ πΉ = (π β Ο, π₯ β V β¦ if((π = 1o β§ π₯ β π), β , if(π₯ β (V Γ π), β¨βͺ π, (1st βπ₯)β©, β¨π, π₯β©))) β β’ ((π β Ο β§ 1o β π) β (πββsuc π) = ((πββπ) Γ π)) | ||
Theorem | finxpsuc 36582 | The value of Cartesian exponentiation at a successor. (Contributed by ML, 24-Oct-2020.) |
β’ ((π β Ο β§ π β β ) β (πββsuc π) = ((πββπ) Γ π)) | ||
Theorem | finxp2o 36583 | The value of Cartesian exponentiation at two. (Contributed by ML, 19-Oct-2020.) |
β’ (πββ2o) = (π Γ π) | ||
Theorem | finxp3o 36584 | The value of Cartesian exponentiation at three. (Contributed by ML, 24-Oct-2020.) |
β’ (πββ3o) = ((π Γ π) Γ π) | ||
Theorem | finxpnom 36585 | Cartesian exponentiation when the exponent is not a natural number defaults to the empty set. (Contributed by ML, 24-Oct-2020.) |
β’ (Β¬ π β Ο β (πββπ) = β ) | ||
Theorem | finxp00 36586 | Cartesian exponentiation of the empty set to any power is the empty set. (Contributed by ML, 24-Oct-2020.) |
β’ (β ββπ) = β | ||
Theorem | iunctb2 36587 | Using the axiom of countable choice ax-cc 10432, the countable union of countable sets is countable. See iunctb 10571 for a somewhat more general theorem. (Contributed by ML, 10-Dec-2020.) |
β’ (βπ₯ β Ο π΅ βΌ Ο β βͺ π₯ β Ο π΅ βΌ Ο) | ||
Theorem | domalom 36588* | A class which dominates every natural number is not finite. (Contributed by ML, 14-Dec-2020.) |
β’ (βπ β Ο π βΌ π΄ β Β¬ π΄ β Fin) | ||
Theorem | isinf2 36589* | The converse of isinf 9262. 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 36590* | Using the axiom of choice, any infinite class has a countable subset. (Contributed by ML, 14-Dec-2020.) |
β’ (Β¬ π΄ β Fin β βπ₯(π₯ β π΄ β§ π₯ β Ο)) | ||
Theorem | ralssiun 36591* | 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 36592* | 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 36593* | 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 36594* | 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 36593 for a proof of this fact. (Contributed by ML, 23-Mar-2021.) |
β’ ((πΉ:π΄βΆπ½ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β πΉ:π΄β1-1βπ½) | ||
Theorem | fvineqsneu 36595* | 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 36596* | 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 36598 defines countably compact topologies. Proofs of theorems are similarly labeled pibtN, for example pibt2 36601. | ||
Theorem | pibp16 36597* | 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 23112. (Contributed by ML, 8-Dec-2020.) |
β’ π = βͺ π½ β β’ (π½ β Comp β (π½ β Top β§ βπ¦ β π« π½(π = βͺ π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§))) | ||
Theorem | pibp19 36598* | 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 36599* | 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 36600* | Theorem T000001 of pi-base. A compact topology is also countably compact. See pibp16 36597 and pibp19 36598 for the definitions of the relevant properties. (Contributed by ML, 8-Dec-2020.) |
β’ πΆ = {π₯ β Top β£ βπ¦ β π« π₯((βͺ π₯ = βͺ π¦ β§ π¦ βΌ Ο) β βπ§ β (π« π¦ β© Fin)βͺ π₯ = βͺ π§)} β β’ (π½ β Comp β π½ β πΆ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |