mmtheorems103 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17411

Statement List for Metamath Proof Explorer - 10201-10300 - Page 103 of 175

Type	Label	Description
Statement
Theorem	symgoprab 10201	Two ways to express the symmetry-group operator class abstraction. (Contributed by Paul Chapman, 25-Feb-2008.)
|- A e. _V   &   |- P = {x | x:A-1-1-onto->A}   =>   |- {<.<.f, g>., h>. | (f:A-1-1-onto->A /\ g:A-1-1-onto->A /\ h = (f o. g))} = {<.<.f, g>., h>. | ((f e. P /\ g e. P) /\ h = (f o. g))}
Theorem	symgval 10202	The value of the symmetry group function at A. (Contributed by Paul Chapman, 25-Feb-2008.)
|- A e. _V   &   |- P = {x | x:A-1-1-onto->A}   =>   |- (SymGrp` A) = {<.<.f, g>., h>. | ((f e. P /\ g e. P) /\ h = (f o. g))}
Theorem	symgoprv 10203	The value of the group operation of the symmetry group on A. (Contributed by Paul Chapman, 25-Feb-2008.)
|- A e. _V   &   |- P = {x | x:A-1-1-onto->A}   =>   |- ((F e. P /\ G e. P) -> (F(SymGrp` A)G) = (F o. G))
Theorem	symgf 10204	The domain and codomain of the group operation of the symmetry group on A. (Contributed by Paul Chapman, 25-Feb-2008.)
|- A e. _V   &   |- P = {x | x:A-1-1-onto->A}   =>   |- (SymGrp` A):(P X. P)-->P
Theorem	symggrpi 10205	The symmetry group on A is a group (inference version). (Contributed by Paul Chapman, 4-Jun-2008.)
|- A e. _V   =>   |- (SymGrp` A) e. Grp
Theorem	symgidi 10206	The value of the identity element of the symmetry group on A (Contributed by Paul Chapman, 25-Jul-2008.)
|- A e. _V   =>   |- (Id` (SymGrp` A)) = ( _I |` A)
Order theory
Syntax	ccha 10207	Extend class notation with the class of all totally ordered sets.
class Toset
Definition	df-toset 10208	Define the class of all totally ordered sets. (Contributed by FL, 3-Nov-2009.)
|- Toset = (Poset i^i {r | A.x e. U.U.rA.y e. U.U.r(xry \/ yrx)})
Theorem	istoset 10209	The predicate is a toset. (Contributed by FL, 3-Nov-2009.)
|- X = U.U.R   =>   |- (R e. A -> (R e. Toset <-> (R e. Poset /\ A.x e. X A.y e. X (xRy \/ yRx))))
Finite intersections
Syntax	cfi 10210	Extend class notation with the function whose value is the class of all the finite intersections of the elements of a given set.
class fi
Definition	df-fi 10211	Function whose value is the class of all the finite intersections of the elements of x. (Contributed by FL, 2-Sep-2008.)
|- fi = {<.x, y>. | y = {u | E.z(z C_ x /\ z e. Fin /\ u = |^|z)}}
Theorem	fiv 10212	The set of all the finite intersections of the elements of A. (Contributed by FL, 2-Sep-2008.)
|- (A e. B -> ( fi ` A) = {u | E.z(z C_ A /\ z e. Fin /\ u = |^|z)})
Theorem	fine 10213	Condition required for a nonempty finite intersection. (Contributed by FL, 2-Sep-2008.)
|- (A =/= (/) -> {x | E.y(y C_ A /\ y e. Fin /\ x = |^|y)} =/= (/))
Theorem	fine2 10214	If A is not empty, the class of all the finite intersections of A is not empty either. (Contributed by FL, 2-Sep-2008.)
|- (A e. B -> (A =/= (/) -> ( fi ` A) =/= (/)))
Theorem	abfi 10215	Any element of A is the intersection of a finite subclass of A. (Contributed by FL, 2-Sep-2008.)
|- A C_ {x | E.y(y C_ A /\ y e. Fin /\ x = |^|y)}
Theorem	abfi2 10216	Any element of a set A is the intersection of a finite subset of A. (Contributed by FL, 27-Apr-2008.)
|- (A e. B -> A C_ ( fi ` A))
Theorem	spfi 10217	Specific properties of a finite intersection. (Contributed by FL, 2-Sep-2008.)
|- (A e. B -> (A e. {x | E.y(y C_ C /\ y e. Fin /\ x = |^|y)} <-> E.y(y C_ C /\ y e. Fin /\ A = |^|y)))
Theorem	sppfi 10218	Specific properties of an element of ( fi ` C). (Contributed by FL, 2-Sep-2008.)
|- ((A e. B /\ C e. D) -> (A e. ( fi ` C) <-> E.z(z C_ C /\ z e. Fin /\ A = |^|z)))
Theorem	fiuni 10219	The union of the finite intersections of a set is simply the union of the set itself. (Contributed by Jeff Hankins, 5-Sep-2009.)
|- (A e. B -> U.A = U.( fi ` A))
Theorem	fiiu2 10220	If A is the intersection of a finite set of elements of B then A C_ U.B. (Contributed by FL, 2-Sep-2008.)
|- (B e. C -> (A e. ( fi ` B) -> A C_ U.B))
Theorem	fibas 10221	A collection of finite intersections is a basis. The initial set is a subbasis for the topology. Compare subbas 8914. (Contributed by Jeff Hankins, 25-Aug-2009.)
|- (A e. B -> ( fi ` A) e. Bases)
Theorem	hausnei2 10222	The Hausdorff condition still holds if one considers general neighborhoods instead of open sets. (Contributed by Jeff Hankins, 5-Sep-2009.)
|- X = U.J   =>   |- (J e. Top -> (J e. Haus <-> A.x e. X A.y e. X (x =/= y -> E.u e. ((nei` J)` {x})E.v e. ((nei` J)` {y})(u i^i v) = (/))))
Theorem	tx1cn 10223	Continuity of the first projection map of a topological product. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- T = (R X.t S)   &   |- X = U.R   &   |- Y = U.S   &   |- Z = (X X. Y)   =>   |- ((R e. Top /\ S e. Top) -> (1st |` Z) e. (T Cn R))
Theorem	tx2cn 10224	Continuity of the second projection map of a topological product. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- T = (R X.t S)   &   |- X = U.R   &   |- Y = U.S   &   |- Z = (X X. Y)   =>   |- ((R e. Top /\ S e. Top) -> (2nd |` Z) e. (T Cn S))
Theorem	upxp 10225	Universal property of the Cartesian product considered as a categorical product in the category of sets. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- P = (1st |` (B X. C))   &   |- Q = (2nd |` (B X. C))   =>   |- ((A e. D /\ F:A-->B /\ G:A-->C) -> E!h(h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h)))
Theorem	uptx 10226	Universal property of the binary topological product. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- T = (R X.t S)   &   |- X = U.R   &   |- Y = U.S   &   |- Z = (X X. Y)   &   |- P = (1st |` Z)   &   |- Q = (2nd |` Z)   =>   |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> E!h e. (U Cn T)(F = (P o. h) /\ G = (Q o. h)))
Theorem	txcn 10227	A map into the product of two topological spaces is continuous iff both of its projections are continuous. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- T = (R X.t S)   &   |- X = U.R   &   |- Y = U.S   &   |- Z = (X X. Y)   &   |- W = U.U   &   |- P = (1st |` Z)   &   |- Q = (2nd |` Z)   =>   |- (((R e. Top /\ S e. Top /\ U e. Top) /\ F:W-->Z) -> (F e. (U Cn T) <-> ((P o. F) e. (U Cn R) /\ (Q o. F) e. (U Cn S))))
Theorem	txcnopab 10228	A map into the product of two topological spaces is continuous if both of its projections are continuous. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- T = (R X.t S)   &   |- W = U.U   &   |- H = {<.x, y>. | (x e. W /\ y = <.(F` x), (G` x)>.)}   =>   |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> H e. (U Cn T))
Theorem	2txcn 10229	The product map between two topological product spaces is continuous. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- T = (R X.t S)   &   |- L = (J X.t K)   &   |- X = U.R   &   |- Y = U.S   &   |- H = {<.<.x, y>., z>. | ((x e. X /\ y e. Y) /\ z = <.(F` x), (G` y)>.)}   =>   |- (((R e. Top /\ S e. Top) /\ (J e. Top /\ K e. Top) /\ (F e. (R Cn J) /\ G e. (S Cn K))) -> H e. (T Cn L))
Homeomorphisms
Syntax	chomeosm 10230	Extend class notation with the class of all homeomorphisms.
class Homeo
Syntax	chomeo 10231	Extend class notation with the relation "is homeomorph to.".
class ~=
Definition	df-homeo 10232	Function returning all the homeomorphisms from topology j to topology k.
|- Homeo = {<.<.j, k>., z>. | ((j e. Top /\ k e. Top) /\ z = {f | (f:U.j-1-1-onto->U.k /\ A.x e. j (f"x) e. k /\ A.x e. k (`'f"x) e. j)})}
Definition	df-hmph 10233	Definition of the relation x is homeomorph to y.
|- ~= = {<.x, y>. | (x e. Top /\ y e. Top /\ E.f f e. (x Homeo y))}
Theorem	homeofval 10234	The set of all the homeomorphisms between two topologies. (Contributed by FL, 20-Feb-2007.)
|- X = U.J   &   |- Y = U.K   =>   |- ((J e. Top /\ K e. Top) -> (J Homeo K) = {f | (f:X-1-1-onto->Y /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)})
Theorem	ishomeo 10235	The predicate F is a homeomorphism between topology J and topology K. Based on Bourbaki TG I.2. (Contributed by FL, 20-Feb-2007.)
|- X = U.J   &   |- Y = U.K   =>   |- ((J e. Top /\ K e. Top /\ F e. A) -> (F e. (J Homeo K) <-> (F:X-1-1-onto->Y /\ A.x e. J (F"x) e. K /\ A.x e. K (`'F"x) e. J)))
Theorem	hmeomap 10236	A homeomorphism is a 1-1-onto mapping. (Contributed by FL, 5-Mar-2007.)
|- X = U.J   &   |- Y = U.K   =>   |- ((J e. Top /\ K e. Top) -> (F e. (J Homeo K) -> F:X-1-1-onto->Y))
Theorem	hmeocna 10237	The image of an open set by the converse of a homeomorphism is an open set. (Contributed by FL, 5-Mar-2007.)
|- ((J e. Top /\ K e. Top) -> (F e. (J Homeo K) -> A.x e. K (`'F"x) e. J))
Theorem	hmeocnb 10238	The image of an open set by a homeomorphism is an open set. (Contributed by FL, 5-Mar-2007.)
|- ((J e. Top /\ K e. Top) -> (F e. (J Homeo K) -> A.x e. J (F"x) e. K))
Theorem	hmeobc 10239	A homeomorphism is a bicontinuous bijection. (Contributed by FL, 1-Sep-2008.)
|- X = U.J   &   |- Y = U.K   =>   |- ((J e. Top /\ K e. Top /\ F e. A) -> (F e. (J Homeo K) <-> (F:X-1-1-onto->Y /\ F e. (J Cn K) /\ `'F e. (K Cn J))))
Theorem	cnvhmpha 10240	The converse of a homeomorphism is a homeomorphism. (Contributed by FL, 5-Mar-2007.)
|- ((J e. Top /\ K e. Top) -> (F e. (J Homeo K) -> `'F e. (K Homeo J)))
Theorem	hmph 10241	Express the predicate J is homeomorph to K. (Contributed by FL, 20-Feb-2007.)
|- ((J e. Top /\ K e. Top) -> (J ~= K <-> E.f f e. (J Homeo K)))
Initial and final topologies
Syntax	csubsp 10242	Extend class notation with the function returning a subspace topology.
class subSp
Definition	df-subsp 10243	Function returning the subspace topology induced by the topology y and the set x.
|- subSp = {<.<.x, y>., z>. | (y e. Top /\ z = {u | E.v e. y u = (v i^i x)})}
Theorem	subsp 10244	The subspace topology induced by the topology J on the set A. (Contributed by FL, 4-Jun-2007.)
|- J e. Top   &   |- A e. _V   =>   |- (subSp` <.A, J>.) = {u | E.v e. J u = (v i^i A)}
Theorem	issubsp 10245	The predicate "is a subspace topology". (Contributed by FL, 22-Dec-2008.)
|- B e. _V   &   |- J e. Top   =>   |- (A e. C -> (A e. (subSp` <.B, J>.) <-> E.v e. J A = (v i^i B)))
Theorem	issubsplem1 10246	The predicate "is a subspace topology". (Contributed by FL, 28-Jan-2009.)
|- J e. Top   =>   |- ((A e. C /\ B e. _V) -> (A e. (subSp` <.B, J>.) <-> E.v e. J A = (v i^i B)))
Theorem	issubspt 10247	The predicate "is an open set of a subspace topology". (Contributed by FL, 28-Jan-2009.)
|- ((J e. Top /\ A e. C /\ B e. _V) -> (A e. (subSp` <.B, J>.) <-> E.v e. J A = (v i^i B)))
Theorem	elsubsp 10248	Result used many times. (Contributed by Jeff Hankins, 11-Jul-2009.)
|- X = U.J   =>   |- (((J e. Top /\ S C_ X) /\ (A e. J /\ B = (A i^i S))) -> B e. (subSp` <.S, J>.))
Theorem	subspid 10249	The subspace topology of the base set is the original topology. (Contributed by Jeff Hankins, 9-Jul-2009.)
|- X = U.J   =>   |- (J e. Top -> (subSp` <.X, J>.) = J)
Theorem	stoiglem 10250	The underlying set of a subspace topology. (Contributed by FL, 28-Jan-2009.)
|- J e. Top   &   |- A C_ U.J   =>   |- <.A, (subSp` <.A, J>.)>. e. TopSp
Theorem	stoig 10251	The topological space built with a subspace topology. (Contributed by FL, 28-Jan-2009.)
|- ((J e. Top /\ A C_ U.J) -> <.A, (subSp` <.A, J>.)>. e. TopSp)
Theorem	stoig2 10252	The underlying set of a subspace topology. (Contributed by FL, 28-Jan-2009.)
|- ((J e. Top /\ A C_ U.J) -> U.(subSp` <.A, J>.) = A)
Theorem	stoig3 10253	A subspace topology is a topology. (Contributed by FL, 28-Jan-2009.)
|- ((J e. Top /\ A C_ U.J) -> (subSp` <.A, J>.) e. Top)
Theorem	subcld 10254	A closed set of a subspace topology is a closed set of the original topology intersected with the subset. (Contributed by FL, 11-Jul-2009.)
|- X = U.J   =>   |- ((J e. Top /\ S C_ X) -> (A e. (Clsd` (subSp` <.S, J>.)) <-> E.x e. (Clsd` J)A = (x i^i S)))
Theorem	subtopmetlem 10255	Lemma for subtopmet 10256. (Contributed by Jeff Hankins, 21-Aug-2009.)
Theorem	subtopmet 10256	Two alternate formulations of a subspace topology of a metric space topology. (Contributed by Jeff Hankins, 21-Aug-2009.)
|- D = (C |` (Y X. Y))   &   |- X = dom dom C   &   |- J = (Open` C)   &   |- K = (Open` D)   =>   |- ((C e. Met /\ Y C_ X) -> (subSp` <.Y, J>.) = K)
Filter Bases
Syntax	cfbas 10257	Extend class definition to include the class of filter bases.
class fBas
Syntax	cfg 10258	Extend class definition to include the filter generating function.
class filGen
Definition	df-fbas 10259	Define the class of all filter bases. (Contributed by Jeff Hankins, 1-Sep-2009.)
|- fBas = {x | (x =/= (/) /\ (/) e/ x /\ A.y e. x A.z e. x (x i^i ~P(y i^i z)) =/= (/))}
Definition	df-fg 10260	Define the filter generating function. (Contributed by Jeff Hankins, 1-Sep-2009.)
|- filGen = {<.x, y>. | (x e. fBas /\ y = {z e. ~PU.x | (x i^i ~Pz) =/= (/)})}
Theorem	isfbas 10261	The predicate "F is a filter base." Note that some authors require filter bases to be closed under pairwise intersections, but that is not necessary under our definition. One advantage of this definition is that tails in a directed set form a filter base under our meaning. (Contributed by Jeff Hankins, 1-Sep-2009.)
|- (F e. A -> (F e. fBas <-> (F =/= (/) /\ (/) e/ F /\ A.x e. F A.y e. F (F i^i ~P(x i^i y)) =/= (/))))
Theorem	fbasne0 10262	There are no empty filter bases. (Contributed by Jeff Hankins, 1-Sep-2009.)
|- (F e. fBas -> F =/= (/))
Theorem	isfbas2 10263	The predicate "F is a filter base." (Contributed by Jeff Hankins, 1-Sep-2009.)
|- (F e. A -> (F e. fBas <-> (F =/= (/) /\ (/) e/ F /\ A.x e. F A.y e. F E.z e. F z C_ (x i^i y))))
Filters
Syntax	cfil 10264	Extend class notation with the class of all filters.
class Fil
Definition	df-fil 10265	The class of all filters. Bourbaki TG I.36 def. 1 axioms FI, FIIa, FIIb, FIII. Filters are used to define the concept of limit in the general case. It's a generalization of the idea of neighborhoods. Suppose you are in RR. With neighborhoods you can express the idea of a variable that tends to a specific number but you can't express the idea of a variable that tends to infinity. Filters relax the "axioms" of neighborhoods and then succeed in expressing the idea of something that tends to infinity. Filters were invented by Cartan in 1937 and made famous by Bourbaki in his treatise. A notion similar to the notion of filter is the concept of net invented by Moore and Smith in 1922. (Contributed by FL, 20-Jul-2007.)
|- Fil = {f | ((-. (/) e. f /\ U.f e. f) /\ A.xA.y((x e. f /\ y C_ U.f /\ x C_ y) -> y e. f) /\ A.x e. f A.y e. f (x i^i y) e. f)}
Theorem	isfil 10266	The predicate "is a filter." (Contributed by FL, 20-Jul-2007.)
|- X = U.F   =>   |- (F e. A -> (F e. Fil <-> ((-. (/) e. F /\ X e. F) /\ A.xA.y((x e. F /\ y C_ X /\ x C_ y) -> y e. F) /\ A.x e. F A.y e. F (x i^i y) e. F)))
Theorem	filusb 10267	The underlying set belongs to the filter. (Contributed by FL, 20-Jul-2007.)
|- X = U.F   =>   |- (F e. Fil -> X e. F)
Theorem	filesn 10268	The empty set doesn't belong to a filter. (Contributed by FL, 20-Jul-2007.)
|- (F e. Fil -> -. (/) e. F)
Theorem	filint 10269	A filter is closed under taking intersections. (Contributed by FL, 20-Jul-2007.)
|- ((F e. Fil /\ A e. F /\ B e. F) -> (A i^i B) e. F)
Theorem	fillsb 10270	A filter is closed under taking supersets. (Contributed by FL, 20-Jul-2007.)
|- X = U.F   =>   |- (F e. Fil -> ((A e. F /\ B C_ X /\ A C_ B) -> B e. F))
Theorem	fipfil 10271	The intersection of two elements of a filter can't be empty. (Contributed by FL, 19-Sep-2007.)
|- (F e. Fil -> ((A e. F /\ B e. F) -> (A i^i B) =/= (/)))
Theorem	fipfil2 10272	A filter has the finite intersection property. Bourbaki TG I.36 note of def. 1. (Contributed by FL, 2-Sep-2007.)
|- (F e. Fil -> ((A C_ F /\ A =/= (/) /\ A e. Fin) -> |^|A =/= (/)))
Theorem	emnfil 10273	The empty set is not a filter. Bourbaki TG I.36 def 1 note. (Contributed by FL, 31-Oct-2007.)
|- -. (/) e. Fil
Theorem	filintf 10274	The intersection of two filters is a filter. Use fiint 5650 to extend this property to the intersection of a finite set of filters. Bourbaki TG I.36 par. 3. (Contributed by FL, 19-Sep-2007.)
|- ((F e. Fil /\ G e. Fil /\ U.F = U.G) -> (F i^i G) e. Fil)
Theorem	oefil2 10275	A singleton is a filter. Bourbaki TG I.36, example 1. (Contributed by FL, 19-Sep-2007.)
|- ((A e. B /\ A =/= (/)) -> {A} e. Fil)
Theorem	filfbas 10276	A filter is a filter base. (Contributed by Jeff Hankins, 2-Sep-2009.)
|- (F e. Fil -> F e. fBas)
Theorem	0nelfb 10277	No filter base contains the empty set. (Contributed by Jeff Hankins, 1-Sep-2009.)
|- (F e. fBas -> (/) e/ F)
Theorem	fbasssin 10278	A filter base contains subsets of its pairwise intersections. (Contributed by Jeff Hankins, 1-Sep-2009.)
|- ((F e. fBas /\ A e. F /\ B e. F) -> E.x e. F x C_ (A i^i B))
Theorem	fbssint 10279	A filter base contains subsets of its finite intersections. (Contributed by Jeff Hankins, 1-Sep-2009.)
|- ((F e. fBas /\ A C_ F /\ A e. Fin) -> E.x e. F x C_ |^|A)
Theorem	infi 10280	The intersection of two finite intersections is a finite intersection. (Contributed by FL, 2-Sep-2008.)
|- (C e. D -> ((A e. ( fi ` C) /\ B e. ( fi ` C)) -> (A i^i B) e. ( fi ` C)))
Theorem	fsubbas 10281	A condition for a set to generate a filter base. (Contributed by Jeff Hankins, 2-Sep-2009.)
|- (A e. B -> (( fi ` A) e. fBas <-> (A =/= (/) /\ (/) e/ ( fi ` A))))
Theorem	fbunfip 10282	A helpful lemma for showing that certain sets generate filters. (Contributed by Jeff Hankins, 3-Sep-2009.)
|- ((F e. fBas /\ G e. fBas) -> ((/) e/ ( fi ` (F u. G)) <-> A.x e. F A.y e. G (x i^i y) =/= (/)))
Theorem	fgf 10283	The filter generating class gives a filter for every filter base. (Contributed by Jeff Hankins, 3-Sep-2009.)
|- X = U.F   =>   |- (F e. fBas -> (filGen` F) = {x e. ~PX | (F i^i ~Px) =/= (/)})
Theorem	elfg 10284	A condition for elements of a generated filter. (Contributed by Jeff Hankins, 3-Sep-2009.)
|- X = U.F   =>   |- (F e. fBas -> (A e. (filGen` F) <-> (A C_ X /\ E.x e. F x C_ A)))
Theorem	fbssfg 10285	A filter base is a subset of its generated filter. (Contributed by Jeff Hankins, 3-Sep-2009.)
|- (F e. fBas -> F C_ (filGen` F))
Theorem	fgbas 10286	The base set of a generated filter is the base set of the parent base. (Contributed by Jeff Hankins, 3-Sep-2009.)
|- X = U.F   =>   |- (F e. fBas -> X = U.(filGen` F))
Theorem	fgss 10287	A bigger base generates a bigger filter.
|- ((F e. fBas /\ G e. fBas /\ F C_ G) -> (filGen` F) C_ (filGen` G))
Theorem	fbfgss 10288	A condition for a filter to be finer than another involving their filter bases. (Contributed by Jeff Hankins, 3-Sep-2009.)
|- X = U.F   &   |- Y = U.G   =>   |- ((F e. fBas /\ G e. fBas /\ X = Y) -> ((filGen` F) C_ (filGen` G) <-> A.x e. F E.y e. G y C_ x))
Theorem	fgid 10289	A filter generates itself. (Contributed by Jeff Hankins, 5-Sep-2009.)
|- (F e. Fil -> (filGen` F) = F)
Theorem	fgfil 10290	A generated filter is a filter. (Contributed by Jeff Hankins, 3-Sep-2009.)
|- (F e. fBas -> (filGen` F) e. Fil)
Theorem	extbas1 10291	A way to extend the base set of a filter. (Contributed by Jeff Hankins, 6-Sep-2009.)
|- X = U.F   =>   |- ((F e. fBas /\ X C_ A) -> (F u. {A}) e. fBas)
Theorem	extbas2 10292	The base set of an extended filter. (Contributed by Jeff Hankins, 7-Sep-2009.)
|- X = U.F   =>   |- ((X C_ A /\ A e. B) -> U.(F u. {A}) = A)
Theorem	filrn 10293	Given a filter on a domain, produce a filter on the range. (Contributed by Jeff Hankins, 7-Sep-2009.)
|- X = U.B   &   |- C = {y | E.x e. B y = (F"x)}   =>   |- ((B e. fBas /\ F Fn X) -> C e. fBas)
Limits
Syntax	cflim1 10294	Extend class notation with a function returning the limit of a filter.
class fLim1
Definition	df-flim1 10295	Define a function (indexed by a topology x) whose value is the limits of a filter a.
|- fLim1 = {<.x, y>. | (x e. Top /\ y = {<.a, b>. | (a e. Fil /\ U.a = U.x /\ b = {l e. U.x | ((nei` x)` {l}) C_ a})})}
Theorem	sfvlim 10296	Functions whose values are the limits of the filters. (Contributed by FL, 1-Sep-2008.)
|- X = U.J   =>   |- (J e. Top -> (fLim1` J) = {<.a, b>. | (a e. Fil /\ U.a = X /\ b = {l e. X | ((nei` J)` {l}) C_ a})})
Theorem	limfil 10297	The set of limit points of a filter. (Contributed by Jeff Hankins, 4-Sep-2009.)
|- X = U.J   &   |- Y = U.F   =>   |- ((J e. Top /\ F e. Fil /\ X = Y) -> ((fLim1` J)` F) = {l e. X | ((nei` J)` {l}) C_ F})
Theorem	isfillim 10298	The predicate "is a limit point of a filter." (Contributed by Jeff Hankins, 4-Sep-2009.)
|- X = U.J   &   |- Y = U.F   =>   |- ((J e. Top /\ F e. Fil /\ X = Y) -> (A e. ((fLim1` J)` F) <-> (A e. X /\ ((nei` J)` {A}) C_ F)))
Theorem	limfilss 10299	A limit point of a filter is a limit point of a finer filter. (Contributed by Jeff Hankins, 5-Sep-2009.)
|- X = U.J   &   |- Y = U.F   &   |- Z = U.G   =>   |- ((((J e. Top /\ F e. Fil /\ G e. Fil) /\ X = Y /\ X = Z) /\ F C_ G /\ A e. ((fLim1` J)` F)) -> A e. ((fLim1` J)` G))
Theorem	flimelbas 10300	A limit point of a filter belongs to its base set. (Contributed by Jeff Hankins, 4-Sep-2009.)
|- X = U.J   &   |- Y = U.F   =>   |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fLim1` J)` F)) -> A e. X)