![]() |
Metamath
Proof Explorer Theorem List (p. 353 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | opnrebl2 35201* | A set is open in the standard topology of the reals precisely when every point can be enclosed in an arbitrarily small ball. (Contributed by Jeff Hankins, 22-Sep-2013.) (Proof shortened by Mario Carneiro, 30-Jan-2014.) |
β’ (π΄ β (topGenβran (,)) β (π΄ β β β§ βπ₯ β π΄ βπ¦ β β+ βπ§ β β+ (π§ β€ π¦ β§ ((π₯ β π§)(,)(π₯ + π§)) β π΄))) | ||
Theorem | nn0prpwlem 35202* | Lemma for nn0prpw 35203. Use strong induction to show that every positive integer has unique prime power divisors. (Contributed by Jeff Hankins, 28-Sep-2013.) |
β’ (π΄ β β β βπ β β (π < π΄ β βπ β β βπ β β Β¬ ((πβπ) β₯ π β (πβπ) β₯ π΄))) | ||
Theorem | nn0prpw 35203* | Two nonnegative integers are the same if and only if they are divisible by the same prime powers. (Contributed by Jeff Hankins, 29-Sep-2013.) |
β’ ((π΄ β β0 β§ π΅ β β0) β (π΄ = π΅ β βπ β β βπ β β ((πβπ) β₯ π΄ β (πβπ) β₯ π΅))) | ||
Theorem | topbnd 35204 | Two equivalent expressions for the boundary of a topology. (Contributed by Jeff Hankins, 23-Sep-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β (((clsβπ½)βπ΄) β© ((clsβπ½)β(π β π΄))) = (((clsβπ½)βπ΄) β ((intβπ½)βπ΄))) | ||
Theorem | opnbnd 35205 | A set is open iff it is disjoint from its boundary. (Contributed by Jeff Hankins, 23-Sep-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β (π΄ β π½ β (π΄ β© (((clsβπ½)βπ΄) β© ((clsβπ½)β(π β π΄)))) = β )) | ||
Theorem | cldbnd 35206 | A set is closed iff it contains its boundary. (Contributed by Jeff Hankins, 1-Oct-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β (π΄ β (Clsdβπ½) β (((clsβπ½)βπ΄) β© ((clsβπ½)β(π β π΄))) β π΄)) | ||
Theorem | ntruni 35207* | A union of interiors is a subset of the interior of the union. The reverse inclusion may not hold. (Contributed by Jeff Hankins, 31-Aug-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π« π) β βͺ π β π ((intβπ½)βπ) β ((intβπ½)ββͺ π)) | ||
Theorem | clsun 35208 | A pairwise union of closures is the closure of the union. (Contributed by Jeff Hankins, 31-Aug-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((clsβπ½)β(π΄ βͺ π΅)) = (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅))) | ||
Theorem | clsint2 35209* | The closure of an intersection is a subset of the intersection of the closures. (Contributed by Jeff Hankins, 31-Aug-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ πΆ β π« π) β ((clsβπ½)ββ© πΆ) β β© π β πΆ ((clsβπ½)βπ)) | ||
Theorem | opnregcld 35210* | A set is regularly closed iff it is the closure of some open set. (Contributed by Jeff Hankins, 27-Sep-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β (((clsβπ½)β((intβπ½)βπ΄)) = π΄ β βπ β π½ π΄ = ((clsβπ½)βπ))) | ||
Theorem | cldregopn 35211* | A set if regularly open iff it is the interior of some closed set. (Contributed by Jeff Hankins, 27-Sep-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β (((intβπ½)β((clsβπ½)βπ΄)) = π΄ β βπ β (Clsdβπ½)π΄ = ((intβπ½)βπ))) | ||
Theorem | neiin 35212 | Two neighborhoods intersect to form a neighborhood of the intersection. (Contributed by Jeff Hankins, 31-Aug-2009.) |
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄) β§ π β ((neiβπ½)βπ΅)) β (π β© π) β ((neiβπ½)β(π΄ β© π΅))) | ||
Theorem | hmeoclda 35213 | Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009.) (Revised by Mario Carneiro, 3-Jun-2014.) |
β’ (((π½ β Top β§ πΎ β Top β§ πΉ β (π½HomeoπΎ)) β§ π β (Clsdβπ½)) β (πΉ β π) β (ClsdβπΎ)) | ||
Theorem | hmeocldb 35214 | Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009.) |
β’ (((π½ β Top β§ πΎ β Top β§ πΉ β (π½HomeoπΎ)) β§ π β (ClsdβπΎ)) β (β‘πΉ β π) β (Clsdβπ½)) | ||
Theorem | ivthALT 35215* | An alternate proof of the Intermediate Value Theorem ivth 24970 using topology. (Contributed by Jeff Hankins, 17-Aug-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (((π΄ β β β§ π΅ β β β§ π β β) β§ π΄ < π΅ β§ ((π΄[,]π΅) β π· β§ π· β β β§ (πΉ β (π·βcnββ) β§ (πΉ β (π΄[,]π΅)) β β β§ π β ((πΉβπ΄)(,)(πΉβπ΅))))) β βπ₯ β (π΄(,)π΅)(πΉβπ₯) = π) | ||
Syntax | cfne 35216 | Extend class definition to include the "finer than" relation. |
class Fne | ||
Definition | df-fne 35217* | Define the fineness relation for covers. (Contributed by Jeff Hankins, 28-Sep-2009.) |
β’ Fne = {β¨π₯, π¦β© β£ (βͺ π₯ = βͺ π¦ β§ βπ§ β π₯ π§ β βͺ (π¦ β© π« π§))} | ||
Theorem | fnerel 35218 | Fineness is a relation. (Contributed by Jeff Hankins, 28-Sep-2009.) |
β’ Rel Fne | ||
Theorem | isfne 35219* | The predicate "π΅ is finer than π΄". This property is, in a sense, the opposite of refinement, as refinement requires every element to be a subset of an element of the original and fineness requires that every element of the original have a subset in the finer cover containing every point. I do not know of a literature reference for this. (Contributed by Jeff Hankins, 28-Sep-2009.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΅ β πΆ β (π΄Fneπ΅ β (π = π β§ βπ₯ β π΄ π₯ β βͺ (π΅ β© π« π₯)))) | ||
Theorem | isfne4 35220 | The predicate "π΅ is finer than π΄ " in terms of the topology generation function. (Contributed by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΄Fneπ΅ β (π = π β§ π΄ β (topGenβπ΅))) | ||
Theorem | isfne4b 35221 | A condition for a topology to be finer than another. (Contributed by Jeff Hankins, 28-Sep-2009.) (Revised by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΅ β π β (π΄Fneπ΅ β (π = π β§ (topGenβπ΄) β (topGenβπ΅)))) | ||
Theorem | isfne2 35222* | The predicate "π΅ is finer than π΄". (Contributed by Jeff Hankins, 28-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΅ β πΆ β (π΄Fneπ΅ β (π = π β§ βπ₯ β π΄ βπ¦ β π₯ βπ§ β π΅ (π¦ β π§ β§ π§ β π₯)))) | ||
Theorem | isfne3 35223* | The predicate "π΅ is finer than π΄". (Contributed by Jeff Hankins, 11-Oct-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΅ β πΆ β (π΄Fneπ΅ β (π = π β§ βπ₯ β π΄ βπ¦(π¦ β π΅ β§ π₯ = βͺ π¦)))) | ||
Theorem | fnebas 35224 | A finer cover covers the same set as the original. (Contributed by Jeff Hankins, 28-Sep-2009.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΄Fneπ΅ β π = π) | ||
Theorem | fnetg 35225 | A finer cover generates a topology finer than the original set. (Contributed by Mario Carneiro, 11-Sep-2015.) |
β’ (π΄Fneπ΅ β π΄ β (topGenβπ΅)) | ||
Theorem | fnessex 35226* | If π΅ is finer than π΄ and π is an element of π΄, every point in π is an element of a subset of π which is in π΅. (Contributed by Jeff Hankins, 28-Sep-2009.) |
β’ ((π΄Fneπ΅ β§ π β π΄ β§ π β π) β βπ₯ β π΅ (π β π₯ β§ π₯ β π)) | ||
Theorem | fneuni 35227* | If π΅ is finer than π΄, every element of π΄ is a union of elements of π΅. (Contributed by Jeff Hankins, 11-Oct-2009.) |
β’ ((π΄Fneπ΅ β§ π β π΄) β βπ₯(π₯ β π΅ β§ π = βͺ π₯)) | ||
Theorem | fneint 35228* | If a cover is finer than another, every point can be approached more closely by intersections. (Contributed by Jeff Hankins, 11-Oct-2009.) |
β’ (π΄Fneπ΅ β β© {π₯ β π΅ β£ π β π₯} β β© {π₯ β π΄ β£ π β π₯}) | ||
Theorem | fness 35229 | A cover is finer than its subcovers. (Contributed by Jeff Hankins, 11-Oct-2009.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ ((π΅ β πΆ β§ π΄ β π΅ β§ π = π) β π΄Fneπ΅) | ||
Theorem | fneref 35230 | Reflexivity of the fineness relation. (Contributed by Jeff Hankins, 12-Oct-2009.) |
β’ (π΄ β π β π΄Fneπ΄) | ||
Theorem | fnetr 35231 | Transitivity of the fineness relation. (Contributed by Jeff Hankins, 5-Oct-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ ((π΄Fneπ΅ β§ π΅FneπΆ) β π΄FneπΆ) | ||
Theorem | fneval 35232 | Two covers are finer than each other iff they are both bases for the same topology. (Contributed by Mario Carneiro, 11-Sep-2015.) |
β’ βΌ = (Fne β© β‘Fne) β β’ ((π΄ β π β§ π΅ β π) β (π΄ βΌ π΅ β (topGenβπ΄) = (topGenβπ΅))) | ||
Theorem | fneer 35233 | Fineness intersected with its converse is an equivalence relation. (Contributed by Jeff Hankins, 6-Oct-2009.) (Revised by Mario Carneiro, 11-Sep-2015.) |
β’ βΌ = (Fne β© β‘Fne) β β’ βΌ Er V | ||
Theorem | topfne 35234 | Fineness for covers corresponds precisely with fineness for topologies. (Contributed by Jeff Hankins, 29-Sep-2009.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ ((πΎ β Top β§ π = π) β (π½ β πΎ β π½FneπΎ)) | ||
Theorem | topfneec 35235 | A cover is equivalent to a topology iff it is a base for that topology. (Contributed by Jeff Hankins, 8-Oct-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ βΌ = (Fne β© β‘Fne) β β’ (π½ β Top β (π΄ β [π½] βΌ β (topGenβπ΄) = π½)) | ||
Theorem | topfneec2 35236 | A topology is precisely identified with its equivalence class. (Contributed by Jeff Hankins, 12-Oct-2009.) |
β’ βΌ = (Fne β© β‘Fne) β β’ ((π½ β Top β§ πΎ β Top) β ([π½] βΌ = [πΎ] βΌ β π½ = πΎ)) | ||
Theorem | fnessref 35237* | A cover is finer iff it has a subcover which is both finer and a refinement. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π = π β (π΄Fneπ΅ β βπ(π β π΅ β§ (π΄Fneπ β§ πRefπ΄)))) | ||
Theorem | refssfne 35238* | A cover is a refinement iff it is a subcover of something which is both finer and a refinement. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π = π β (π΅Refπ΄ β βπ(π΅ β π β§ (π΄Fneπ β§ πRefπ΄)))) | ||
Theorem | neibastop1 35239* | A collection of neighborhood bases determines a topology. Part of Theorem 4.5 of Stephen Willard's General Topology. (Contributed by Jeff Hankins, 8-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(π« π« π β {β })) & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯) β§ π€ β (πΉβπ₯))) β ((πΉβπ₯) β© π« (π£ β© π€)) β β ) & β’ π½ = {π β π« π β£ βπ₯ β π ((πΉβπ₯) β© π« π) β β } β β’ (π β π½ β (TopOnβπ)) | ||
Theorem | neibastop2lem 35240* | Lemma for neibastop2 35241. (Contributed by Jeff Hankins, 12-Sep-2009.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(π« π« π β {β })) & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯) β§ π€ β (πΉβπ₯))) β ((πΉβπ₯) β© π« (π£ β© π€)) β β ) & β’ π½ = {π β π« π β£ βπ₯ β π ((πΉβπ₯) β© π« π) β β } & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯))) β π₯ β π£) & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯))) β βπ‘ β (πΉβπ₯)βπ¦ β π‘ ((πΉβπ¦) β© π« π£) β β ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β (πΉβπ)) & β’ (π β π β π) & β’ πΊ = (rec((π β V β¦ βͺ π§ β π βͺ π₯ β π ((πΉβπ₯) β© π« π§)), {π}) βΎ Ο) & β’ π = {π¦ β π β£ βπ β βͺ ran πΊ((πΉβπ¦) β© π« π) β β } β β’ (π β βπ’ β π½ (π β π’ β§ π’ β π)) | ||
Theorem | neibastop2 35241* | In the topology generated by a neighborhood base, a set is a neighborhood of a point iff it contains a subset in the base. (Contributed by Jeff Hankins, 9-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(π« π« π β {β })) & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯) β§ π€ β (πΉβπ₯))) β ((πΉβπ₯) β© π« (π£ β© π€)) β β ) & β’ π½ = {π β π« π β£ βπ₯ β π ((πΉβπ₯) β© π« π) β β } & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯))) β π₯ β π£) & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯))) β βπ‘ β (πΉβπ₯)βπ¦ β π‘ ((πΉβπ¦) β© π« π£) β β ) β β’ ((π β§ π β π) β (π β ((neiβπ½)β{π}) β (π β π β§ ((πΉβπ) β© π« π) β β ))) | ||
Theorem | neibastop3 35242* | The topology generated by a neighborhood base is unique. (Contributed by Jeff Hankins, 16-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(π« π« π β {β })) & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯) β§ π€ β (πΉβπ₯))) β ((πΉβπ₯) β© π« (π£ β© π€)) β β ) & β’ π½ = {π β π« π β£ βπ₯ β π ((πΉβπ₯) β© π« π) β β } & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯))) β π₯ β π£) & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯))) β βπ‘ β (πΉβπ₯)βπ¦ β π‘ ((πΉβπ¦) β© π« π£) β β ) β β’ (π β β!π β (TopOnβπ)βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β }) | ||
Theorem | topmtcl 35243 | The meet of a collection of topologies on π is again a topology on π. (Contributed by Jeff Hankins, 5-Oct-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
β’ ((π β π β§ π β (TopOnβπ)) β (π« π β© β© π) β (TopOnβπ)) | ||
Theorem | topmeet 35244* | Two equivalent formulations of the meet of a collection of topologies. (Contributed by Jeff Hankins, 4-Oct-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
β’ ((π β π β§ π β (TopOnβπ)) β (π« π β© β© π) = βͺ {π β (TopOnβπ) β£ βπ β π π β π}) | ||
Theorem | topjoin 35245* | Two equivalent formulations of the join of a collection of topologies. (Contributed by Jeff Hankins, 6-Oct-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
β’ ((π β π β§ π β (TopOnβπ)) β (topGenβ(fiβ({π} βͺ βͺ π))) = β© {π β (TopOnβπ) β£ βπ β π π β π}) | ||
Theorem | fnemeet1 35246* | The meet of a collection of equivalence classes of covers with respect to fineness. (Contributed by Jeff Hankins, 5-Oct-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β (π« π β© β© π‘ β π (topGenβπ‘))Fneπ΄) | ||
Theorem | fnemeet2 35247* | The meet of equivalence classes under the fineness relation-part two. (Contributed by Jeff Hankins, 6-Oct-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
β’ ((π β π β§ βπ¦ β π π = βͺ π¦) β (πFne(π« π β© β© π‘ β π (topGenβπ‘)) β (π = βͺ π β§ βπ₯ β π πFneπ₯))) | ||
Theorem | fnejoin1 35248* | Join of equivalence classes under the fineness relation-part one. (Contributed by Jeff Hankins, 8-Oct-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
β’ ((π β π β§ βπ¦ β π π = βͺ π¦ β§ π΄ β π) β π΄Fneif(π = β , {π}, βͺ π)) | ||
Theorem | fnejoin2 35249* | Join of equivalence classes under the fineness relation-part two. (Contributed by Jeff Hankins, 8-Oct-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
β’ ((π β π β§ βπ¦ β π π = βͺ π¦) β (if(π = β , {π}, βͺ π)Fneπ β (π = βͺ π β§ βπ₯ β π π₯Fneπ))) | ||
Theorem | fgmin 35250 | Minimality property of a generated filter: every filter that contains π΅ contains its generated filter. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Mario Carneiro, 7-Aug-2015.) |
β’ ((π΅ β (fBasβπ) β§ πΉ β (Filβπ)) β (π΅ β πΉ β (πfilGenπ΅) β πΉ)) | ||
Theorem | neifg 35251* | The neighborhood filter of a nonempty set is generated by its open supersets. See comments for opnfbas 23345. (Contributed by Jeff Hankins, 3-Sep-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π β§ π β β ) β (πfilGen{π₯ β π½ β£ π β π₯}) = ((neiβπ½)βπ)) | ||
Theorem | tailfval 35252* | The tail function for a directed set. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
β’ π = dom π· β β’ (π· β DirRel β (tailβπ·) = (π₯ β π β¦ (π· β {π₯}))) | ||
Theorem | tailval 35253 | The tail of an element in a directed set. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
β’ π = dom π· β β’ ((π· β DirRel β§ π΄ β π) β ((tailβπ·)βπ΄) = (π· β {π΄})) | ||
Theorem | eltail 35254 | An element of a tail. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
β’ π = dom π· β β’ ((π· β DirRel β§ π΄ β π β§ π΅ β πΆ) β (π΅ β ((tailβπ·)βπ΄) β π΄π·π΅)) | ||
Theorem | tailf 35255 | The tail function of a directed set sends its elements to its subsets. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
β’ π = dom π· β β’ (π· β DirRel β (tailβπ·):πβΆπ« π) | ||
Theorem | tailini 35256 | A tail contains its initial element. (Contributed by Jeff Hankins, 25-Nov-2009.) |
β’ π = dom π· β β’ ((π· β DirRel β§ π΄ β π) β π΄ β ((tailβπ·)βπ΄)) | ||
Theorem | tailfb 35257 | The collection of tails of a directed set is a filter base. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 8-Aug-2015.) |
β’ π = dom π· β β’ ((π· β DirRel β§ π β β ) β ran (tailβπ·) β (fBasβπ)) | ||
Theorem | filnetlem1 35258* | Lemma for filnet 35262. Change variables. (Contributed by Jeff Hankins, 13-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.) |
β’ π» = βͺ π β πΉ ({π} Γ π) & β’ π· = {β¨π₯, π¦β© β£ ((π₯ β π» β§ π¦ β π») β§ (1st βπ¦) β (1st βπ₯))} & β’ π΄ β V & β’ π΅ β V β β’ (π΄π·π΅ β ((π΄ β π» β§ π΅ β π») β§ (1st βπ΅) β (1st βπ΄))) | ||
Theorem | filnetlem2 35259* | Lemma for filnet 35262. The field of the direction. (Contributed by Jeff Hankins, 13-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.) |
β’ π» = βͺ π β πΉ ({π} Γ π) & β’ π· = {β¨π₯, π¦β© β£ ((π₯ β π» β§ π¦ β π») β§ (1st βπ¦) β (1st βπ₯))} β β’ (( I βΎ π») β π· β§ π· β (π» Γ π»)) | ||
Theorem | filnetlem3 35260* | Lemma for filnet 35262. (Contributed by Jeff Hankins, 13-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.) |
β’ π» = βͺ π β πΉ ({π} Γ π) & β’ π· = {β¨π₯, π¦β© β£ ((π₯ β π» β§ π¦ β π») β§ (1st βπ¦) β (1st βπ₯))} β β’ (π» = βͺ βͺ π· β§ (πΉ β (Filβπ) β (π» β (πΉ Γ π) β§ π· β DirRel))) | ||
Theorem | filnetlem4 35261* | Lemma for filnet 35262. (Contributed by Jeff Hankins, 15-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.) |
β’ π» = βͺ π β πΉ ({π} Γ π) & β’ π· = {β¨π₯, π¦β© β£ ((π₯ β π» β§ π¦ β π») β§ (1st βπ¦) β (1st βπ₯))} β β’ (πΉ β (Filβπ) β βπ β DirRel βπ(π:dom πβΆπ β§ πΉ = ((π FilMap π)βran (tailβπ)))) | ||
Theorem | filnet 35262* | A filter has the same convergence and clustering properties as some net. (Contributed by Jeff Hankins, 12-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.) |
β’ (πΉ β (Filβπ) β βπ β DirRel βπ(π:dom πβΆπ β§ πΉ = ((π FilMap π)βran (tailβπ)))) | ||
Theorem | tb-ax1 35263 | The first of three axioms in the Tarski-Bernays axiom system. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β π) β ((π β π) β (π β π))) | ||
Theorem | tb-ax2 35264 | The second of three axioms in the Tarski-Bernays axiom system. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β (π β π)) | ||
Theorem | tb-ax3 35265 |
The third of three axioms in the Tarski-Bernays axiom system.
This axiom, along with ax-mp 5, tb-ax1 35263, and tb-ax2 35264, can be used to derive any theorem or rule that uses only β. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (((π β π) β π) β π) | ||
Theorem | tbsyl 35266 | The weak syllogism from Tarski-Bernays'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β π) & β’ (π β π) β β’ (π β π) | ||
Theorem | re1ax2lem 35267 | Lemma for re1ax2 35268. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β (π β π)) β (π β (π β π))) | ||
Theorem | re1ax2 35268 | ax-2 7 rederived from the Tarski-Bernays axiom system. Often tb-ax1 35263 is replaced with this theorem to make a "standard" system. This is because this theorem is easier to work with, despite it being longer. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β (π β π)) β ((π β π) β (π β π))) | ||
Theorem | naim1 35269 | Constructor theorem for βΌ. (Contributed by Anthony Hart, 1-Sep-2011.) |
β’ ((π β π) β ((π βΌ π) β (π βΌ π))) | ||
Theorem | naim2 35270 | Constructor theorem for βΌ. (Contributed by Anthony Hart, 1-Sep-2011.) |
β’ ((π β π) β ((π βΌ π) β (π βΌ π))) | ||
Theorem | naim1i 35271 | Constructor rule for βΌ. (Contributed by Anthony Hart, 2-Sep-2011.) |
β’ (π β π) & β’ (π βΌ π) β β’ (π βΌ π) | ||
Theorem | naim2i 35272 | Constructor rule for βΌ. (Contributed by Anthony Hart, 2-Sep-2011.) |
β’ (π β π) & β’ (π βΌ π) β β’ (π βΌ π) | ||
Theorem | naim12i 35273 | Constructor rule for βΌ. (Contributed by Anthony Hart, 2-Sep-2011.) |
β’ (π β π) & β’ (π β π) & β’ (π βΌ π) β β’ (π βΌ π) | ||
Theorem | nabi1i 35274 | Constructor rule for βΌ. (Contributed by Anthony Hart, 2-Sep-2011.) |
β’ (π β π) & β’ (π βΌ π) β β’ (π βΌ π) | ||
Theorem | nabi2i 35275 | Constructor rule for βΌ. (Contributed by Anthony Hart, 2-Sep-2011.) |
β’ (π β π) & β’ (π βΌ π) β β’ (π βΌ π) | ||
Theorem | nabi12i 35276 | Constructor rule for βΌ. (Contributed by Anthony Hart, 2-Sep-2011.) |
β’ (π β π) & β’ (π β π) & β’ (π βΌ π) β β’ (π βΌ π) | ||
Syntax | w3nand 35277 | The double nand. |
wff (π βΌ π βΌ π) | ||
Definition | df-3nand 35278 | The double nand. This definition allows to express the input of three variables only being false if all three are true. (Contributed by Anthony Hart, 2-Sep-2011.) |
β’ ((π βΌ π βΌ π) β (π β (π β Β¬ π))) | ||
Theorem | df3nandALT1 35279 | The double nand expressed in terms of pure nand. (Contributed by Anthony Hart, 2-Sep-2011.) |
β’ ((π βΌ π βΌ π) β (π βΌ ((π βΌ π) βΌ (π βΌ π)))) | ||
Theorem | df3nandALT2 35280 | The double nand expressed in terms of negation and and not. (Contributed by Anthony Hart, 13-Sep-2011.) |
β’ ((π βΌ π βΌ π) β Β¬ (π β§ π β§ π)) | ||
Theorem | andnand1 35281 | Double and in terms of double nand. (Contributed by Anthony Hart, 2-Sep-2011.) |
β’ ((π β§ π β§ π) β ((π βΌ π βΌ π) βΌ (π βΌ π βΌ π))) | ||
Theorem | imnand2 35282 | An β nand relation. (Contributed by Anthony Hart, 2-Sep-2011.) |
β’ ((Β¬ π β π) β ((π βΌ π) βΌ (π βΌ π))) | ||
Theorem | nalfal 35283 | Not all sets hold β₯ as true. (Contributed by Anthony Hart, 13-Sep-2011.) |
β’ Β¬ βπ₯β₯ | ||
Theorem | nexntru 35284 | There does not exist a set such that β€ is not true. (Contributed by Anthony Hart, 13-Sep-2011.) |
β’ Β¬ βπ₯ Β¬ β€ | ||
Theorem | nexfal 35285 | There does not exist a set such that β₯ is true. (Contributed by Anthony Hart, 13-Sep-2011.) |
β’ Β¬ βπ₯β₯ | ||
Theorem | neufal 35286 | There does not exist exactly one set such that β₯ is true. (Contributed by Anthony Hart, 13-Sep-2011.) |
β’ Β¬ β!π₯β₯ | ||
Theorem | neutru 35287 | There does not exist exactly one set such that β€ is true. (Contributed by Anthony Hart, 13-Sep-2011.) |
β’ Β¬ β!π₯β€ | ||
Theorem | nmotru 35288 | There does not exist at most one set such that β€ is true. (Contributed by Anthony Hart, 13-Sep-2011.) |
β’ Β¬ β*π₯β€ | ||
Theorem | mofal 35289 | There exist at most one set such that β₯ is true. (Contributed by Anthony Hart, 13-Sep-2011.) |
β’ β*π₯β₯ | ||
Theorem | nrmo 35290 | "At most one" restricted existential quantifier for a statement which is never true. (Contributed by Thierry Arnoux, 27-Nov-2023.) |
β’ (π₯ β π΄ β Β¬ π) β β’ β*π₯ β π΄ π | ||
Theorem | meran1 35291 | A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011.) |
β’ (Β¬ (Β¬ (Β¬ π β¨ π) β¨ (π β¨ (π β¨ π))) β¨ (Β¬ (Β¬ π β¨ π) β¨ (π β¨ (π β¨ π)))) | ||
Theorem | meran2 35292 | A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011.) |
β’ (Β¬ (Β¬ (Β¬ π β¨ π) β¨ (π β¨ (π β¨ π))) β¨ (Β¬ (Β¬ π β¨ π) β¨ (π β¨ (π β¨ π)))) | ||
Theorem | meran3 35293 | A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011.) |
β’ (Β¬ (Β¬ (Β¬ π β¨ π) β¨ (π β¨ (π β¨ π))) β¨ (Β¬ (Β¬ π β¨ π) β¨ (π β¨ (π β¨ π)))) | ||
Theorem | waj-ax 35294 | A single axiom for propositional calculus discovered by Mordchaj Wajsberg (Logical Works, Polish Academy of Sciences, 1977). See: Fitelson, Some recent results in algebra and logical calculi obtained using automated reasoning, 2003 (axiom W on slide 8). (Contributed by Anthony Hart, 13-Aug-2011.) |
β’ ((π βΌ (π βΌ π)) βΌ (((π βΌ π) βΌ ((π βΌ π) βΌ (π βΌ π))) βΌ (π βΌ (π βΌ π)))) | ||
Theorem | lukshef-ax2 35295 | A single axiom for propositional calculus discovered by Jan Lukasiewicz. See: Fitelson, Some recent results in algebra and logical calculi obtained using automated reasoning, 2003 (axiom L2 on slide 8). (Contributed by Anthony Hart, 14-Aug-2011.) |
β’ ((π βΌ (π βΌ π)) βΌ ((π βΌ (π βΌ π)) βΌ ((π βΌ π) βΌ ((π βΌ π) βΌ (π βΌ π))))) | ||
Theorem | arg-ax 35296 | A single axiom for propositional calculus discovered by Ken Harris and Branden Fitelson. See: Fitelson, Some recent results in algebra and logical calculi obtained using automated reasoning, 2003 (axiom HF1 on slide 8). (Contributed by Anthony Hart, 14-Aug-2011.) |
β’ ((π βΌ (π βΌ π)) βΌ ((π βΌ (π βΌ π)) βΌ ((π βΌ π) βΌ ((π βΌ π) βΌ (π βΌ π))))) | ||
Theorem | negsym1 35297 |
In the paper "On Variable Functors of Propositional Arguments",
Lukasiewicz introduced a system that can handle variable connectives.
This was done by introducing a variable, marked with a lowercase delta,
which takes a wff as input. In the system, "delta π "
means that
"something is true of π". The expression "delta
π
" can be
substituted with Β¬ π, π β§ π, βπ₯π, etc.
Later on, Meredith discovered a single axiom, in the form of ( delta delta β₯ β delta π ). This represents the shortest theorem in the extended propositional calculus that cannot be derived as an instance of a theorem in propositional calculus. A symmetry with Β¬. (Contributed by Anthony Hart, 4-Sep-2011.) |
β’ (Β¬ Β¬ β₯ β Β¬ π) | ||
Theorem | imsym1 35298 |
A symmetry with β.
See negsym1 35297 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
β’ ((π β (π β β₯)) β (π β π)) | ||
Theorem | bisym1 35299 |
A symmetry with β.
See negsym1 35297 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
β’ ((π β (π β β₯)) β (π β π)) | ||
Theorem | consym1 35300 |
A symmetry with β§.
See negsym1 35297 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
β’ ((π β§ (π β§ β₯)) β (π β§ π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |