![]() |
Metamath
Proof Explorer Theorem List (p. 356 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | imp5q 35501 | A triple importation inference. (Contributed by Jeff Hankins, 8-Jul-2009.) |
β’ (π β (π β (π β (π β (π β π))))) β β’ ((π β§ π) β ((π β§ π β§ π) β π)) | ||
Theorem | ecase13d 35502 | Deduction for elimination by cases. (Contributed by Jeff Hankins, 18-Aug-2009.) |
β’ (π β Β¬ π) & β’ (π β Β¬ π) & β’ (π β (π β¨ π β¨ π)) β β’ (π β π) | ||
Theorem | subtr 35503 | Transitivity of implicit substitution. (Contributed by Jeff Hankins, 13-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
β’ β²π₯π΄ & β’ β²π₯π΅ & β’ β²π₯π & β’ β²π₯π & β’ (π₯ = π΄ β π = π) & β’ (π₯ = π΅ β π = π) β β’ ((π΄ β πΆ β§ π΅ β π·) β (π΄ = π΅ β π = π)) | ||
Theorem | subtr2 35504 | Transitivity of implicit substitution into a wff. (Contributed by Jeff Hankins, 19-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
β’ β²π₯π΄ & β’ β²π₯π΅ & β’ β²π₯π & β’ β²π₯π & β’ (π₯ = π΄ β (π β π)) & β’ (π₯ = π΅ β (π β π)) β β’ ((π΄ β πΆ β§ π΅ β π·) β (π΄ = π΅ β (π β π))) | ||
Theorem | trer 35505* | A relation intersected with its converse is an equivalence relation if the relation is transitive. (Contributed by Jeff Hankins, 6-Oct-2009.) (Revised by Mario Carneiro, 12-Aug-2015.) |
β’ (βπβπβπ((π β€ π β§ π β€ π) β π β€ π) β ( β€ β© β‘ β€ ) Er dom ( β€ β© β‘ β€ )) | ||
Theorem | elicc3 35506 | An equivalent membership condition for closed intervals. (Contributed by Jeff Hankins, 14-Jul-2009.) |
β’ ((π΄ β β* β§ π΅ β β*) β (πΆ β (π΄[,]π΅) β (πΆ β β* β§ π΄ β€ π΅ β§ (πΆ = π΄ β¨ (π΄ < πΆ β§ πΆ < π΅) β¨ πΆ = π΅)))) | ||
Theorem | finminlem 35507* | A useful lemma about finite sets. If a property holds for a finite set, it holds for a minimal set. (Contributed by Jeff Hankins, 4-Dec-2009.) |
β’ (π₯ = π¦ β (π β π)) β β’ (βπ₯ β Fin π β βπ₯(π β§ βπ¦((π¦ β π₯ β§ π) β π₯ = π¦))) | ||
Theorem | gtinf 35508* | Any number greater than an infimum is greater than some element of the set. (Contributed by Jeff Hankins, 29-Sep-2013.) (Revised by AV, 10-Oct-2021.) |
β’ (((π β β β§ π β β β§ βπ₯ β β βπ¦ β π π₯ β€ π¦) β§ (π΄ β β β§ inf(π, β, < ) < π΄)) β βπ§ β π π§ < π΄) | ||
Theorem | opnrebl 35509* | A set is open in the standard topology of the reals precisely when every point can be enclosed in an open ball. (Contributed by Jeff Hankins, 23-Sep-2013.) (Proof shortened by Mario Carneiro, 30-Jan-2014.) |
β’ (π΄ β (topGenβran (,)) β (π΄ β β β§ βπ₯ β π΄ βπ¦ β β+ ((π₯ β π¦)(,)(π₯ + π¦)) β π΄)) | ||
Theorem | opnrebl2 35510* | 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 35511* | Lemma for nn0prpw 35512. Use strong induction to show that every positive integer has unique prime power divisors. (Contributed by Jeff Hankins, 28-Sep-2013.) |
β’ (π΄ β β β βπ β β (π < π΄ β βπ β β βπ β β Β¬ ((πβπ) β₯ π β (πβπ) β₯ π΄))) | ||
Theorem | nn0prpw 35512* | 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 35513 | Two equivalent expressions for the boundary of a topology. (Contributed by Jeff Hankins, 23-Sep-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β (((clsβπ½)βπ΄) β© ((clsβπ½)β(π β π΄))) = (((clsβπ½)βπ΄) β ((intβπ½)βπ΄))) | ||
Theorem | opnbnd 35514 | A set is open iff it is disjoint from its boundary. (Contributed by Jeff Hankins, 23-Sep-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β (π΄ β π½ β (π΄ β© (((clsβπ½)βπ΄) β© ((clsβπ½)β(π β π΄)))) = β )) | ||
Theorem | cldbnd 35515 | A set is closed iff it contains its boundary. (Contributed by Jeff Hankins, 1-Oct-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β (π΄ β (Clsdβπ½) β (((clsβπ½)βπ΄) β© ((clsβπ½)β(π β π΄))) β π΄)) | ||
Theorem | ntruni 35516* | 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 35517 | A pairwise union of closures is the closure of the union. (Contributed by Jeff Hankins, 31-Aug-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((clsβπ½)β(π΄ βͺ π΅)) = (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅))) | ||
Theorem | clsint2 35518* | 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 35519* | 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 35520* | 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 35521 | Two neighborhoods intersect to form a neighborhood of the intersection. (Contributed by Jeff Hankins, 31-Aug-2009.) |
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄) β§ π β ((neiβπ½)βπ΅)) β (π β© π) β ((neiβπ½)β(π΄ β© π΅))) | ||
Theorem | hmeoclda 35522 | Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009.) (Revised by Mario Carneiro, 3-Jun-2014.) |
β’ (((π½ β Top β§ πΎ β Top β§ πΉ β (π½HomeoπΎ)) β§ π β (Clsdβπ½)) β (πΉ β π) β (ClsdβπΎ)) | ||
Theorem | hmeocldb 35523 | Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009.) |
β’ (((π½ β Top β§ πΎ β Top β§ πΉ β (π½HomeoπΎ)) β§ π β (ClsdβπΎ)) β (β‘πΉ β π) β (Clsdβπ½)) | ||
Theorem | ivthALT 35524* | An alternate proof of the Intermediate Value Theorem ivth 25204 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 35525 | Extend class definition to include the "finer than" relation. |
class Fne | ||
Definition | df-fne 35526* | Define the fineness relation for covers. (Contributed by Jeff Hankins, 28-Sep-2009.) |
β’ Fne = {β¨π₯, π¦β© β£ (βͺ π₯ = βͺ π¦ β§ βπ§ β π₯ π§ β βͺ (π¦ β© π« π§))} | ||
Theorem | fnerel 35527 | Fineness is a relation. (Contributed by Jeff Hankins, 28-Sep-2009.) |
β’ Rel Fne | ||
Theorem | isfne 35528* | 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 35529 | The predicate "π΅ is finer than π΄ " in terms of the topology generation function. (Contributed by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΄Fneπ΅ β (π = π β§ π΄ β (topGenβπ΅))) | ||
Theorem | isfne4b 35530 | 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 35531* | The predicate "π΅ is finer than π΄". (Contributed by Jeff Hankins, 28-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΅ β πΆ β (π΄Fneπ΅ β (π = π β§ βπ₯ β π΄ βπ¦ β π₯ βπ§ β π΅ (π¦ β π§ β§ π§ β π₯)))) | ||
Theorem | isfne3 35532* | The predicate "π΅ is finer than π΄". (Contributed by Jeff Hankins, 11-Oct-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΅ β πΆ β (π΄Fneπ΅ β (π = π β§ βπ₯ β π΄ βπ¦(π¦ β π΅ β§ π₯ = βͺ π¦)))) | ||
Theorem | fnebas 35533 | A finer cover covers the same set as the original. (Contributed by Jeff Hankins, 28-Sep-2009.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΄Fneπ΅ β π = π) | ||
Theorem | fnetg 35534 | A finer cover generates a topology finer than the original set. (Contributed by Mario Carneiro, 11-Sep-2015.) |
β’ (π΄Fneπ΅ β π΄ β (topGenβπ΅)) | ||
Theorem | fnessex 35535* | 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 35536* | If π΅ is finer than π΄, every element of π΄ is a union of elements of π΅. (Contributed by Jeff Hankins, 11-Oct-2009.) |
β’ ((π΄Fneπ΅ β§ π β π΄) β βπ₯(π₯ β π΅ β§ π = βͺ π₯)) | ||
Theorem | fneint 35537* | 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 35538 | A cover is finer than its subcovers. (Contributed by Jeff Hankins, 11-Oct-2009.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ ((π΅ β πΆ β§ π΄ β π΅ β§ π = π) β π΄Fneπ΅) | ||
Theorem | fneref 35539 | Reflexivity of the fineness relation. (Contributed by Jeff Hankins, 12-Oct-2009.) |
β’ (π΄ β π β π΄Fneπ΄) | ||
Theorem | fnetr 35540 | 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 35541 | 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 35542 | 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 35543 | Fineness for covers corresponds precisely with fineness for topologies. (Contributed by Jeff Hankins, 29-Sep-2009.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ ((πΎ β Top β§ π = π) β (π½ β πΎ β π½FneπΎ)) | ||
Theorem | topfneec 35544 | 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 35545 | A topology is precisely identified with its equivalence class. (Contributed by Jeff Hankins, 12-Oct-2009.) |
β’ βΌ = (Fne β© β‘Fne) β β’ ((π½ β Top β§ πΎ β Top) β ([π½] βΌ = [πΎ] βΌ β π½ = πΎ)) | ||
Theorem | fnessref 35546* | 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 35547* | 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 35548* | 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 35549* | Lemma for neibastop2 35550. (Contributed by Jeff Hankins, 12-Sep-2009.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(π« π« π β {β })) & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯) β§ π€ β (πΉβπ₯))) β ((πΉβπ₯) β© π« (π£ β© π€)) β β ) & β’ π½ = {π β π« π β£ βπ₯ β π ((πΉβπ₯) β© π« π) β β } & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯))) β π₯ β π£) & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯))) β βπ‘ β (πΉβπ₯)βπ¦ β π‘ ((πΉβπ¦) β© π« π£) β β ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β (πΉβπ)) & β’ (π β π β π) & β’ πΊ = (rec((π β V β¦ βͺ π§ β π βͺ π₯ β π ((πΉβπ₯) β© π« π§)), {π}) βΎ Ο) & β’ π = {π¦ β π β£ βπ β βͺ ran πΊ((πΉβπ¦) β© π« π) β β } β β’ (π β βπ’ β π½ (π β π’ β§ π’ β π)) | ||
Theorem | neibastop2 35550* | 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 35551* | 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 35552 | 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 35553* | 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 35554* | 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 35555* | 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 35556* | 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 35557* | 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 35558* | 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 35559 | 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 35560* | The neighborhood filter of a nonempty set is generated by its open supersets. See comments for opnfbas 23567. (Contributed by Jeff Hankins, 3-Sep-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π β§ π β β ) β (πfilGen{π₯ β π½ β£ π β π₯}) = ((neiβπ½)βπ)) | ||
Theorem | tailfval 35561* | 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 35562 | 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 35563 | An element of a tail. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
β’ π = dom π· β β’ ((π· β DirRel β§ π΄ β π β§ π΅ β πΆ) β (π΅ β ((tailβπ·)βπ΄) β π΄π·π΅)) | ||
Theorem | tailf 35564 | 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 35565 | A tail contains its initial element. (Contributed by Jeff Hankins, 25-Nov-2009.) |
β’ π = dom π· β β’ ((π· β DirRel β§ π΄ β π) β π΄ β ((tailβπ·)βπ΄)) | ||
Theorem | tailfb 35566 | 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 35567* | Lemma for filnet 35571. Change variables. (Contributed by Jeff Hankins, 13-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.) |
β’ π» = βͺ π β πΉ ({π} Γ π) & β’ π· = {β¨π₯, π¦β© β£ ((π₯ β π» β§ π¦ β π») β§ (1st βπ¦) β (1st βπ₯))} & β’ π΄ β V & β’ π΅ β V β β’ (π΄π·π΅ β ((π΄ β π» β§ π΅ β π») β§ (1st βπ΅) β (1st βπ΄))) | ||
Theorem | filnetlem2 35568* | Lemma for filnet 35571. The field of the direction. (Contributed by Jeff Hankins, 13-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.) |
β’ π» = βͺ π β πΉ ({π} Γ π) & β’ π· = {β¨π₯, π¦β© β£ ((π₯ β π» β§ π¦ β π») β§ (1st βπ¦) β (1st βπ₯))} β β’ (( I βΎ π») β π· β§ π· β (π» Γ π»)) | ||
Theorem | filnetlem3 35569* | Lemma for filnet 35571. (Contributed by Jeff Hankins, 13-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.) |
β’ π» = βͺ π β πΉ ({π} Γ π) & β’ π· = {β¨π₯, π¦β© β£ ((π₯ β π» β§ π¦ β π») β§ (1st βπ¦) β (1st βπ₯))} β β’ (π» = βͺ βͺ π· β§ (πΉ β (Filβπ) β (π» β (πΉ Γ π) β§ π· β DirRel))) | ||
Theorem | filnetlem4 35570* | Lemma for filnet 35571. (Contributed by Jeff Hankins, 15-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.) |
β’ π» = βͺ π β πΉ ({π} Γ π) & β’ π· = {β¨π₯, π¦β© β£ ((π₯ β π» β§ π¦ β π») β§ (1st βπ¦) β (1st βπ₯))} β β’ (πΉ β (Filβπ) β βπ β DirRel βπ(π:dom πβΆπ β§ πΉ = ((π FilMap π)βran (tailβπ)))) | ||
Theorem | filnet 35571* | 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 35572 | 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 35573 | 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 35574 |
The third of three axioms in the Tarski-Bernays axiom system.
This axiom, along with ax-mp 5, tb-ax1 35572, and tb-ax2 35573, 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 35575 | The weak syllogism from Tarski-Bernays'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β π) & β’ (π β π) β β’ (π β π) | ||
Theorem | re1ax2lem 35576 | Lemma for re1ax2 35577. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β (π β π)) β (π β (π β π))) | ||
Theorem | re1ax2 35577 | ax-2 7 rederived from the Tarski-Bernays axiom system. Often tb-ax1 35572 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 35578 | Constructor theorem for βΌ. (Contributed by Anthony Hart, 1-Sep-2011.) |
β’ ((π β π) β ((π βΌ π) β (π βΌ π))) | ||
Theorem | naim2 35579 | Constructor theorem for βΌ. (Contributed by Anthony Hart, 1-Sep-2011.) |
β’ ((π β π) β ((π βΌ π) β (π βΌ π))) | ||
Theorem | naim1i 35580 | Constructor rule for βΌ. (Contributed by Anthony Hart, 2-Sep-2011.) |
β’ (π β π) & β’ (π βΌ π) β β’ (π βΌ π) | ||
Theorem | naim2i 35581 | Constructor rule for βΌ. (Contributed by Anthony Hart, 2-Sep-2011.) |
β’ (π β π) & β’ (π βΌ π) β β’ (π βΌ π) | ||
Theorem | naim12i 35582 | Constructor rule for βΌ. (Contributed by Anthony Hart, 2-Sep-2011.) |
β’ (π β π) & β’ (π β π) & β’ (π βΌ π) β β’ (π βΌ π) | ||
Theorem | nabi1i 35583 | Constructor rule for βΌ. (Contributed by Anthony Hart, 2-Sep-2011.) |
β’ (π β π) & β’ (π βΌ π) β β’ (π βΌ π) | ||
Theorem | nabi2i 35584 | Constructor rule for βΌ. (Contributed by Anthony Hart, 2-Sep-2011.) |
β’ (π β π) & β’ (π βΌ π) β β’ (π βΌ π) | ||
Theorem | nabi12i 35585 | Constructor rule for βΌ. (Contributed by Anthony Hart, 2-Sep-2011.) |
β’ (π β π) & β’ (π β π) & β’ (π βΌ π) β β’ (π βΌ π) | ||
Syntax | w3nand 35586 | The double nand. |
wff (π βΌ π βΌ π) | ||
Definition | df-3nand 35587 | 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 35588 | The double nand expressed in terms of pure nand. (Contributed by Anthony Hart, 2-Sep-2011.) |
β’ ((π βΌ π βΌ π) β (π βΌ ((π βΌ π) βΌ (π βΌ π)))) | ||
Theorem | df3nandALT2 35589 | The double nand expressed in terms of negation and and not. (Contributed by Anthony Hart, 13-Sep-2011.) |
β’ ((π βΌ π βΌ π) β Β¬ (π β§ π β§ π)) | ||
Theorem | andnand1 35590 | Double and in terms of double nand. (Contributed by Anthony Hart, 2-Sep-2011.) |
β’ ((π β§ π β§ π) β ((π βΌ π βΌ π) βΌ (π βΌ π βΌ π))) | ||
Theorem | imnand2 35591 | An β nand relation. (Contributed by Anthony Hart, 2-Sep-2011.) |
β’ ((Β¬ π β π) β ((π βΌ π) βΌ (π βΌ π))) | ||
Theorem | nalfal 35592 | Not all sets hold β₯ as true. (Contributed by Anthony Hart, 13-Sep-2011.) |
β’ Β¬ βπ₯β₯ | ||
Theorem | nexntru 35593 | There does not exist a set such that β€ is not true. (Contributed by Anthony Hart, 13-Sep-2011.) |
β’ Β¬ βπ₯ Β¬ β€ | ||
Theorem | nexfal 35594 | There does not exist a set such that β₯ is true. (Contributed by Anthony Hart, 13-Sep-2011.) |
β’ Β¬ βπ₯β₯ | ||
Theorem | neufal 35595 | There does not exist exactly one set such that β₯ is true. (Contributed by Anthony Hart, 13-Sep-2011.) |
β’ Β¬ β!π₯β₯ | ||
Theorem | neutru 35596 | There does not exist exactly one set such that β€ is true. (Contributed by Anthony Hart, 13-Sep-2011.) |
β’ Β¬ β!π₯β€ | ||
Theorem | nmotru 35597 | There does not exist at most one set such that β€ is true. (Contributed by Anthony Hart, 13-Sep-2011.) |
β’ Β¬ β*π₯β€ | ||
Theorem | mofal 35598 | There exist at most one set such that β₯ is true. (Contributed by Anthony Hart, 13-Sep-2011.) |
β’ β*π₯β₯ | ||
Theorem | nrmo 35599 | "At most one" restricted existential quantifier for a statement which is never true. (Contributed by Thierry Arnoux, 27-Nov-2023.) |
β’ (π₯ β π΄ β Β¬ π) β β’ β*π₯ β π΄ π | ||
Theorem | meran1 35600 | A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011.) |
β’ (Β¬ (Β¬ (Β¬ π β¨ π) β¨ (π β¨ (π β¨ π))) β¨ (Β¬ (Β¬ π β¨ π) β¨ (π β¨ (π β¨ π)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |