P. 324 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32301-32400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	exp510 32301	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
|- ( ( ph /\ ( ( ( ps /\ ch ) /\ th ) /\ ta ) ) -> et )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )
Theorem	exp511 32302	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
|- ( ( ph /\ ( ( ps /\ ( ch /\ th ) ) /\ ta ) ) -> et )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )
Theorem	exp512 32303	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
|- ( ( ph /\ ( ( ps /\ ch ) /\ ( th /\ ta ) ) ) -> et )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )
Theorem	3com12d 32304	Commutation in consequent. Swap 1st and 2nd. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ph -> ( ps /\ ch /\ th ) )   =>    |- ( ph -> ( ch /\ ps /\ th ) )
Theorem	imp5p 32305	A triple importation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
|- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )   =>    |- ( ph -> ( ps -> ( ( ch /\ th /\ ta ) -> et ) ) )
Theorem	imp5q 32306	A triple importation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
|- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )   =>    |- ( ( ph /\ ps ) -> ( ( ch /\ th /\ ta ) -> et ) )
Theorem	ecase13d 32307	Deduction for elimination by cases. (Contributed by Jeff Hankins, 18-Aug-2009.)
|- ( ph -> -. ch )   &    |- ( ph -> -. th )   &    |- ( ph -> ( ch \/ ps \/ th ) )   =>    |- ( ph -> ps )
Theorem	subtr 32308	Transitivity of implicit substitution. (Contributed by Jeff Hankins, 13-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
|- F/_ x A   &    |- F/_ x B   &    |- F/_ x Y   &    |- F/_ x Z   &    |- ( x = A -> X = Y )   &    |- ( x = B -> X = Z )   =>    |- ( ( A e. C /\ B e. D ) -> ( A = B -> Y = Z ) )
Theorem	subtr2 32309	Transitivity of implicit substitution into a wff. (Contributed by Jeff Hankins, 19-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
|- F/_ x A   &    |- F/_ x B   &    |- F/ x ps   &    |- F/ x ch   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ( x = B -> ( ph <-> ch ) )   =>    |- ( ( A e. C /\ B e. D ) -> ( A = B -> ( ps <-> ch ) ) )
Theorem	trer 32310*	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.)
|- ( A. a A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) -> ( .<_ i^i `' .<_ ) Er dom ( .<_ i^i `' .<_ ) )
Theorem	elicc3 32311	An equivalent membership condition for closed intervals. (Contributed by Jeff Hankins, 14-Jul-2009.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A [,] B ) <-> ( C e. RR* /\ A <_ B /\ ( C = A \/ ( A < C /\ C < B ) \/ C = B ) ) ) )
Theorem	finminlem 32312*	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.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x e. Fin ph -> E. x ( ph /\ A. y ( ( y C_ x /\ ps ) -> x = y ) ) )
Theorem	gtinf 32313*	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.)
|- ( ( ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. y e. S x <_ y ) /\ ( A e. RR /\ inf ( S , RR , < ) < A ) ) -> E. z e. S z < A )
Theorem	gtinfOLD 32314*	Any number greater than an infimum is greater than some element of the set. (Contributed by Jeff Hankins, 29-Sep-2013.) Obsolete version of gtinf 32313 as of 10-Oct-2021. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. y e. S x <_ y ) /\ ( A e. RR /\ sup ( S , RR , `' < ) < A ) ) -> E. z e. S z < A )
Theorem	opnrebl 32315*	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.)
|- ( A e. ( topGen ` ran (,) ) <-> ( A C_ RR /\ A. x e. A E. y e. RR+ ( ( x - y ) (,) ( x + y ) ) C_ A ) )
Theorem	opnrebl2 32316*	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.)
|- ( A e. ( topGen ` ran (,) ) <-> ( A C_ RR /\ A. x e. A A. y e. RR+ E. z e. RR+ ( z <_ y /\ ( ( x - z ) (,) ( x + z ) ) C_ A ) ) )
Theorem	nn0prpwlem 32317*	Lemma for nn0prpw 32318. Use strong induction to show that every positive integer has unique prime power divisors. (Contributed by Jeff Hankins, 28-Sep-2013.)
|- ( A e. NN -> A. k e. NN ( k < A -> E. p e. Prime E. n e. NN -. ( ( p ^ n ) || k <-> ( p ^ n ) || A ) ) )
Theorem	nn0prpw 32318*	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.)
|- ( ( A e. NN0 /\ B e. NN0 ) -> ( A = B <-> A. p e. Prime A. n e. NN ( ( p ^ n ) || A <-> ( p ^ n ) || B ) ) )
20.9.2  Basic topological facts
Theorem	topbnd 32319	Two equivalent expressions for the boundary of a topology. (Contributed by Jeff Hankins, 23-Sep-2009.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X ) -> ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) = ( ( ( cls ` J ) ` A ) \ ( ( int ` J ) ` A ) ) )
Theorem	opnbnd 32320	A set is open iff it is disjoint from its boundary. (Contributed by Jeff Hankins, 23-Sep-2009.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X ) -> ( A e. J <-> ( A i^i ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) ) = (/) ) )
Theorem	cldbnd 32321	A set is closed iff it contains its boundary. (Contributed by Jeff Hankins, 1-Oct-2009.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X ) -> ( A e. ( Clsd ` J ) <-> ( ( ( cls ` J ) ` A ) i^i ( ( cls ` J ) ` ( X \ A ) ) ) C_ A ) )
Theorem	ntruni 32322*	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.)
|- X = U. J   =>    |- ( ( J e. Top /\ O C_ ~P X ) -> U_ o e. O ( ( int ` J ) ` o ) C_ ( ( int ` J ) ` U. O ) )
Theorem	clsun 32323	A pairwise union of closures is the closure of the union. (Contributed by Jeff Hankins, 31-Aug-2009.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X /\ B C_ X ) -> ( ( cls ` J ) ` ( A u. B ) ) = ( ( ( cls ` J ) ` A ) u. ( ( cls ` J ) ` B ) ) )
Theorem	clsint2 32324*	The closure of an intersection is a subset of the intersection of the closures. (Contributed by Jeff Hankins, 31-Aug-2009.)
|- X = U. J   =>    |- ( ( J e. Top /\ C C_ ~P X ) -> ( ( cls ` J ) ` |^| C ) C_ |^|_ c e. C ( ( cls ` J ) ` c ) )
Theorem	opnregcld 32325*	A set is regularly closed iff it is the closure of some open set. (Contributed by Jeff Hankins, 27-Sep-2009.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X ) -> ( ( ( cls ` J ) ` ( ( int ` J ) ` A ) ) = A <-> E. o e. J A = ( ( cls ` J ) ` o ) ) )
Theorem	cldregopn 32326*	A set if regularly open iff it is the interior of some closed set. (Contributed by Jeff Hankins, 27-Sep-2009.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X ) -> ( ( ( int ` J ) ` ( ( cls ` J ) ` A ) ) = A <-> E. c e. ( Clsd ` J ) A = ( ( int ` J ) ` c ) ) )
Theorem	neiin 32327	Two neighborhoods intersect to form a neighborhood of the intersection. (Contributed by Jeff Hankins, 31-Aug-2009.)
|- ( ( J e. Top /\ M e. ( ( nei ` J ) ` A ) /\ N e. ( ( nei ` J ) ` B ) ) -> ( M i^i N ) e. ( ( nei ` J ) ` ( A i^i B ) ) )
Theorem	hmeoclda 32328	Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009.) (Revised by Mario Carneiro, 3-Jun-2014.)
|- ( ( ( J e. Top /\ K e. Top /\ F e. ( J Homeo K ) ) /\ S e. ( Clsd ` J ) ) -> ( F " S ) e. ( Clsd ` K ) )
Theorem	hmeocldb 32329	Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009.)
|- ( ( ( J e. Top /\ K e. Top /\ F e. ( J Homeo K ) ) /\ S e. ( Clsd ` K ) ) -> ( `' F " S ) e. ( Clsd ` J ) )
20.9.3  Topology of the real numbers
Theorem	ivthALT 32330*	An alternate proof of the Intermediate Value Theorem ivth 23223 using topology. (Contributed by Jeff Hankins, 17-Aug-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( ( A e. RR /\ B e. RR /\ U e. RR ) /\ A < B /\ ( ( A [,] B ) C_ D /\ D C_ CC /\ ( F e. ( D -cn-> CC ) /\ ( F " ( A [,] B ) ) C_ RR /\ U e. ( ( F ` A ) (,) ( F ` B ) ) ) ) ) -> E. x e. ( A (,) B ) ( F ` x ) = U )
20.9.4  Refinements
Syntax	cfne 32331	Extend class definition to include the "finer than" relation.
class Fne
Definition	df-fne 32332*	Define the fineness relation for covers. (Contributed by Jeff Hankins, 28-Sep-2009.)
|- Fne = { <. x , y >. | ( U. x = U. y /\ A. z e. x z C_ U. ( y i^i ~P z ) ) }
Theorem	fnerel 32333	Fineness is a relation. (Contributed by Jeff Hankins, 28-Sep-2009.)
|- Rel Fne
Theorem	isfne 32334*	The predicate " B is finer than A." 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.)
|- X = U. A   &    |- Y = U. B   =>    |- ( B e. C -> ( A Fne B <-> ( X = Y /\ A. x e. A x C_ U. ( B i^i ~P x ) ) ) )
Theorem	isfne4 32335	The predicate " B is finer than A " in terms of the topology generation function. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- X = U. A   &    |- Y = U. B   =>    |- ( A Fne B <-> ( X = Y /\ A C_ ( topGen ` B ) ) )
Theorem	isfne4b 32336	A condition for a topology to be finer than another. (Contributed by Jeff Hankins, 28-Sep-2009.) (Revised by Mario Carneiro, 11-Sep-2015.)
|- X = U. A   &    |- Y = U. B   =>    |- ( B e. V -> ( A Fne B <-> ( X = Y /\ ( topGen ` A ) C_ ( topGen ` B ) ) ) )
Theorem	isfne2 32337*	The predicate " B is finer than A." (Contributed by Jeff Hankins, 28-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
|- X = U. A   &    |- Y = U. B   =>    |- ( B e. C -> ( A Fne B <-> ( X = Y /\ A. x e. A A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) ) )
Theorem	isfne3 32338*	The predicate " B is finer than A." (Contributed by Jeff Hankins, 11-Oct-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
|- X = U. A   &    |- Y = U. B   =>    |- ( B e. C -> ( A Fne B <-> ( X = Y /\ A. x e. A E. y ( y C_ B /\ x = U. y ) ) ) )
Theorem	fnebas 32339	A finer cover covers the same set as the original. (Contributed by Jeff Hankins, 28-Sep-2009.)
|- X = U. A   &    |- Y = U. B   =>    |- ( A Fne B -> X = Y )
Theorem	fnetg 32340	A finer cover generates a topology finer than the original set. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( A Fne B -> A C_ ( topGen ` B ) )
Theorem	fnessex 32341*	If B is finer than A and S is an element of A, every point in S is an element of a subset of S which is in B. (Contributed by Jeff Hankins, 28-Sep-2009.)
|- ( ( A Fne B /\ S e. A /\ P e. S ) -> E. x e. B ( P e. x /\ x C_ S ) )
Theorem	fneuni 32342*	If B is finer than A, every element of A is a union of elements of B. (Contributed by Jeff Hankins, 11-Oct-2009.)
|- ( ( A Fne B /\ S e. A ) -> E. x ( x C_ B /\ S = U. x ) )
Theorem	fneint 32343*	If a cover is finer than another, every point can be approached more closely by intersections. (Contributed by Jeff Hankins, 11-Oct-2009.)
|- ( A Fne B -> |^| { x e. B | P e. x } C_ |^| { x e. A | P e. x } )
Theorem	fness 32344	A cover is finer than its subcovers. (Contributed by Jeff Hankins, 11-Oct-2009.)
|- X = U. A   &    |- Y = U. B   =>    |- ( ( B e. C /\ A C_ B /\ X = Y ) -> A Fne B )
Theorem	fneref 32345	Reflexivity of the fineness relation. (Contributed by Jeff Hankins, 12-Oct-2009.)
|- ( A e. V -> A Fne A )
Theorem	fnetr 32346	Transitivity of the fineness relation. (Contributed by Jeff Hankins, 5-Oct-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
|- ( ( A Fne B /\ B Fne C ) -> A Fne C )
Theorem	fneval 32347	Two covers are finer than each other iff they are both bases for the same topology. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- .~ = ( Fne i^i `' Fne )   =>    |- ( ( A e. V /\ B e. W ) -> ( A .~ B <-> ( topGen ` A ) = ( topGen ` B ) ) )
Theorem	fneer 32348	Fineness intersected with its converse is an equivalence relation. (Contributed by Jeff Hankins, 6-Oct-2009.) (Revised by Mario Carneiro, 11-Sep-2015.)
|- .~ = ( Fne i^i `' Fne )   =>    |- .~ Er _V
Theorem	topfne 32349	Fineness for covers corresponds precisely with fineness for topologies. (Contributed by Jeff Hankins, 29-Sep-2009.)
|- X = U. J   &    |- Y = U. K   =>    |- ( ( K e. Top /\ X = Y ) -> ( J C_ K <-> J Fne K ) )
Theorem	topfneec 32350	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 i^i `' Fne )   =>    |- ( J e. Top -> ( A e. [ J ] .~ <-> ( topGen ` A ) = J ) )
Theorem	topfneec2 32351	A topology is precisely identified with its equivalence class. (Contributed by Jeff Hankins, 12-Oct-2009.)
|- .~ = ( Fne i^i `' Fne )   =>    |- ( ( J e. Top /\ K e. Top ) -> ( [ J ] .~ = [ K ] .~ <-> J = K ) )
Theorem	fnessref 32352*	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.)
|- X = U. A   &    |- Y = U. B   =>    |- ( X = Y -> ( A Fne B <-> E. c ( c C_ B /\ ( A Fne c /\ c Ref A ) ) ) )
Theorem	refssfne 32353*	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.)
|- X = U. A   &    |- Y = U. B   =>    |- ( X = Y -> ( B Ref A <-> E. c ( B C_ c /\ ( A Fne c /\ c Ref A ) ) ) )
20.9.5  Neighborhood bases determine topologies
Theorem	neibastop1 32354*	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.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( ~P ~P X \ { (/) } ) )   &    |- ( ( ph /\ ( x e. X /\ v e. ( F ` x ) /\ w e. ( F ` x ) ) ) -> ( ( F ` x ) i^i ~P ( v i^i w ) ) =/= (/) )   &    |- J = { o e. ~P X | A. x e. o ( ( F ` x ) i^i ~P o ) =/= (/) }   =>    |- ( ph -> J e. (TopOn ` X ) )
Theorem	neibastop2lem 32355*	Lemma for neibastop2 32356. (Contributed by Jeff Hankins, 12-Sep-2009.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( ~P ~P X \ { (/) } ) )   &    |- ( ( ph /\ ( x e. X /\ v e. ( F ` x ) /\ w e. ( F ` x ) ) ) -> ( ( F ` x ) i^i ~P ( v i^i w ) ) =/= (/) )   &    |- J = { o e. ~P X | A. x e. o ( ( F ` x ) i^i ~P o ) =/= (/) }   &    |- ( ( ph /\ ( x e. X /\ v e. ( F ` x ) ) ) -> x e. v )   &    |- ( ( ph /\ ( x e. X /\ v e. ( F ` x ) ) ) -> E. t e. ( F ` x ) A. y e. t ( ( F ` y ) i^i ~P v ) =/= (/) )   &    |- ( ph -> P e. X )   &    |- ( ph -> N C_ X )   &    |- ( ph -> U e. ( F ` P ) )   &    |- ( ph -> U C_ N )   &    |- G = ( rec ( ( a e. _V |-> U_ z e. a U_ x e. X ( ( F ` x ) i^i ~P z ) ) , { U } ) |` om )   &    |- S = { y e. X | E. f e. U. ran G ( ( F ` y ) i^i ~P f ) =/= (/) }   =>    |- ( ph -> E. u e. J ( P e. u /\ u C_ N ) )
Theorem	neibastop2 32356*	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.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( ~P ~P X \ { (/) } ) )   &    |- ( ( ph /\ ( x e. X /\ v e. ( F ` x ) /\ w e. ( F ` x ) ) ) -> ( ( F ` x ) i^i ~P ( v i^i w ) ) =/= (/) )   &    |- J = { o e. ~P X | A. x e. o ( ( F ` x ) i^i ~P o ) =/= (/) }   &    |- ( ( ph /\ ( x e. X /\ v e. ( F ` x ) ) ) -> x e. v )   &    |- ( ( ph /\ ( x e. X /\ v e. ( F ` x ) ) ) -> E. t e. ( F ` x ) A. y e. t ( ( F ` y ) i^i ~P v ) =/= (/) )   =>    |- ( ( ph /\ P e. X ) -> ( N e. ( ( nei ` J ) ` { P } ) <-> ( N C_ X /\ ( ( F ` P ) i^i ~P N ) =/= (/) ) ) )
Theorem	neibastop3 32357*	The topology generated by a neighborhood base is unique. (Contributed by Jeff Hankins, 16-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( ~P ~P X \ { (/) } ) )   &    |- ( ( ph /\ ( x e. X /\ v e. ( F ` x ) /\ w e. ( F ` x ) ) ) -> ( ( F ` x ) i^i ~P ( v i^i w ) ) =/= (/) )   &    |- J = { o e. ~P X | A. x e. o ( ( F ` x ) i^i ~P o ) =/= (/) }   &    |- ( ( ph /\ ( x e. X /\ v e. ( F ` x ) ) ) -> x e. v )   &    |- ( ( ph /\ ( x e. X /\ v e. ( F ` x ) ) ) -> E. t e. ( F ` x ) A. y e. t ( ( F ` y ) i^i ~P v ) =/= (/) )   =>    |- ( ph -> E! j e. (TopOn ` X ) A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } )
20.9.6  Lattice structure of topologies
Theorem	topmtcl 32358	The meet of a collection of topologies on X is again a topology on X. (Contributed by Jeff Hankins, 5-Oct-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
|- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> ( ~P X i^i |^| S ) e. (TopOn ` X ) )
Theorem	topmeet 32359*	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.)
|- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> ( ~P X i^i |^| S ) = U. { k e. (TopOn ` X ) | A. j e. S k C_ j } )
Theorem	topjoin 32360*	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.)
|- ( ( X e. V /\ S C_ (TopOn ` X ) ) -> ( topGen ` ( fi ` ( { X } u. U. S ) ) ) = |^| { k e. (TopOn ` X ) | A. j e. S j C_ k } )
Theorem	fnemeet1 32361*	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.)
|- ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) Fne A )
Theorem	fnemeet2 32362*	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.)
|- ( ( X e. V /\ A. y e. S X = U. y ) -> ( T Fne ( ~P X i^i |^|_ t e. S ( topGen ` t ) ) <-> ( X = U. T /\ A. x e. S T Fne x ) ) )
Theorem	fnejoin1 32363*	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.)
|- ( ( X e. V /\ A. y e. S X = U. y /\ A e. S ) -> A Fne if ( S = (/) , { X } , U. S ) )
Theorem	fnejoin2 32364*	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.)
|- ( ( X e. V /\ A. y e. S X = U. y ) -> ( if ( S = (/) , { X } , U. S ) Fne T <-> ( X = U. T /\ A. x e. S x Fne T ) ) )
20.9.7  Filter bases
Theorem	fgmin 32365	Minimality property of a generated filter: every filter that contains B contains its generated filter. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Mario Carneiro, 7-Aug-2015.)
|- ( ( B e. ( fBas ` X ) /\ F e. ( Fil ` X ) ) -> ( B C_ F <-> ( X filGen B ) C_ F ) )
Theorem	neifg 32366*	The neighborhood filter of a nonempty set is generated by its open supersets. See comments for opnfbas 21646. (Contributed by Jeff Hankins, 3-Sep-2009.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( X filGen { x e. J | S C_ x } ) = ( ( nei ` J ) ` S ) )
20.9.8  Directed sets, nets
Theorem	tailfval 32367*	The tail function for a directed set. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 24-Nov-2013.)
|- X = dom D   =>    |- ( D e. DirRel -> ( tail ` D ) = ( x e. X |-> ( D " { x } ) ) )
Theorem	tailval 32368	The tail of an element in a directed set. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 24-Nov-2013.)
|- X = dom D   =>    |- ( ( D e. DirRel /\ A e. X ) -> ( ( tail ` D ) ` A ) = ( D " { A } ) )
Theorem	eltail 32369	An element of a tail. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 24-Nov-2013.)
|- X = dom D   =>    |- ( ( D e. DirRel /\ A e. X /\ B e. C ) -> ( B e. ( ( tail ` D ) ` A ) <-> A D B ) )
Theorem	tailf 32370	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.)
|- X = dom D   =>    |- ( D e. DirRel -> ( tail ` D ) : X --> ~P X )
Theorem	tailini 32371	A tail contains its initial element. (Contributed by Jeff Hankins, 25-Nov-2009.)
|- X = dom D   =>    |- ( ( D e. DirRel /\ A e. X ) -> A e. ( ( tail ` D ) ` A ) )
Theorem	tailfb 32372	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.)
|- X = dom D   =>    |- ( ( D e. DirRel /\ X =/= (/) ) -> ran ( tail ` D ) e. ( fBas ` X ) )
Theorem	filnetlem1 32373*	Lemma for filnet 32377. Change variables. (Contributed by Jeff Hankins, 13-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.)
|- H = U_ n e. F ( { n } X. n )   &    |- D = { <. x , y >. | ( ( x e. H /\ y e. H ) /\ ( 1st ` y ) C_ ( 1st ` x ) ) }   &    |- A e. _V   &    |- B e. _V   =>    |- ( A D B <-> ( ( A e. H /\ B e. H ) /\ ( 1st ` B ) C_ ( 1st ` A ) ) )
Theorem	filnetlem2 32374*	Lemma for filnet 32377. The field of the direction. (Contributed by Jeff Hankins, 13-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.)
|- H = U_ n e. F ( { n } X. n )   &    |- D = { <. x , y >. | ( ( x e. H /\ y e. H ) /\ ( 1st ` y ) C_ ( 1st ` x ) ) }   =>    |- ( ( _I |` H ) C_ D /\ D C_ ( H X. H ) )
Theorem	filnetlem3 32375*	Lemma for filnet 32377. (Contributed by Jeff Hankins, 13-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.)
|- H = U_ n e. F ( { n } X. n )   &    |- D = { <. x , y >. | ( ( x e. H /\ y e. H ) /\ ( 1st ` y ) C_ ( 1st ` x ) ) }   =>    |- ( H = U. U. D /\ ( F e. ( Fil ` X ) -> ( H C_ ( F X. X ) /\ D e. DirRel ) ) )
Theorem	filnetlem4 32376*	Lemma for filnet 32377. (Contributed by Jeff Hankins, 15-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.)
|- H = U_ n e. F ( { n } X. n )   &    |- D = { <. x , y >. | ( ( x e. H /\ y e. H ) /\ ( 1st ` y ) C_ ( 1st ` x ) ) }   =>    |- ( F e. ( Fil ` X ) -> E. d e. DirRel E. f ( f : dom d --> X /\ F = ( ( X FilMap f ) ` ran ( tail ` d ) ) ) )
Theorem	filnet 32377*	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.)
|- ( F e. ( Fil ` X ) -> E. d e. DirRel E. f ( f : dom d --> X /\ F = ( ( X FilMap f ) ` ran ( tail ` d ) ) ) )
20.10  Mathbox for Anthony Hart
20.10.1  Propositional Calculus
Theorem	tb-ax1 32378	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.)
|- ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) )
Theorem	tb-ax2 32379	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.)
|- ( ph -> ( ps -> ph ) )
Theorem	tb-ax3 32380	The third of three axioms in the Tarski-Bernays axiom system. This axiom, along with ax-mp 5, tb-ax1 32378, and tb-ax2 32379, 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.)
|- ( ( ( ph -> ps ) -> ph ) -> ph )
Theorem	tbsyl 32381	The weak syllogism from Tarski-Bernays'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ps )   &    |- ( ps -> ch )   =>    |- ( ph -> ch )
Theorem	re1ax2lem 32382	Lemma for re1ax2 32383. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( ph -> ( ps -> ch ) ) -> ( ps -> ( ph -> ch ) ) )
Theorem	re1ax2 32383	ax-2 7 rederived from the Tarski-Bernays axiom system. Often tb-ax1 32378 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.)
|- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) )
Theorem	naim1 32384	Constructor theorem for -/\. (Contributed by Anthony Hart, 1-Sep-2011.)
|- ( ( ph -> ps ) -> ( ( ps -/\ ch ) -> ( ph -/\ ch ) ) )
Theorem	naim2 32385	Constructor theorem for -/\. (Contributed by Anthony Hart, 1-Sep-2011.)
|- ( ( ph -> ps ) -> ( ( ch -/\ ps ) -> ( ch -/\ ph ) ) )
Theorem	naim1i 32386	Constructor rule for -/\. (Contributed by Anthony Hart, 2-Sep-2011.)
|- ( ph -> ps )   &    |- ( ps -/\ ch )   =>    |- ( ph -/\ ch )
Theorem	naim2i 32387	Constructor rule for -/\. (Contributed by Anthony Hart, 2-Sep-2011.)
|- ( ph -> ps )   &    |- ( ch -/\ ps )   =>    |- ( ch -/\ ph )
Theorem	naim12i 32388	Constructor rule for -/\. (Contributed by Anthony Hart, 2-Sep-2011.)
|- ( ph -> ps )   &    |- ( ch -> th )   &    |- ( ps -/\ th )   =>    |- ( ph -/\ ch )
Theorem	nabi1 32389	Constructor theorem for -/\. (Contributed by Anthony Hart, 1-Sep-2011.)
|- ( ( ph <-> ps ) -> ( ( ph -/\ ch ) <-> ( ps -/\ ch ) ) )
Theorem	nabi2 32390	Constructor theorem for -/\. (Contributed by Anthony Hart, 1-Sep-2011.)
|- ( ( ph <-> ps ) -> ( ( ch -/\ ph ) <-> ( ch -/\ ps ) ) )
Theorem	nabi1i 32391	Constructor rule for -/\. (Contributed by Anthony Hart, 2-Sep-2011.)
|- ( ph <-> ps )   &    |- ( ps -/\ ch )   =>    |- ( ph -/\ ch )
Theorem	nabi2i 32392	Constructor rule for -/\. (Contributed by Anthony Hart, 2-Sep-2011.)
|- ( ph <-> ps )   &    |- ( ch -/\ ps )   =>    |- ( ch -/\ ph )
Theorem	nabi12i 32393	Constructor rule for -/\. (Contributed by Anthony Hart, 2-Sep-2011.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   &    |- ( ps -/\ th )   =>    |- ( ph -/\ ch )
Syntax	w3nand 32394	The double nand.
wff ( ph -/\ ps -/\ ch )
Definition	df-3nand 32395	The double nand. This definition allows us to express the input of three variables only being false if all three are true. (Contributed by Anthony Hart, 2-Sep-2011.)
|- ( ( ph -/\ ps -/\ ch ) <-> ( ph -> ( ps -> -. ch ) ) )
Theorem	df3nandALT1 32396	The double nand expressed in terms of pure nand. (Contributed by Anthony Hart, 2-Sep-2011.)
|- ( ( ph -/\ ps -/\ ch ) <-> ( ph -/\ ( ( ps -/\ ch ) -/\ ( ps -/\ ch ) ) ) )
Theorem	df3nandALT2 32397	The double nand expressed in terms of negation and and not. (Contributed by Anthony Hart, 13-Sep-2011.)
|- ( ( ph -/\ ps -/\ ch ) <-> -. ( ph /\ ps /\ ch ) )
Theorem	andnand1 32398	Double and in terms of double nand. (Contributed by Anthony Hart, 2-Sep-2011.)
|- ( ( ph /\ ps /\ ch ) <-> ( ( ph -/\ ps -/\ ch ) -/\ ( ph -/\ ps -/\ ch ) ) )
Theorem	imnand2 32399	An -> nand relation. (Contributed by Anthony Hart, 2-Sep-2011.)
|- ( ( -. ph -> ps ) <-> ( ( ph -/\ ph ) -/\ ( ps -/\ ps ) ) )
20.10.2  Predicate Calculus
Theorem	allt 32400	For all sets, T. is true. (Contributed by Anthony Hart, 13-Sep-2011.)
|- A. x T.