P. 144 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14301-14400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fczpsrbag 14301*	The constant function equal to zero is a finite bag. (Contributed by AV, 8-Jul-2019.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( I e. V -> ( x e. I |-> 0 ) e. D )
Theorem	psrbaglesuppg 14302*	The support of a dominated bag is smaller than the dominating bag. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( `' G " NN ) C_ ( `' F " NN ) )
Theorem	psrbasg 14303*	The base set of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) (Proof shortened by AV, 8-Jul-2019.)
|- S = ( I mPwSer R )   &    |- K = ( Base ` R )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- B = ( Base ` S )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. W )   =>    |- ( ph -> B = ( K ^m D ) )
Theorem	psrelbas 14304*	An element of the set of power series is a function on the coefficients. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- S = ( I mPwSer R )   &    |- K = ( Base ` R )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- B = ( Base ` S )   &    |- ( ph -> X e. B )   =>    |- ( ph -> X : D --> K )
Theorem	psrelbasfun 14305	An element of the set of power series is a function. (Contributed by AV, 17-Jul-2019.)
|- S = ( I mPwSer R )   &    |- B = ( Base ` S )   =>    |- ( X e. B -> Fun X )
Theorem	psrplusgg 14306	The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .+ = ( +g ` R )   &    |- .+b = ( +g ` S )   =>    |- ( ( I e. V /\ R e. W ) -> .+b = ( oF .+ |` ( B X. B ) ) )
Theorem	psradd 14307	The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .+ = ( +g ` R )   &    |- .+b = ( +g ` S )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .+b Y ) = ( X oF .+ Y ) )
Theorem	psraddcl 14308	Closure of the power series addition operation. (Contributed by Mario Carneiro, 28-Dec-2014.) Generalize to magmas. (Revised by SN, 12-Apr-2025.)
|- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .+ = ( +g ` S )   &    |- ( ph -> R e. Mgm )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .+ Y ) e. B )
Theorem	psr0cl 14309*	The zero element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Grp )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- .0. = ( 0g ` R )   &    |- B = ( Base ` S )   =>    |- ( ph -> ( D X. { .0. } ) e. B )
Theorem	psr0lid 14310*	The zero element of the ring of power series is a left identity. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Grp )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- .0. = ( 0g ` R )   &    |- B = ( Base ` S )   &    |- .+ = ( +g ` S )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( ( D X. { .0. } ) .+ X ) = X )
Theorem	psrnegcl 14311*	The negative function in the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Grp )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- N = ( invg ` R )   &    |- B = ( Base ` S )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( N o. X ) e. B )
Theorem	psrlinv 14312*	The negative function in the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Grp )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- N = ( invg ` R )   &    |- B = ( Base ` S )   &    |- ( ph -> X e. B )   &    |- .0. = ( 0g ` R )   &    |- .+ = ( +g ` S )   =>    |- ( ph -> ( ( N o. X ) .+ X ) = ( D X. { .0. } ) )
Theorem	psrgrp 14313	The ring of power series is a group. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof shortened by SN, 7-Feb-2025.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Grp )   =>    |- ( ph -> S e. Grp )
Theorem	psr0 14314*	The zero element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Grp )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- O = ( 0g ` R )   &    |- .0. = ( 0g ` S )   =>    |- ( ph -> .0. = ( D X. { O } ) )
Theorem	psrneg 14315*	The negative function of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Grp )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- N = ( invg ` R )   &    |- B = ( Base ` S )   &    |- M = ( invg ` S )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( M ` X ) = ( N o. X ) )
Theorem	psr1clfi 14316*	The identity element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Ring )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- U = ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) )   &    |- B = ( Base ` S )   =>    |- ( ph -> U e. B )
PART 9  BASIC TOPOLOGY
9.1  Topology
9.1.1  Topological spaces A topology on a set is a set of subsets of that set, called open sets, which satisfy certain conditions. One condition is that the whole set be an open set. Therefore, a set is recoverable from a topology on it (as its union), and it may sometimes be more convenient to consider topologies without reference to the underlying set.
9.1.1.1  Topologies
Syntax	ctop 14317	Syntax for the class of topologies.
class Top
Definition	df-top 14318*	Define the class of topologies. It is a proper class. See istopg 14319 and istopfin 14320 for the corresponding characterizations, using respectively binary intersections like in this definition and nonempty finite intersections. The final form of the definition is due to Bourbaki (Def. 1 of [BourbakiTop1] p. I.1), while the idea of defining a topology in terms of its open sets is due to Aleksandrov. For the convoluted history of the definitions of these notions, see Gregory H. Moore, The emergence of open sets, closed sets, and limit points in analysis and topology, Historia Mathematica 35 (2008) 220--241. (Contributed by NM, 3-Mar-2006.) (Revised by BJ, 20-Oct-2018.)
|- Top = { x | ( A. y e. ~P x U. y e. x /\ A. y e. x A. z e. x ( y i^i z ) e. x ) }
Theorem	istopg 14319*	Express the predicate " J is a topology". See istopfin 14320 for another characterization using nonempty finite intersections instead of binary intersections. Note: In the literature, a topology is often represented by a calligraphic letter T, which resembles the letter J. This confusion may have led to J being used by some authors (e.g., K. D. Joshi, Introduction to General Topology (1983), p. 114) and it is convenient for us since we later use T to represent linear transformations (operators). (Contributed by Stefan Allan, 3-Mar-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- ( J e. A -> ( J e. Top <-> ( A. x ( x C_ J -> U. x e. J ) /\ A. x e. J A. y e. J ( x i^i y ) e. J ) ) )
Theorem	istopfin 14320*	Express the predicate " J is a topology" using nonempty finite intersections instead of binary intersections as in istopg 14319. It is not clear we can prove the converse without adding additional conditions. (Contributed by NM, 19-Jul-2006.) (Revised by Jim Kingdon, 14-Jan-2023.)
|- ( J e. Top -> ( A. x ( x C_ J -> U. x e. J ) /\ A. x ( ( x C_ J /\ x =/= (/) /\ x e. Fin ) -> |^| x e. J ) ) )
Theorem	uniopn 14321	The union of a subset of a topology (that is, the union of any family of open sets of a topology) is an open set. (Contributed by Stefan Allan, 27-Feb-2006.)
|- ( ( J e. Top /\ A C_ J ) -> U. A e. J )
Theorem	iunopn 14322*	The indexed union of a subset of a topology is an open set. (Contributed by NM, 5-Oct-2006.)
|- ( ( J e. Top /\ A. x e. A B e. J ) -> U_ x e. A B e. J )
Theorem	inopn 14323	The intersection of two open sets of a topology is an open set. (Contributed by NM, 17-Jul-2006.)
|- ( ( J e. Top /\ A e. J /\ B e. J ) -> ( A i^i B ) e. J )
Theorem	fiinopn 14324	The intersection of a nonempty finite family of open sets is open. (Contributed by FL, 20-Apr-2012.)
|- ( J e. Top -> ( ( A C_ J /\ A =/= (/) /\ A e. Fin ) -> |^| A e. J ) )
Theorem	unopn 14325	The union of two open sets is open. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( J e. Top /\ A e. J /\ B e. J ) -> ( A u. B ) e. J )
Theorem	0opn 14326	The empty set is an open subset of any topology. (Contributed by Stefan Allan, 27-Feb-2006.)
|- ( J e. Top -> (/) e. J )
Theorem	0ntop 14327	The empty set is not a topology. (Contributed by FL, 1-Jun-2008.)
|- -. (/) e. Top
Theorem	topopn 14328	The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006.)
|- X = U. J   =>    |- ( J e. Top -> X e. J )
Theorem	eltopss 14329	A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006.)
|- X = U. J   =>    |- ( ( J e. Top /\ A e. J ) -> A C_ X )
9.1.1.2  Topologies on sets
Syntax	ctopon 14330	Syntax for the function of topologies on sets.
class TopOn
Definition	df-topon 14331*	Define the function that associates with a set the set of topologies on it. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )
Theorem	funtopon 14332	The class TopOn is a function. (Contributed by BJ, 29-Apr-2021.)
|- Fun TopOn
Theorem	istopon 14333	Property of being a topology with a given base set. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by Mario Carneiro, 13-Aug-2015.)
|- ( J e. (TopOn ` B ) <-> ( J e. Top /\ B = U. J ) )
Theorem	topontop 14334	A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( J e. (TopOn ` B ) -> J e. Top )
Theorem	toponuni 14335	The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( J e. (TopOn ` B ) -> B = U. J )
Theorem	topontopi 14336	A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- J e. (TopOn ` B )   =>    |- J e. Top
Theorem	toponunii 14337	The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- J e. (TopOn ` B )   =>    |- B = U. J
Theorem	toptopon 14338	Alternative definition of Top in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- X = U. J   =>    |- ( J e. Top <-> J e. (TopOn ` X ) )
Theorem	toptopon2 14339	A topology is the same thing as a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.)
|- ( J e. Top <-> J e. (TopOn ` U. J ) )
Theorem	topontopon 14340	A topology on a set is a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.)
|- ( J e. (TopOn ` X ) -> J e. (TopOn ` U. J ) )
Theorem	toponrestid 14341	Given a topology on a set, restricting it to that same set has no effect. (Contributed by Jim Kingdon, 6-Jul-2022.)
|- A e. (TopOn ` B )   =>    |- A = ( A ↾t B )
Theorem	toponsspwpwg 14342	The set of topologies on a set is included in the double power set of that set. (Contributed by BJ, 29-Apr-2021.) (Revised by Jim Kingdon, 16-Jan-2023.)
|- ( A e. V -> (TopOn ` A ) C_ ~P ~P A )
Theorem	dmtopon 14343	The domain of TopOn is _V. (Contributed by BJ, 29-Apr-2021.)
|- dom TopOn = _V
Theorem	fntopon 14344	The class TopOn is a function with domain _V. (Contributed by BJ, 29-Apr-2021.)
|- TopOn Fn _V
Theorem	toponmax 14345	The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( J e. (TopOn ` B ) -> B e. J )
Theorem	toponss 14346	A member of a topology is a subset of its underlying set. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ A e. J ) -> A C_ X )
Theorem	toponcom 14347	If K is a topology on the base set of topology J, then J is a topology on the base of K. (Contributed by Mario Carneiro, 22-Aug-2015.)
|- ( ( J e. Top /\ K e. (TopOn ` U. J ) ) -> J e. (TopOn ` U. K ) )
Theorem	toponcomb 14348	Biconditional form of toponcom 14347. (Contributed by BJ, 5-Dec-2021.)
|- ( ( J e. Top /\ K e. Top ) -> ( J e. (TopOn ` U. K ) <-> K e. (TopOn ` U. J ) ) )
Theorem	topgele 14349	The topologies over the same set have the greatest element (the discrete topology) and the least element (the indiscrete topology). (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 16-Sep-2015.)
|- ( J e. (TopOn ` X ) -> ( { (/) , X } C_ J /\ J C_ ~P X ) )
9.1.1.3  Topological spaces
Syntax	ctps 14350	Syntax for the class of topological spaces.
class TopSp
Definition	df-topsp 14351	Define the class of topological spaces (as extensible structures). (Contributed by Stefan O'Rear, 13-Aug-2015.)
|- TopSp = { f | ( TopOpen ` f ) e. (TopOn ` ( Base ` f ) ) }
Theorem	istps 14352	Express the predicate "is a topological space". (Contributed by Mario Carneiro, 13-Aug-2015.)
|- A = ( Base ` K )   &    |- J = ( TopOpen ` K )   =>    |- ( K e. TopSp <-> J e. (TopOn ` A ) )
Theorem	istps2 14353	Express the predicate "is a topological space". (Contributed by NM, 20-Oct-2012.)
|- A = ( Base ` K )   &    |- J = ( TopOpen ` K )   =>    |- ( K e. TopSp <-> ( J e. Top /\ A = U. J ) )
Theorem	tpsuni 14354	The base set of a topological space. (Contributed by FL, 27-Jun-2014.)
|- A = ( Base ` K )   &    |- J = ( TopOpen ` K )   =>    |- ( K e. TopSp -> A = U. J )
Theorem	tpstop 14355	The topology extractor on a topological space is a topology. (Contributed by FL, 27-Jun-2014.)
|- J = ( TopOpen ` K )   =>    |- ( K e. TopSp -> J e. Top )
Theorem	tpspropd 14356	A topological space depends only on the base and topology components. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 13-Aug-2015.)
|- ( ph -> ( Base ` K ) = ( Base ` L ) )   &    |- ( ph -> ( TopOpen ` K ) = ( TopOpen ` L ) )   =>    |- ( ph -> ( K e. TopSp <-> L e. TopSp ) )
Theorem	topontopn 14357	Express the predicate "is a topological space". (Contributed by Mario Carneiro, 13-Aug-2015.)
|- A = ( Base ` K )   &    |- J = (TopSet ` K )   =>    |- ( J e. (TopOn ` A ) -> J = ( TopOpen ` K ) )
Theorem	tsettps 14358	If the topology component is already correctly truncated, then it forms a topological space (with the topology extractor function coming out the same as the component). (Contributed by Mario Carneiro, 13-Aug-2015.)
|- A = ( Base ` K )   &    |- J = (TopSet ` K )   =>    |- ( J e. (TopOn ` A ) -> K e. TopSp )
Theorem	istpsi 14359	Properties that determine a topological space. (Contributed by NM, 20-Oct-2012.)
|- ( Base ` K ) = A   &    |- ( TopOpen ` K ) = J   &    |- A = U. J   &    |- J e. Top   =>    |- K e. TopSp
Theorem	eltpsg 14360	Properties that determine a topological space from a construction (using no explicit indices). (Contributed by Mario Carneiro, 13-Aug-2015.)
|- K = { <. ( Base ` ndx ) , A >. , <. (TopSet ` ndx ) , J >. }   =>    |- ( J e. (TopOn ` A ) -> K e. TopSp )
Theorem	eltpsi 14361	Properties that determine a topological space from a construction (using no explicit indices). (Contributed by NM, 20-Oct-2012.) (Revised by Mario Carneiro, 13-Aug-2015.)
|- K = { <. ( Base ` ndx ) , A >. , <. (TopSet ` ndx ) , J >. }   &    |- A = U. J   &    |- J e. Top   =>    |- K e. TopSp
9.1.2  Topological bases
Syntax	ctb 14362	Syntax for the class of topological bases.
class TopBases
Definition	df-bases 14363*	Define the class of topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 14365). Note that "bases" is the plural of "basis". (Contributed by NM, 17-Jul-2006.)
|- TopBases = { x | A. y e. x A. z e. x ( y i^i z ) C_ U. ( x i^i ~P ( y i^i z ) ) }
Theorem	isbasisg 14364*	Express the predicate "the set B is a basis for a topology". (Contributed by NM, 17-Jul-2006.)
|- ( B e. C -> ( B e. TopBases <-> A. x e. B A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) ) )
Theorem	isbasis2g 14365*	Express the predicate "the set B is a basis for a topology". (Contributed by NM, 17-Jul-2006.)
|- ( B e. C -> ( B e. TopBases <-> A. x e. B A. y e. B A. z e. ( x i^i y ) E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) ) )
Theorem	isbasis3g 14366*	Express the predicate "the set B is a basis for a topology". Definition of basis in [Munkres] p. 78. (Contributed by NM, 17-Jul-2006.)
|- ( B e. C -> ( B e. TopBases <-> ( A. x e. B x C_ U. B /\ A. x e. U. B E. y e. B x e. y /\ A. x e. B A. y e. B A. z e. ( x i^i y ) E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) ) ) )
Theorem	basis1 14367	Property of a basis. (Contributed by NM, 16-Jul-2006.)
|- ( ( B e. TopBases /\ C e. B /\ D e. B ) -> ( C i^i D ) C_ U. ( B i^i ~P ( C i^i D ) ) )
Theorem	basis2 14368*	Property of a basis. (Contributed by NM, 17-Jul-2006.)
|- ( ( ( B e. TopBases /\ C e. B ) /\ ( D e. B /\ A e. ( C i^i D ) ) ) -> E. x e. B ( A e. x /\ x C_ ( C i^i D ) ) )
Theorem	fiinbas 14369*	If a set is closed under finite intersection, then it is a basis for a topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( B e. C /\ A. x e. B A. y e. B ( x i^i y ) e. B ) -> B e. TopBases )
Theorem	baspartn 14370*	A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( ( P e. V /\ A. x e. P A. y e. P ( x = y \/ ( x i^i y ) = (/) ) ) -> P e. TopBases )
Theorem	tgval2 14371*	Definition of a topology generated by a basis in [Munkres] p. 78. Later we show (in tgcl 14384) that ( topGen ` B ) is indeed a topology (on U. B, see unitg 14382). See also tgval 12964 and tgval3 14378. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
|- ( B e. V -> ( topGen ` B ) = { x | ( x C_ U. B /\ A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) } )
Theorem	eltg 14372	Membership in a topology generated by a basis. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
|- ( B e. V -> ( A e. ( topGen ` B ) <-> A C_ U. ( B i^i ~P A ) ) )
Theorem	eltg2 14373*	Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
|- ( B e. V -> ( A e. ( topGen ` B ) <-> ( A C_ U. B /\ A. x e. A E. y e. B ( x e. y /\ y C_ A ) ) ) )
Theorem	eltg2b 14374*	Membership in a topology generated by a basis. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Mario Carneiro, 10-Jan-2015.)
|- ( B e. V -> ( A e. ( topGen ` B ) <-> A. x e. A E. y e. B ( x e. y /\ y C_ A ) ) )
Theorem	eltg4i 14375	An open set in a topology generated by a basis is the union of all basic open sets contained in it. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( A e. ( topGen ` B ) -> A = U. ( B i^i ~P A ) )
Theorem	eltg3i 14376	The union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 30-Aug-2015.)
|- ( ( B e. V /\ A C_ B ) -> U. A e. ( topGen ` B ) )
Theorem	eltg3 14377*	Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Jim Kingdon, 4-Mar-2023.)
|- ( B e. V -> ( A e. ( topGen ` B ) <-> E. x ( x C_ B /\ A = U. x ) ) )
Theorem	tgval3 14378*	Alternate expression for the topology generated by a basis. Lemma 2.1 of [Munkres] p. 80. See also tgval 12964 and tgval2 14371. (Contributed by NM, 17-Jul-2006.) (Revised by Mario Carneiro, 30-Aug-2015.)
|- ( B e. V -> ( topGen ` B ) = { x | E. y ( y C_ B /\ x = U. y ) } )
Theorem	tg1 14379	Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.)
|- ( A e. ( topGen ` B ) -> A C_ U. B )
Theorem	tg2 14380*	Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.)
|- ( ( A e. ( topGen ` B ) /\ C e. A ) -> E. x e. B ( C e. x /\ x C_ A ) )
Theorem	bastg 14381	A member of a basis is a subset of the topology it generates. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
|- ( B e. V -> B C_ ( topGen ` B ) )
Theorem	unitg 14382	The topology generated by a basis B is a topology on U. B. Importantly, this theorem means that we don't have to specify separately the base set for the topological space generated by a basis. In other words, any member of the class TopBases completely specifies the basis it corresponds to. (Contributed by NM, 16-Jul-2006.) (Proof shortened by OpenAI, 30-Mar-2020.)
|- ( B e. V -> U. ( topGen ` B ) = U. B )
Theorem	tgss 14383	Subset relation for generated topologies. (Contributed by NM, 7-May-2007.)
|- ( ( C e. V /\ B C_ C ) -> ( topGen ` B ) C_ ( topGen ` C ) )
Theorem	tgcl 14384	Show that a basis generates a topology. Remark in [Munkres] p. 79. (Contributed by NM, 17-Jul-2006.)
|- ( B e. TopBases -> ( topGen ` B ) e. Top )
Theorem	tgclb 14385	The property tgcl 14384 can be reversed: if the topology generated by B is actually a topology, then B must be a topological basis. This yields an alternative definition of TopBases. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- ( B e. TopBases <-> ( topGen ` B ) e. Top )
Theorem	tgtopon 14386	A basis generates a topology on U. B. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( B e. TopBases -> ( topGen ` B ) e. (TopOn ` U. B ) )
Theorem	topbas 14387	A topology is its own basis. (Contributed by NM, 17-Jul-2006.)
|- ( J e. Top -> J e. TopBases )
Theorem	tgtop 14388	A topology is its own basis. (Contributed by NM, 18-Jul-2006.)
|- ( J e. Top -> ( topGen ` J ) = J )
Theorem	eltop 14389	Membership in a topology, expressed without quantifiers. (Contributed by NM, 19-Jul-2006.)
|- ( J e. Top -> ( A e. J <-> A C_ U. ( J i^i ~P A ) ) )
Theorem	eltop2 14390*	Membership in a topology. (Contributed by NM, 19-Jul-2006.)
|- ( J e. Top -> ( A e. J <-> A. x e. A E. y e. J ( x e. y /\ y C_ A ) ) )
Theorem	eltop3 14391*	Membership in a topology. (Contributed by NM, 19-Jul-2006.)
|- ( J e. Top -> ( A e. J <-> E. x ( x C_ J /\ A = U. x ) ) )
Theorem	tgdom 14392	A space has no more open sets than subsets of a basis. (Contributed by Stefan O'Rear, 22-Feb-2015.) (Revised by Mario Carneiro, 9-Apr-2015.)
|- ( B e. V -> ( topGen ` B ) ~<_ ~P B )
Theorem	tgiun 14393*	The indexed union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- ( ( B e. V /\ A. x e. A C e. B ) -> U_ x e. A C e. ( topGen ` B ) )
Theorem	tgidm 14394	The topology generator function is idempotent. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.)
|- ( B e. V -> ( topGen ` ( topGen ` B ) ) = ( topGen ` B ) )
Theorem	bastop 14395	Two ways to express that a basis is a topology. (Contributed by NM, 18-Jul-2006.)
|- ( B e. TopBases -> ( B e. Top <-> ( topGen ` B ) = B ) )
Theorem	tgtop11 14396	The topology generation function is one-to-one when applied to completed topologies. (Contributed by NM, 18-Jul-2006.)
|- ( ( J e. Top /\ K e. Top /\ ( topGen ` J ) = ( topGen ` K ) ) -> J = K )
Theorem	en1top 14397	{ (/) } is the only topology with one element. (Contributed by FL, 18-Aug-2008.)
|- ( J e. Top -> ( J ~~ 1o <-> J = { (/) } ) )
Theorem	tgss3 14398	A criterion for determining whether one topology is finer than another. Lemma 2.2 of [Munkres] p. 80 using abbreviations. (Contributed by NM, 20-Jul-2006.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
|- ( ( B e. V /\ C e. W ) -> ( ( topGen ` B ) C_ ( topGen ` C ) <-> B C_ ( topGen ` C ) ) )
Theorem	tgss2 14399*	A criterion for determining whether one topology is finer than another, based on a comparison of their bases. Lemma 2.2 of [Munkres] p. 80. (Contributed by NM, 20-Jul-2006.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
|- ( ( B e. V /\ U. B = U. C ) -> ( ( topGen ` B ) C_ ( topGen ` C ) <-> A. x e. U. B A. y e. B ( x e. y -> E. z e. C ( x e. z /\ z C_ y ) ) ) )
Theorem	basgen 14400	Given a topology J, show that a subset B satisfying the third antecedent is a basis for it. Lemma 2.3 of [Munkres] p. 81 using abbreviations. (Contributed by NM, 22-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.)
|- ( ( J e. Top /\ B C_ J /\ J C_ ( topGen ` B ) ) -> ( topGen ` B ) = J )