![]() |
Metamath
Proof Explorer Theorem List (p. 358 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rankpwg 35701 | The rank of a power set. Closed form of rankpw 9858. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ (π΄ β π β (rankβπ« π΄) = suc (rankβπ΄)) | ||
Theorem | rank0 35702 | The rank of the empty set is β . (Contributed by Scott Fenton, 17-Jul-2015.) |
β’ (rankββ ) = β | ||
Theorem | rankeq1o 35703 | The only set with rank 1o is the singleton of the empty set. (Contributed by Scott Fenton, 17-Jul-2015.) |
β’ ((rankβπ΄) = 1o β π΄ = {β }) | ||
Syntax | chf 35704 | The constant Hf is a class. |
class Hf | ||
Definition | df-hf 35705 | Define the hereditarily finite sets. These are the finite sets whose elements are finite, and so forth. (Contributed by Scott Fenton, 9-Jul-2015.) |
β’ Hf = βͺ (π 1 β Ο) | ||
Theorem | elhf 35706* | Membership in the hereditarily finite sets. (Contributed by Scott Fenton, 9-Jul-2015.) |
β’ (π΄ β Hf β βπ₯ β Ο π΄ β (π 1βπ₯)) | ||
Theorem | elhf2 35707 | Alternate form of membership in the hereditarily finite sets. (Contributed by Scott Fenton, 13-Jul-2015.) |
β’ π΄ β V β β’ (π΄ β Hf β (rankβπ΄) β Ο) | ||
Theorem | elhf2g 35708 | Hereditarily finiteness via rank. Closed form of elhf2 35707. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ (π΄ β π β (π΄ β Hf β (rankβπ΄) β Ο)) | ||
Theorem | 0hf 35709 | The empty set is a hereditarily finite set. (Contributed by Scott Fenton, 9-Jul-2015.) |
β’ β β Hf | ||
Theorem | hfun 35710 | The union of two HF sets is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ ((π΄ β Hf β§ π΅ β Hf ) β (π΄ βͺ π΅) β Hf ) | ||
Theorem | hfsn 35711 | The singleton of an HF set is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ (π΄ β Hf β {π΄} β Hf ) | ||
Theorem | hfadj 35712 | Adjoining one HF element to an HF set preserves HF status. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ ((π΄ β Hf β§ π΅ β Hf ) β (π΄ βͺ {π΅}) β Hf ) | ||
Theorem | hfelhf 35713 | Any member of an HF set is itself an HF set. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ ((π΄ β π΅ β§ π΅ β Hf ) β π΄ β Hf ) | ||
Theorem | hftr 35714 | The class of all hereditarily finite sets is transitive. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ Tr Hf | ||
Theorem | hfext 35715* | Extensionality for HF sets depends only on comparison of HF elements. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ ((π΄ β Hf β§ π΅ β Hf ) β (π΄ = π΅ β βπ₯ β Hf (π₯ β π΄ β π₯ β π΅))) | ||
Theorem | hfuni 35716 | The union of an HF set is itself hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ (π΄ β Hf β βͺ π΄ β Hf ) | ||
Theorem | hfpw 35717 | The power class of an HF set is hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ (π΄ β Hf β π« π΄ β Hf ) | ||
Theorem | hfninf 35718 | Ο is not hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ Β¬ Ο β Hf | ||
Theorem | mpomulnzcnf 35719* | Multiplication maps nonzero complex numbers to nonzero complex numbers. Version of mulnzcnf 11882 using maps-to notation, which does not require ax-mulf 11210. (Contributed by GG, 18-Apr-2025.) |
β’ (π₯ β (β β {0}), π¦ β (β β {0}) β¦ (π₯ Β· π¦)):((β β {0}) Γ (β β {0}))βΆ(β β {0}) | ||
Theorem | a1i14 35720 | Add two antecedents to a wff. (Contributed by Jeff Hankins, 4-Aug-2009.) |
β’ (π β (π β π)) β β’ (π β (π β (π β (π β π)))) | ||
Theorem | a1i24 35721 | Add two antecedents to a wff. Deduction associated with a1i13 27. (Contributed by Jeff Hankins, 5-Aug-2009.) |
β’ (π β (π β π)) β β’ (π β (π β (π β (π β π)))) | ||
Theorem | exp5d 35722 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ (((π β§ π) β§ π) β ((π β§ π) β π)) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp5g 35723 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((π β§ π) β (((π β§ π) β§ π) β π)) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp5k 35724 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ (π β (((π β§ (π β§ π)) β§ π) β π)) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp56 35725 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((((π β§ π) β§ π) β§ (π β§ π)) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp58 35726 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ (((π β§ π) β§ ((π β§ π) β§ π)) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp510 35727 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((π β§ (((π β§ π) β§ π) β§ π)) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp511 35728 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((π β§ ((π β§ (π β§ π)) β§ π)) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp512 35729 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((π β§ ((π β§ π) β§ (π β§ π))) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | 3com12d 35730 | Commutation in consequent. Swap 1st and 2nd. (Contributed by Jeff Hankins, 17-Nov-2009.) |
β’ (π β (π β§ π β§ π)) β β’ (π β (π β§ π β§ π)) | ||
Theorem | imp5p 35731 | A triple importation inference. (Contributed by Jeff Hankins, 8-Jul-2009.) |
β’ (π β (π β (π β (π β (π β π))))) β β’ (π β (π β ((π β§ π β§ π) β π))) | ||
Theorem | imp5q 35732 | A triple importation inference. (Contributed by Jeff Hankins, 8-Jul-2009.) |
β’ (π β (π β (π β (π β (π β π))))) β β’ ((π β§ π) β ((π β§ π β§ π) β π)) | ||
Theorem | ecase13d 35733 | Deduction for elimination by cases. (Contributed by Jeff Hankins, 18-Aug-2009.) |
β’ (π β Β¬ π) & β’ (π β Β¬ π) & β’ (π β (π β¨ π β¨ π)) β β’ (π β π) | ||
Theorem | subtr 35734 | Transitivity of implicit substitution. (Contributed by Jeff Hankins, 13-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
β’ β²π₯π΄ & β’ β²π₯π΅ & β’ β²π₯π & β’ β²π₯π & β’ (π₯ = π΄ β π = π) & β’ (π₯ = π΅ β π = π) β β’ ((π΄ β πΆ β§ π΅ β π·) β (π΄ = π΅ β π = π)) | ||
Theorem | subtr2 35735 | Transitivity of implicit substitution into a wff. (Contributed by Jeff Hankins, 19-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
β’ β²π₯π΄ & β’ β²π₯π΅ & β’ β²π₯π & β’ β²π₯π & β’ (π₯ = π΄ β (π β π)) & β’ (π₯ = π΅ β (π β π)) β β’ ((π΄ β πΆ β§ π΅ β π·) β (π΄ = π΅ β (π β π))) | ||
Theorem | trer 35736* | 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 35737 | An equivalent membership condition for closed intervals. (Contributed by Jeff Hankins, 14-Jul-2009.) |
β’ ((π΄ β β* β§ π΅ β β*) β (πΆ β (π΄[,]π΅) β (πΆ β β* β§ π΄ β€ π΅ β§ (πΆ = π΄ β¨ (π΄ < πΆ β§ πΆ < π΅) β¨ πΆ = π΅)))) | ||
Theorem | finminlem 35738* | 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 35739* | 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 35740* | 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 35741* | 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 35742* | Lemma for nn0prpw 35743. Use strong induction to show that every positive integer has unique prime power divisors. (Contributed by Jeff Hankins, 28-Sep-2013.) |
β’ (π΄ β β β βπ β β (π < π΄ β βπ β β βπ β β Β¬ ((πβπ) β₯ π β (πβπ) β₯ π΄))) | ||
Theorem | nn0prpw 35743* | 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 35744 | Two equivalent expressions for the boundary of a topology. (Contributed by Jeff Hankins, 23-Sep-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β (((clsβπ½)βπ΄) β© ((clsβπ½)β(π β π΄))) = (((clsβπ½)βπ΄) β ((intβπ½)βπ΄))) | ||
Theorem | opnbnd 35745 | A set is open iff it is disjoint from its boundary. (Contributed by Jeff Hankins, 23-Sep-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β (π΄ β π½ β (π΄ β© (((clsβπ½)βπ΄) β© ((clsβπ½)β(π β π΄)))) = β )) | ||
Theorem | cldbnd 35746 | A set is closed iff it contains its boundary. (Contributed by Jeff Hankins, 1-Oct-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β (π΄ β (Clsdβπ½) β (((clsβπ½)βπ΄) β© ((clsβπ½)β(π β π΄))) β π΄)) | ||
Theorem | ntruni 35747* | 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 35748 | A pairwise union of closures is the closure of the union. (Contributed by Jeff Hankins, 31-Aug-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((clsβπ½)β(π΄ βͺ π΅)) = (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅))) | ||
Theorem | clsint2 35749* | 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 35750* | 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 35751* | 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 35752 | Two neighborhoods intersect to form a neighborhood of the intersection. (Contributed by Jeff Hankins, 31-Aug-2009.) |
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄) β§ π β ((neiβπ½)βπ΅)) β (π β© π) β ((neiβπ½)β(π΄ β© π΅))) | ||
Theorem | hmeoclda 35753 | Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009.) (Revised by Mario Carneiro, 3-Jun-2014.) |
β’ (((π½ β Top β§ πΎ β Top β§ πΉ β (π½HomeoπΎ)) β§ π β (Clsdβπ½)) β (πΉ β π) β (ClsdβπΎ)) | ||
Theorem | hmeocldb 35754 | Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009.) |
β’ (((π½ β Top β§ πΎ β Top β§ πΉ β (π½HomeoπΎ)) β§ π β (ClsdβπΎ)) β (β‘πΉ β π) β (Clsdβπ½)) | ||
Theorem | ivthALT 35755* | An alternate proof of the Intermediate Value Theorem ivth 25370 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 35756 | Extend class definition to include the "finer than" relation. |
class Fne | ||
Definition | df-fne 35757* | Define the fineness relation for covers. (Contributed by Jeff Hankins, 28-Sep-2009.) |
β’ Fne = {β¨π₯, π¦β© β£ (βͺ π₯ = βͺ π¦ β§ βπ§ β π₯ π§ β βͺ (π¦ β© π« π§))} | ||
Theorem | fnerel 35758 | Fineness is a relation. (Contributed by Jeff Hankins, 28-Sep-2009.) |
β’ Rel Fne | ||
Theorem | isfne 35759* | 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 35760 | The predicate "π΅ is finer than π΄ " in terms of the topology generation function. (Contributed by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΄Fneπ΅ β (π = π β§ π΄ β (topGenβπ΅))) | ||
Theorem | isfne4b 35761 | 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 35762* | The predicate "π΅ is finer than π΄". (Contributed by Jeff Hankins, 28-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΅ β πΆ β (π΄Fneπ΅ β (π = π β§ βπ₯ β π΄ βπ¦ β π₯ βπ§ β π΅ (π¦ β π§ β§ π§ β π₯)))) | ||
Theorem | isfne3 35763* | The predicate "π΅ is finer than π΄". (Contributed by Jeff Hankins, 11-Oct-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΅ β πΆ β (π΄Fneπ΅ β (π = π β§ βπ₯ β π΄ βπ¦(π¦ β π΅ β§ π₯ = βͺ π¦)))) | ||
Theorem | fnebas 35764 | A finer cover covers the same set as the original. (Contributed by Jeff Hankins, 28-Sep-2009.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΄Fneπ΅ β π = π) | ||
Theorem | fnetg 35765 | A finer cover generates a topology finer than the original set. (Contributed by Mario Carneiro, 11-Sep-2015.) |
β’ (π΄Fneπ΅ β π΄ β (topGenβπ΅)) | ||
Theorem | fnessex 35766* | 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 35767* | If π΅ is finer than π΄, every element of π΄ is a union of elements of π΅. (Contributed by Jeff Hankins, 11-Oct-2009.) |
β’ ((π΄Fneπ΅ β§ π β π΄) β βπ₯(π₯ β π΅ β§ π = βͺ π₯)) | ||
Theorem | fneint 35768* | 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 35769 | A cover is finer than its subcovers. (Contributed by Jeff Hankins, 11-Oct-2009.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ ((π΅ β πΆ β§ π΄ β π΅ β§ π = π) β π΄Fneπ΅) | ||
Theorem | fneref 35770 | Reflexivity of the fineness relation. (Contributed by Jeff Hankins, 12-Oct-2009.) |
β’ (π΄ β π β π΄Fneπ΄) | ||
Theorem | fnetr 35771 | 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 35772 | 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 35773 | 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 35774 | Fineness for covers corresponds precisely with fineness for topologies. (Contributed by Jeff Hankins, 29-Sep-2009.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ ((πΎ β Top β§ π = π) β (π½ β πΎ β π½FneπΎ)) | ||
Theorem | topfneec 35775 | 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 35776 | A topology is precisely identified with its equivalence class. (Contributed by Jeff Hankins, 12-Oct-2009.) |
β’ βΌ = (Fne β© β‘Fne) β β’ ((π½ β Top β§ πΎ β Top) β ([π½] βΌ = [πΎ] βΌ β π½ = πΎ)) | ||
Theorem | fnessref 35777* | 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 35778* | 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 35779* | 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 35780* | Lemma for neibastop2 35781. (Contributed by Jeff Hankins, 12-Sep-2009.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(π« π« π β {β })) & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯) β§ π€ β (πΉβπ₯))) β ((πΉβπ₯) β© π« (π£ β© π€)) β β ) & β’ π½ = {π β π« π β£ βπ₯ β π ((πΉβπ₯) β© π« π) β β } & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯))) β π₯ β π£) & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯))) β βπ‘ β (πΉβπ₯)βπ¦ β π‘ ((πΉβπ¦) β© π« π£) β β ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β (πΉβπ)) & β’ (π β π β π) & β’ πΊ = (rec((π β V β¦ βͺ π§ β π βͺ π₯ β π ((πΉβπ₯) β© π« π§)), {π}) βΎ Ο) & β’ π = {π¦ β π β£ βπ β βͺ ran πΊ((πΉβπ¦) β© π« π) β β } β β’ (π β βπ’ β π½ (π β π’ β§ π’ β π)) | ||
Theorem | neibastop2 35781* | 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 35782* | 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 35783 | 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 35784* | 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 35785* | 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 35786* | 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 35787* | 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 35788* | 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 35789* | 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 35790 | 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 35791* | The neighborhood filter of a nonempty set is generated by its open supersets. See comments for opnfbas 23733. (Contributed by Jeff Hankins, 3-Sep-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π β§ π β β ) β (πfilGen{π₯ β π½ β£ π β π₯}) = ((neiβπ½)βπ)) | ||
Theorem | tailfval 35792* | 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 35793 | 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 35794 | An element of a tail. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
β’ π = dom π· β β’ ((π· β DirRel β§ π΄ β π β§ π΅ β πΆ) β (π΅ β ((tailβπ·)βπ΄) β π΄π·π΅)) | ||
Theorem | tailf 35795 | 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 35796 | A tail contains its initial element. (Contributed by Jeff Hankins, 25-Nov-2009.) |
β’ π = dom π· β β’ ((π· β DirRel β§ π΄ β π) β π΄ β ((tailβπ·)βπ΄)) | ||
Theorem | tailfb 35797 | 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 35798* | Lemma for filnet 35802. Change variables. (Contributed by Jeff Hankins, 13-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.) |
β’ π» = βͺ π β πΉ ({π} Γ π) & β’ π· = {β¨π₯, π¦β© β£ ((π₯ β π» β§ π¦ β π») β§ (1st βπ¦) β (1st βπ₯))} & β’ π΄ β V & β’ π΅ β V β β’ (π΄π·π΅ β ((π΄ β π» β§ π΅ β π») β§ (1st βπ΅) β (1st βπ΄))) | ||
Theorem | filnetlem2 35799* | Lemma for filnet 35802. The field of the direction. (Contributed by Jeff Hankins, 13-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.) |
β’ π» = βͺ π β πΉ ({π} Γ π) & β’ π· = {β¨π₯, π¦β© β£ ((π₯ β π» β§ π¦ β π») β§ (1st βπ¦) β (1st βπ₯))} β β’ (( I βΎ π») β π· β§ π· β (π» Γ π»)) | ||
Theorem | filnetlem3 35800* | Lemma for filnet 35802. (Contributed by Jeff Hankins, 13-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.) |
β’ π» = βͺ π β πΉ ({π} Γ π) & β’ π· = {β¨π₯, π¦β© β£ ((π₯ β π» β§ π¦ β π») β§ (1st βπ¦) β (1st βπ₯))} β β’ (π» = βͺ βͺ π· β§ (πΉ β (Filβπ) β (π» β (πΉ Γ π) β§ π· β DirRel))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |