P. 202 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20101-20200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fgval 20101*	The filter generating class gives a filter for every filter base. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( F e. ( fBas ` X ) -> ( X filGen F ) = { x e. ~P X | ( F i^i ~P x ) =/= (/) } )
Theorem	elfg 20102*	A condition for elements of a generated filter. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( F e. ( fBas ` X ) -> ( A e. ( X filGen F ) <-> ( A C_ X /\ E. x e. F x C_ A ) ) )
Theorem	ssfg 20103	A filter base is a subset of its generated filter. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( F e. ( fBas ` X ) -> F C_ ( X filGen F ) )
Theorem	fgss 20104	A bigger base generates a bigger filter. (Contributed by NM, 5-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) /\ F C_ G ) -> ( X filGen F ) C_ ( X filGen G ) )
Theorem	fgss2 20105*	A condition for a filter to be finer than another involving their filter bases. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( ( X filGen F ) C_ ( X filGen G ) <-> A. x e. F E. y e. G y C_ x ) )
Theorem	fgfil 20106	A filter generates itself. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( F e. ( Fil ` X ) -> ( X filGen F ) = F )
Theorem	elfilss 20107*	An element belongs to a filter iff any element below it does. (Contributed by Stefan O'Rear, 2-Aug-2015.)
|- ( ( F e. ( Fil ` X ) /\ A C_ X ) -> ( A e. F <-> E. t e. F t C_ A ) )
Theorem	filfinnfr 20108	No filter containing a finite element is free. (Contributed by Jeff Hankins, 5-Dec-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( ( F e. ( Fil ` X ) /\ S e. F /\ S e. Fin ) -> |^| F =/= (/) )
Theorem	fgcl 20109	A generated filter is a filter. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( F e. ( fBas ` X ) -> ( X filGen F ) e. ( Fil ` X ) )
Theorem	fgabs 20110	Absorption law for filter generation. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ( ( F e. ( fBas ` Y ) /\ Y C_ X ) -> ( X filGen ( Y filGen F ) ) = ( X filGen F ) )
Theorem	neifil 20111	The neighborhoods of a nonempty set is a filter. Example 2 of [BourbakiTop1] p. I.36. (Contributed by FL, 18-Sep-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ S C_ X /\ S =/= (/) ) -> ( ( nei ` J ) ` S ) e. ( Fil ` X ) )
Theorem	filunibas 20112	Recover the base set from a filter. (Contributed by Stefan O'Rear, 2-Aug-2015.)
|- ( F e. ( Fil ` X ) -> U. F = X )
Theorem	filunirn 20113	Two ways to express a filter on an unspecified base. (Contributed by Stefan O'Rear, 2-Aug-2015.)
|- ( F e. U. ran Fil <-> F e. ( Fil ` U. F ) )
Theorem	filcon 20114	A filter gives rise to a connected topology. (Contributed by Jeff Hankins, 6-Dec-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( F e. ( Fil ` X ) -> ( F u. { (/) } ) e. Con )
Theorem	fbasrn 20115*	Given a filter on a domain, produce a filter on the range. (Contributed by Jeff Hankins, 7-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- C = ran ( x e. B |-> ( F " x ) )   =>    |- ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> C e. ( fBas ` Y ) )
Theorem	filuni 20116*	The union of a nonempty set of filters with a common base and closed under pairwise union is a filter. (Contributed by Mario Carneiro, 28-Nov-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( ( F C_ ( Fil ` X ) /\ F =/= (/) /\ A. f e. F A. g e. F ( f u. g ) e. F ) -> U. F e. ( Fil ` X ) )
Theorem	trfil1 20117	Conditions for the trace of a filter L to be a filter. (Contributed by FL, 2-Sep-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> A = U. ( L ↾t A ) )
Theorem	trfil2 20118*	Conditions for the trace of a filter L to be a filter. (Contributed by FL, 2-Sep-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( ( L ↾t A ) e. ( Fil ` A ) <-> A. v e. L ( v i^i A ) =/= (/) ) )
Theorem	trfil3 20119	Conditions for the trace of a filter L to be a filter. (Contributed by Stefan O'Rear, 2-Aug-2015.)
|- ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( ( L ↾t A ) e. ( Fil ` A ) <-> -. ( Y \ A ) e. L ) )
Theorem	trfilss 20120	If A is a member of the filter, then the filter truncated to A is a subset of the original filter. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( F ↾t A ) C_ F )
Theorem	fgtr 20121	If A is a member of the filter, then truncating F to A and regenerating the behavior outside A using filGen recovers the original filter. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( X filGen ( F ↾t A ) ) = F )
Theorem	trfg 20122	The trace operation and the filGen operation are inverses to one another in some sense, with filGen growing the base set and ↾t shrinking it. See fgtr 20121 for the converse cancellation law. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ( ( F e. ( Fil ` A ) /\ A C_ X /\ X e. V ) -> ( ( X filGen F ) ↾t A ) = F )
Theorem	trnei 20123	The trace, over a set A, of the filter of the neighborhoods of a point P is a filter iff P belongs to the closure of A. (This is trfil2 20118 applied to a filter of neighborhoods.) (Contributed by FL, 15-Sep-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( ( J e. (TopOn ` Y ) /\ A C_ Y /\ P e. Y ) -> ( P e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { P } ) ↾t A ) e. ( Fil ` A ) ) )
Theorem	cfinfil 20124*	Relative complements of the finite parts of an infinite set is a filter. When A = NN the set of the relative complements is called Frechet's filter and is used to define the concept of limit of a sequence. (Contributed by FL, 14-Jul-2008.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( ( X e. V /\ A C_ X /\ -. A e. Fin ) -> { x e. ~P X | ( A \ x ) e. Fin } e. ( Fil ` X ) )
Theorem	csdfil 20125*	The set of all elements whose complement is dominated by the base set is a filter. (Contributed by Mario Carneiro, 14-Dec-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( ( X e. dom card /\ om ~<_ X ) -> { x e. ~P X | ( X \ x ) ~< X } e. ( Fil ` X ) )
Theorem	supfil 20126*	The supersets of a nonempty set which are also subsets of a given base set form a filter. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.)
|- ( ( A e. V /\ B C_ A /\ B =/= (/) ) -> { x e. ~P A | B C_ x } e. ( Fil ` A ) )
Theorem	zfbas 20127	The set of upper sets of integers is a filter base on ZZ, which corresponds to convergence of sequences on ZZ. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- ran ZZ>= e. ( fBas ` ZZ )
Theorem	uzrest 20128	The restriction of the set of upper sets of integers to an upper set of integers is the set of upper sets of integers based at a point above the cutoff. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- Z = ( ZZ>= ` M )   =>    |- ( M e. ZZ -> ( ran ZZ>= ↾t Z ) = ( ZZ>= " Z ) )
Theorem	uzfbas 20129	The set of upper sets of integers based at a point in a fixed upper integer set like NN is a filter base on NN, which corresponds to convergence of sequences on NN. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- Z = ( ZZ>= ` M )   =>    |- ( M e. ZZ -> ( ZZ>= " Z ) e. ( fBas ` Z ) )
12.2.3  Ultrafilters
Syntax	cufil 20130	Extend class notation with the ultrafilters-on-a-set function.
class UFil
Syntax	cufl 20131	Extend class notation with the ultrafilter lemma.
class UFL
Definition	df-ufil 20132*	Define the set of ultrafilters on a set. An ultrafilter is a filter that gives a definite result for every subset. (Contributed by Jeff Hankins, 30-Nov-2009.)
|- UFil = ( g e. _V |-> { f e. ( Fil ` g ) | A. x e. ~P g ( x e. f \/ ( g \ x ) e. f ) } )
Definition	df-ufl 20133*	Define the class of base sets for which the ultrafilter lemma filssufil 20143 holds. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- UFL = { x | A. f e. ( Fil ` x ) E. g e. ( UFil ` x ) f C_ g }
Theorem	isufil 20134*	The property of being an ultrafilter. (Contributed by Jeff Hankins, 30-Nov-2009.) (Revised by Mario Carneiro, 29-Jul-2015.)
|- ( F e. ( UFil ` X ) <-> ( F e. ( Fil ` X ) /\ A. x e. ~P X ( x e. F \/ ( X \ x ) e. F ) ) )
Theorem	ufilfil 20135	An ultrafilter is a filter. (Contributed by Jeff Hankins, 1-Dec-2009.) (Revised by Mario Carneiro, 29-Jul-2015.)
|- ( F e. ( UFil ` X ) -> F e. ( Fil ` X ) )
Theorem	ufilss 20136	For any subset of the base set of an ultrafilter, either the set is in the ultrafilter or the complement is. (Contributed by Jeff Hankins, 1-Dec-2009.) (Revised by Mario Carneiro, 29-Jul-2015.)
|- ( ( F e. ( UFil ` X ) /\ S C_ X ) -> ( S e. F \/ ( X \ S ) e. F ) )
Theorem	ufilb 20137	The complement is in an ultrafilter iff the set is not. (Contributed by Mario Carneiro, 11-Dec-2013.) (Revised by Mario Carneiro, 29-Jul-2015.)
|- ( ( F e. ( UFil ` X ) /\ S C_ X ) -> ( -. S e. F <-> ( X \ S ) e. F ) )
Theorem	ufilmax 20138	Any filter finer than an ultrafilter is actually equal to it. (Contributed by Jeff Hankins, 1-Dec-2009.) (Revised by Mario Carneiro, 29-Jul-2015.)
|- ( ( F e. ( UFil ` X ) /\ G e. ( Fil ` X ) /\ F C_ G ) -> F = G )
Theorem	isufil2 20139*	The maximal property of an ultrafilter. (Contributed by Jeff Hankins, 30-Nov-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( F e. ( UFil ` X ) <-> ( F e. ( Fil ` X ) /\ A. f e. ( Fil ` X ) ( F C_ f -> F = f ) ) )
Theorem	ufprim 20140	An ultrafilter is a prime filter. (Contributed by Jeff Hankins, 1-Jan-2010.) (Revised by Mario Carneiro, 2-Aug-2015.)
|- ( ( F e. ( UFil ` X ) /\ A C_ X /\ B C_ X ) -> ( ( A e. F \/ B e. F ) <-> ( A u. B ) e. F ) )
Theorem	trufil 20141	Conditions for the trace of an ultrafilter L to be an ultrafilter. (Contributed by Mario Carneiro, 27-Aug-2015.)
|- ( ( L e. ( UFil ` Y ) /\ A C_ Y ) -> ( ( L ↾t A ) e. ( UFil ` A ) <-> A e. L ) )
Theorem	filssufilg 20142*	A filter is contained in some ultrafilter. This version of filssufil 20143 contains the choice as a hypothesis (in the assumption that ~P ~P X is well-orderable). (Contributed by Mario Carneiro, 24-May-2015.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( ( F e. ( Fil ` X ) /\ ~P ~P X e. dom card ) -> E. f e. ( UFil ` X ) F C_ f )
Theorem	filssufil 20143*	A filter is contained in some ultrafilter. (Requires the Axiom of Choice, via numth3 8841.) (Contributed by Jeff Hankins, 2-Dec-2009.) (Revised by Stefan O'Rear, 29-Jul-2015.)
|- ( F e. ( Fil ` X ) -> E. f e. ( UFil ` X ) F C_ f )
Theorem	isufl 20144*	Define the (strong) ultrafilter lemma, parameterized over base sets. A set X satisfies the ultrafilter lemma if every filter on X is a subset of some ultrafilter. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( X e. V -> ( X e. UFL <-> A. f e. ( Fil ` X ) E. g e. ( UFil ` X ) f C_ g ) )
Theorem	ufli 20145*	Property of a set that satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( ( X e. UFL /\ F e. ( Fil ` X ) ) -> E. f e. ( UFil ` X ) F C_ f )
Theorem	numufl 20146	Consequence of filssufilg 20142: a set whose double powerset is well-orderable satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( ~P ~P X e. dom card -> X e. UFL )
Theorem	fiufl 20147	A finite set satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( X e. Fin -> X e. UFL )
Theorem	acufl 20148	The axiom of choice implies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- (CHOICE -> UFL = _V )
Theorem	ssufl 20149	If Y is a subset of X and filters extend to ultrafilters in X, then they still do in Y. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( ( X e. UFL /\ Y C_ X ) -> Y e. UFL )
Theorem	ufileu 20150*	If the ultrafilter containing a given filter is unique, the filter is an ultrafilter. (Contributed by Jeff Hankins, 3-Dec-2009.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- ( F e. ( Fil ` X ) -> ( F e. ( UFil ` X ) <-> E! f e. ( UFil ` X ) F C_ f ) )
Theorem	filufint 20151*	A filter is equal to the intersection of the ultrafilters containing it. (Contributed by Jeff Hankins, 1-Jan-2010.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( F e. ( Fil ` X ) -> |^| { f e. ( UFil ` X ) | F C_ f } = F )
Theorem	uffix 20152*	Lemma for fixufil 20153 and uffixfr 20154. (Contributed by Mario Carneiro, 12-Dec-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( ( X e. V /\ A e. X ) -> ( { { A } } e. ( fBas ` X ) /\ { x e. ~P X | A e. x } = ( X filGen { { A } } ) ) )
Theorem	fixufil 20153*	The condition describing a fixed ultrafilter always produces an ultrafilter. (Contributed by Jeff Hankins, 9-Dec-2009.) (Revised by Mario Carneiro, 12-Dec-2013.) (Revised by Stefan O'Rear, 29-Jul-2015.)
|- ( ( X e. V /\ A e. X ) -> { x e. ~P X | A e. x } e. ( UFil ` X ) )
Theorem	uffixfr 20154*	An ultrafilter is either fixed or free. A fixed ultrafilter is called principal (generated by a single element A), and a free ultrafilter is called nonprincipal (having empty intersection). Note that examples of free ultrafilters cannot be defined in ZFC without some form of global choice. (Contributed by Jeff Hankins, 4-Dec-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( F e. ( UFil ` X ) -> ( A e. |^| F <-> F = { x e. ~P X | A e. x } ) )
Theorem	uffix2 20155*	A classification of fixed ultrafilters. (Contributed by Mario Carneiro, 24-May-2015.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( F e. ( UFil ` X ) -> ( |^| F =/= (/) <-> E. x e. X F = { y e. ~P X | x e. y } ) )
Theorem	uffixsn 20156	The singleton of the generator of a fixed ultrafilter is in the filter. (Contributed by Mario Carneiro, 24-May-2015.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> { A } e. F )
Theorem	ufildom1 20157	An ultrafilter is generated by at most one element (because free ultrafilters have no generators and fixed ultrafilters have exactly one). (Contributed by Mario Carneiro, 24-May-2015.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( F e. ( UFil ` X ) -> |^| F ~<_ 1o )
Theorem	uffinfix 20158*	An ultrafilter containing a finite element is fixed. (Contributed by Jeff Hankins, 5-Dec-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( ( F e. ( UFil ` X ) /\ S e. F /\ S e. Fin ) -> E. x e. X F = { y e. ~P X | x e. y } )
Theorem	cfinufil 20159*	An ultrafilter is free iff it contains the Fréchet filter cfinfil 20124 as a subset. (Contributed by NM, 14-Jul-2008.) (Revised by Stefan O'Rear, 2-Aug-2015.)
|- ( F e. ( UFil ` X ) -> ( |^| F = (/) <-> { x e. ~P X | ( X \ x ) e. Fin } C_ F ) )
Theorem	ufinffr 20160*	An infinite subset is contained in a free ultrafilter. (Contributed by Jeff Hankins, 6-Dec-2009.) (Revised by Mario Carneiro, 4-Dec-2013.)
|- ( ( X e. B /\ A C_ X /\ om ~<_ A ) -> E. f e. ( UFil ` X ) ( A e. f /\ |^| f = (/) ) )
Theorem	ufilen 20161*	Any infinite set has an ultrafilter on it whose elements are of the same cardinality as the set. Any such ultrafilter is necessarily free. (Contributed by Jeff Hankins, 7-Dec-2009.) (Revised by Stefan O'Rear, 3-Aug-2015.)
|- ( om ~<_ X -> E. f e. ( UFil ` X ) A. x e. f x ~~ X )
Theorem	ufildr 20162	An ultrafilter gives rise to a connected door topology. (Contributed by Jeff Hankins, 6-Dec-2009.) (Revised by Stefan O'Rear, 3-Aug-2015.)
|- J = ( F u. { (/) } )   =>    |- ( F e. ( UFil ` X ) -> ( J u. ( Clsd ` J ) ) = ~P X )
Theorem	fin1aufil 20163	There are no definable free ultrafilters in ZFC. However, there are free ultrafilters in some choice-denying constructions. Here we show that given an amorphous set (a.k.a. a Ia-finite I-infinite set) X, the set of infinite subsets of X is a free ultrafilter on X. (Contributed by Mario Carneiro, 20-May-2015.)
|- F = ( ~P X \ Fin )   =>    |- ( X e. (FinIa \ Fin ) -> ( F e. ( UFil ` X ) /\ |^| F = (/) ) )
12.2.4  Filter limits
Syntax	cfm 20164	Extend class definition to include the neighborhood filter mapping function.
class FilMap
Syntax	cflim 20165	Extend class notation with a function returning the limit of a filter.
class fLim
Syntax	cflf 20166	Extend class definition to include the function for filter-based function limits.
class fLimf
Syntax	cfcls 20167	Extend class definition to include the cluster point function on filters.
class fClus
Syntax	cfcf 20168	Extend class definition to include the function for cluster points of a function.
class fClusf
Definition	df-fm 20169*	Define a function that takes a filter to a neighborhood filter of the range. (Since we now allow filter bases to have support smaller than the base set, the function has to come first to ensure that curryings are sets.) (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 20-Jul-2015.)
|- FilMap = ( x e. _V , f e. _V |-> ( y e. ( fBas ` dom f ) |-> ( x filGen ran ( t e. y |-> ( f " t ) ) ) ) )
Definition	df-flim 20170*	Define a function (indexed by a topology j) whose value is the limits of a filter f. (Contributed by Jeff Hankins, 4-Sep-2009.)
|- fLim = ( j e. Top , f e. U. ran Fil |-> { x e. U. j | ( ( ( nei ` j ) ` { x } ) C_ f /\ f C_ ~P U. j ) } )
Definition	df-flf 20171*	Define a function that gives the limits of a function f in the filter sense. (Contributed by Jeff Hankins, 14-Oct-2009.)
|- fLimf = ( x e. Top , y e. U. ran Fil |-> ( f e. ( U. x ^m U. y ) |-> ( x fLim ( ( U. x FilMap f ) ` y ) ) ) )
Definition	df-fcls 20172*	Define a function that takes a filter in a topology to its set of cluster points. (Contributed by Jeff Hankins, 10-Nov-2009.)
|- fClus = ( j e. Top , f e. U. ran Fil |-> if ( U. j = U. f , |^|_ x e. f ( ( cls ` j ) ` x ) , (/) ) )
Definition	df-fcf 20173*	Define a function that gives the cluster points of a function. (Contributed by Jeff Hankins, 24-Nov-2009.)
|- fClusf = ( j e. Top , f e. U. ran Fil |-> ( g e. ( U. j ^m U. f ) |-> ( j fClus ( ( U. j FilMap g ) ` f ) ) ) )
Theorem	fmval 20174*	Introduce a function that takes a function from a filtered domain to a set and produces a filter which consists of supersets of images of filter elements. The functions which are dealt with by this function are similar to nets in topology. For example, suppose we have a sequence filtered by the filter generated by its tails under the usual positive integer ordering. Then the elements of this filter are precisely the supersets of tails of this sequence. Under this definition, it is not too difficult to see that the limit of a function in the filter sense captures the notion of convergence of a sequence. As a result, the notion of a filter generalizes many ideas associated with sequences, and this function is one way to make that relationship precise in Metamath. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- ( ( X e. A /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` B ) = ( X filGen ran ( y e. B |-> ( F " y ) ) ) )
Theorem	fmfil 20175	A mapping filter is a filter. (Contributed by Jeff Hankins, 18-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- ( ( X e. A /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` B ) e. ( Fil ` X ) )
Theorem	fmf 20176	Pushing-forward via a function induces a mapping on filters. (Contributed by Stefan O'Rear, 8-Aug-2015.)
|- ( ( X e. A /\ Y e. B /\ F : Y --> X ) -> ( X FilMap F ) : ( fBas ` Y ) --> ( Fil ` X ) )
Theorem	fmss 20177	A finer filter produces a finer image filter. (Contributed by Jeff Hankins, 16-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- ( ( ( X e. A /\ B e. ( fBas ` Y ) /\ C e. ( fBas ` Y ) ) /\ ( F : Y --> X /\ B C_ C ) ) -> ( ( X FilMap F ) ` B ) C_ ( ( X FilMap F ) ` C ) )
Theorem	elfm 20178*	An element of a mapping filter. (Contributed by Jeff Hankins, 8-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( A e. ( ( X FilMap F ) ` B ) <-> ( A C_ X /\ E. x e. B ( F " x ) C_ A ) ) )
Theorem	elfm2 20179*	An element of a mapping filter. (Contributed by Jeff Hankins, 26-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- L = ( Y filGen B )   =>    |- ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( A e. ( ( X FilMap F ) ` B ) <-> ( A C_ X /\ E. x e. L ( F " x ) C_ A ) ) )
Theorem	fmfg 20180	The image filter of a filter base is the same as the image filter of its generated filter. (Contributed by Jeff Hankins, 18-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- L = ( Y filGen B )   =>    |- ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` B ) = ( ( X FilMap F ) ` L ) )
Theorem	elfm3 20181*	An alternate formulation of elementhood in a mapping filter that requires F to be onto. (Contributed by Jeff Hankins, 1-Oct-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- L = ( Y filGen B )   =>    |- ( ( B e. ( fBas ` Y ) /\ F : Y -onto-> X ) -> ( A e. ( ( X FilMap F ) ` B ) <-> E. x e. L A = ( F " x ) ) )
Theorem	imaelfm 20182	An image of a filter element is in the image filter. (Contributed by Jeff Hankins, 5-Oct-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- L = ( Y filGen B )   =>    |- ( ( ( X e. A /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ S e. L ) -> ( F " S ) e. ( ( X FilMap F ) ` B ) )
Theorem	rnelfmlem 20183*	Lemma for rnelfm 20184. (Contributed by Jeff Hankins, 14-Nov-2009.)
|- ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ran ( x e. L |-> ( `' F " x ) ) e. ( fBas ` Y ) )
Theorem	rnelfm 20184	A condition for a filter to be an image filter for a given function. (Contributed by Jeff Hankins, 14-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> ( L e. ran ( X FilMap F ) <-> ran F e. L ) )
Theorem	fmfnfmlem1 20185*	Lemma for fmfnfm 20189. (Contributed by Jeff Hankins, 18-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- ( ph -> B e. ( fBas ` Y ) )   &    |- ( ph -> L e. ( Fil ` X ) )   &    |- ( ph -> F : Y --> X )   &    |- ( ph -> ( ( X FilMap F ) ` B ) C_ L )   =>    |- ( ph -> ( s e. ( fi ` B ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) )
Theorem	fmfnfmlem2 20186*	Lemma for fmfnfm 20189. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- ( ph -> B e. ( fBas ` Y ) )   &    |- ( ph -> L e. ( Fil ` X ) )   &    |- ( ph -> F : Y --> X )   &    |- ( ph -> ( ( X FilMap F ) ` B ) C_ L )   =>    |- ( ph -> ( E. x e. L s = ( `' F " x ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) )
Theorem	fmfnfmlem3 20187*	Lemma for fmfnfm 20189. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- ( ph -> B e. ( fBas ` Y ) )   &    |- ( ph -> L e. ( Fil ` X ) )   &    |- ( ph -> F : Y --> X )   &    |- ( ph -> ( ( X FilMap F ) ` B ) C_ L )   =>    |- ( ph -> ( fi ` ran ( x e. L |-> ( `' F " x ) ) ) = ran ( x e. L |-> ( `' F " x ) ) )
Theorem	fmfnfmlem4 20188*	Lemma for fmfnfm 20189. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- ( ph -> B e. ( fBas ` Y ) )   &    |- ( ph -> L e. ( Fil ` X ) )   &    |- ( ph -> F : Y --> X )   &    |- ( ph -> ( ( X FilMap F ) ` B ) C_ L )   =>    |- ( ph -> ( t e. L <-> ( t C_ X /\ E. s e. ( fi ` ( B u. ran ( x e. L |-> ( `' F " x ) ) ) ) ( F " s ) C_ t ) ) )
Theorem	fmfnfm 20189*	A filter finer than an image filter is an image filter of the same function. (Contributed by Jeff Hankins, 13-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- ( ph -> B e. ( fBas ` Y ) )   &    |- ( ph -> L e. ( Fil ` X ) )   &    |- ( ph -> F : Y --> X )   &    |- ( ph -> ( ( X FilMap F ) ` B ) C_ L )   =>    |- ( ph -> E. f e. ( Fil ` Y ) ( B C_ f /\ L = ( ( X FilMap F ) ` f ) ) )
Theorem	fmufil 20190	An image filter of an ultrafilter is an ultrafilter. (Contributed by Jeff Hankins, 11-Dec-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
|- ( ( X e. A /\ L e. ( UFil ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` L ) e. ( UFil ` X ) )
Theorem	fmid 20191	The filter map applied to the identity. (Contributed by Jeff Hankins, 8-Nov-2009.) (Revised by Mario Carneiro, 27-Aug-2015.)
|- ( F e. ( Fil ` X ) -> ( ( X FilMap ( _I |` X ) ) ` F ) = F )
Theorem	fmco 20192	Composition of image filters. (Contributed by Mario Carneiro, 27-Aug-2015.)
|- ( ( ( X e. V /\ Y e. W /\ B e. ( fBas ` Z ) ) /\ ( F : Y --> X /\ G : Z --> Y ) ) -> ( ( X FilMap ( F o. G ) ) ` B ) = ( ( X FilMap F ) ` ( ( Y FilMap G ) ` B ) ) )
Theorem	ufldom 20193	The ultrafilter lemma property is a cardinal invariant, so since it transfers to subsets it also transfers over set dominance. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( ( X e. UFL /\ Y ~<_ X ) -> Y e. UFL )
Theorem	flimval 20194*	The set of limit points of a filter. (Contributed by Jeff Hankins, 4-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ F e. U. ran Fil ) -> ( J fLim F ) = { x e. X | ( ( ( nei ` J ) ` { x } ) C_ F /\ F C_ ~P X ) } )
Theorem	elflim2 20195	The predicate "is a limit point of a filter." (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- X = U. J   =>    |- ( A e. ( J fLim F ) <-> ( ( J e. Top /\ F e. U. ran Fil /\ F C_ ~P X ) /\ ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) )
Theorem	flimtop 20196	Reverse closure for the limit point predicate. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 9-Aug-2015.)
|- ( A e. ( J fLim F ) -> J e. Top )
Theorem	flimneiss 20197	A filter contains the neighborhood filter as a subfilter. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 9-Aug-2015.)
|- ( A e. ( J fLim F ) -> ( ( nei ` J ) ` { A } ) C_ F )
Theorem	flimnei 20198	A filter contains all of the neighborhoods of its limit points. (Contributed by Jeff Hankins, 4-Sep-2009.) (Revised by Mario Carneiro, 9-Apr-2015.)
|- ( ( A e. ( J fLim F ) /\ N e. ( ( nei ` J ) ` { A } ) ) -> N e. F )
Theorem	flimelbas 20199	A limit point of a filter belongs to its base set. (Contributed by Jeff Hankins, 4-Sep-2009.) (Revised by Mario Carneiro, 9-Apr-2015.)
|- X = U. J   =>    |- ( A e. ( J fLim F ) -> A e. X )
Theorem	flimfil 20200	Reverse closure for the limit point predicate. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 6-Aug-2015.)
|- X = U. J   =>    |- ( A e. ( J fLim F ) -> F e. ( Fil ` X ) )