P. 149 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14801-14900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tgss3 14801	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 14802*	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 14803	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 )
Theorem	basgen2 14804*	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. (Contributed by NM, 20-Jul-2006.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
|- ( ( J e. Top /\ B C_ J /\ A. x e. J A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) -> ( topGen ` B ) = J )
Theorem	2basgeng 14805	Conditions that determine the equality of two generated topologies. (Contributed by NM, 8-May-2007.) (Revised by Jim Kingdon, 5-Mar-2023.)
|- ( ( B e. V /\ B C_ C /\ C C_ ( topGen ` B ) ) -> ( topGen ` B ) = ( topGen ` C ) )
Theorem	bastop1 14806*	A subset of a topology is a basis for the topology iff every member of the topology is a union of members of the basis. We use the idiom " ( topGen ` B ) = J " to express " B is a basis for topology J " since we do not have a separate notation for this. Definition 15.35 of [Schechter] p. 428. (Contributed by NM, 2-Feb-2008.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
|- ( ( J e. Top /\ B C_ J ) -> ( ( topGen ` B ) = J <-> A. x e. J E. y ( y C_ B /\ x = U. y ) ) )
Theorem	bastop2 14807*	A version of bastop1 14806 that doesn't have B C_ J in the antecedent. (Contributed by NM, 3-Feb-2008.)
|- ( J e. Top -> ( ( topGen ` B ) = J <-> ( B C_ J /\ A. x e. J E. y ( y C_ B /\ x = U. y ) ) ) )
9.1.3  Examples of topologies
Theorem	distop 14808	The discrete topology on a set A. Part of Example 2 in [Munkres] p. 77. (Contributed by FL, 17-Jul-2006.) (Revised by Mario Carneiro, 19-Mar-2015.)
|- ( A e. V -> ~P A e. Top )
Theorem	topnex 14809	The class of all topologies is a proper class. The proof uses discrete topologies and pwnex 4546. (Contributed by BJ, 2-May-2021.)
|- Top e/ _V
Theorem	distopon 14810	The discrete topology on a set A, with base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( A e. V -> ~P A e. (TopOn ` A ) )
Theorem	sn0topon 14811	The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- { (/) } e. (TopOn ` (/) )
Theorem	sn0top 14812	The singleton of the empty set is a topology. (Contributed by Stefan Allan, 3-Mar-2006.) (Proof shortened by Mario Carneiro, 13-Aug-2015.)
|- { (/) } e. Top
Theorem	epttop 14813*	The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- ( ( A e. V /\ P e. A ) -> { x e. ~P A | ( P e. x -> x = A ) } e. (TopOn ` A ) )
Theorem	distps 14814	The discrete topology on a set A expressed as a topological space. (Contributed by FL, 20-Aug-2006.)
|- A e. _V   &    |- K = { <. ( Base ` ndx ) , A >. , <. (TopSet ` ndx ) , ~P A >. }   =>    |- K e. TopSp
9.1.4  Closure and interior
Syntax	ccld 14815	Extend class notation with the set of closed sets of a topology.
class Clsd
Syntax	cnt 14816	Extend class notation with interior of a subset of a topology base set.
class int
Syntax	ccl 14817	Extend class notation with closure of a subset of a topology base set.
class cls
Definition	df-cld 14818*	Define a function on topologies whose value is the set of closed sets of the topology. (Contributed by NM, 2-Oct-2006.)
|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
Definition	df-ntr 14819*	Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 14833. (Contributed by NM, 10-Sep-2006.)
|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
Definition	df-cls 14820*	Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 14834. (Contributed by NM, 3-Oct-2006.)
|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
Theorem	fncld 14821	The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- Clsd Fn Top
Theorem	cldval 14822*	The set of closed sets of a topology. (Note that the set of open sets is just the topology itself, so we don't have a separate definition.) (Contributed by NM, 2-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( J e. Top -> ( Clsd ` J ) = { x e. ~P X | ( X \ x ) e. J } )
Theorem	ntrfval 14823*	The interior function on the subsets of a topology's base set. (Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( J e. Top -> ( int ` J ) = ( x e. ~P X |-> U. ( J i^i ~P x ) ) )
Theorem	clsfval 14824*	The closure function on the subsets of a topology's base set. (Contributed by NM, 3-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( J e. Top -> ( cls ` J ) = ( x e. ~P X |-> |^| { y e. ( Clsd ` J ) | x C_ y } ) )
Theorem	cldrcl 14825	Reverse closure of the closed set operation. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( C e. ( Clsd ` J ) -> J e. Top )
Theorem	iscld 14826	The predicate "the class S is a closed set". (Contributed by NM, 2-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( J e. Top -> ( S e. ( Clsd ` J ) <-> ( S C_ X /\ ( X \ S ) e. J ) ) )
Theorem	iscld2 14827	A subset of the underlying set of a topology is closed iff its complement is open. (Contributed by NM, 4-Oct-2006.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( S e. ( Clsd ` J ) <-> ( X \ S ) e. J ) )
Theorem	cldss 14828	A closed set is a subset of the underlying set of a topology. (Contributed by NM, 5-Oct-2006.) (Revised by Stefan O'Rear, 22-Feb-2015.)
|- X = U. J   =>    |- ( S e. ( Clsd ` J ) -> S C_ X )
Theorem	cldss2 14829	The set of closed sets is contained in the powerset of the base. (Contributed by Mario Carneiro, 6-Jan-2014.)
|- X = U. J   =>    |- ( Clsd ` J ) C_ ~P X
Theorem	cldopn 14830	The complement of a closed set is open. (Contributed by NM, 5-Oct-2006.) (Revised by Stefan O'Rear, 22-Feb-2015.)
|- X = U. J   =>    |- ( S e. ( Clsd ` J ) -> ( X \ S ) e. J )
Theorem	difopn 14831	The difference of a closed set with an open set is open. (Contributed by Mario Carneiro, 6-Jan-2014.)
|- X = U. J   =>    |- ( ( A e. J /\ B e. ( Clsd ` J ) ) -> ( A \ B ) e. J )
Theorem	topcld 14832	The underlying set of a topology is closed. Part of Theorem 6.1(1) of [Munkres] p. 93. (Contributed by NM, 3-Oct-2006.)
|- X = U. J   =>    |- ( J e. Top -> X e. ( Clsd ` J ) )
Theorem	ntrval 14833	The interior of a subset of a topology's base set is the union of all the open sets it includes. Definition of interior of [Munkres] p. 94. (Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) = U. ( J i^i ~P S ) )
Theorem	clsval 14834*	The closure of a subset of a topology's base set is the intersection of all the closed sets that include it. Definition of closure of [Munkres] p. 94. (Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) = |^| { x e. ( Clsd ` J ) | S C_ x } )
Theorem	0cld 14835	The empty set is closed. Part of Theorem 6.1(1) of [Munkres] p. 93. (Contributed by NM, 4-Oct-2006.)
|- ( J e. Top -> (/) e. ( Clsd ` J ) )
Theorem	uncld 14836	The union of two closed sets is closed. Equivalent to Theorem 6.1(3) of [Munkres] p. 93. (Contributed by NM, 5-Oct-2006.)
|- ( ( A e. ( Clsd ` J ) /\ B e. ( Clsd ` J ) ) -> ( A u. B ) e. ( Clsd ` J ) )
Theorem	cldcls 14837	A closed subset equals its own closure. (Contributed by NM, 15-Mar-2007.)
|- ( S e. ( Clsd ` J ) -> ( ( cls ` J ) ` S ) = S )
Theorem	iuncld 14838*	A finite indexed union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.) (Revised by Jim Kingdon, 10-Mar-2023.)
|- X = U. J   =>    |- ( ( J e. Top /\ A e. Fin /\ A. x e. A B e. ( Clsd ` J ) ) -> U_ x e. A B e. ( Clsd ` J ) )
Theorem	unicld 14839	A finite union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ A e. Fin /\ A C_ ( Clsd ` J ) ) -> U. A e. ( Clsd ` J ) )
Theorem	ntropn 14840	The interior of a subset of a topology's underlying set is open. (Contributed by NM, 11-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) e. J )
Theorem	clsss 14841	Subset relationship for closure. (Contributed by NM, 10-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ T C_ S ) -> ( ( cls ` J ) ` T ) C_ ( ( cls ` J ) ` S ) )
Theorem	ntrss 14842	Subset relationship for interior. (Contributed by NM, 3-Oct-2007.) (Revised by Jim Kingdon, 11-Mar-2023.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ T C_ S ) -> ( ( int ` J ) ` T ) C_ ( ( int ` J ) ` S ) )
Theorem	sscls 14843	A subset of a topology's underlying set is included in its closure. (Contributed by NM, 22-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> S C_ ( ( cls ` J ) ` S ) )
Theorem	ntrss2 14844	A subset includes its interior. (Contributed by NM, 3-Oct-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) C_ S )
Theorem	ssntr 14845	An open subset of a set is a subset of the set's interior. (Contributed by Jeff Hankins, 31-Aug-2009.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( ( ( J e. Top /\ S C_ X ) /\ ( O e. J /\ O C_ S ) ) -> O C_ ( ( int ` J ) ` S ) )
Theorem	ntrss3 14846	The interior of a subset of a topological space is included in the space. (Contributed by NM, 1-Oct-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) C_ X )
Theorem	ntrin 14847	A pairwise intersection of interiors is the interior of the intersection. This does not always hold for arbitrary intersections. (Contributed by Jeff Hankins, 31-Aug-2009.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X /\ B C_ X ) -> ( ( int ` J ) ` ( A i^i B ) ) = ( ( ( int ` J ) ` A ) i^i ( ( int ` J ) ` B ) ) )
Theorem	isopn3 14848	A subset is open iff it equals its own interior. (Contributed by NM, 9-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( S e. J <-> ( ( int ` J ) ` S ) = S ) )
Theorem	ntridm 14849	The interior operation is idempotent. (Contributed by NM, 2-Oct-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` ( ( int ` J ) ` S ) ) = ( ( int ` J ) ` S ) )
Theorem	clstop 14850	The closure of a topology's underlying set is the entire set. (Contributed by NM, 5-Oct-2007.) (Proof shortened by Jim Kingdon, 11-Mar-2023.)
|- X = U. J   =>    |- ( J e. Top -> ( ( cls ` J ) ` X ) = X )
Theorem	ntrtop 14851	The interior of a topology's underlying set is the entire set. (Contributed by NM, 12-Sep-2006.)
|- X = U. J   =>    |- ( J e. Top -> ( ( int ` J ) ` X ) = X )
Theorem	clsss2 14852	If a subset is included in a closed set, so is the subset's closure. (Contributed by NM, 22-Feb-2007.)
|- X = U. J   =>    |- ( ( C e. ( Clsd ` J ) /\ S C_ C ) -> ( ( cls ` J ) ` S ) C_ C )
Theorem	clsss3 14853	The closure of a subset of a topological space is included in the space. (Contributed by NM, 26-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) C_ X )
Theorem	ntrcls0 14854	A subset whose closure has an empty interior also has an empty interior. (Contributed by NM, 4-Oct-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ ( ( int ` J ) ` ( ( cls ` J ) ` S ) ) = (/) ) -> ( ( int ` J ) ` S ) = (/) )
Theorem	ntreq0 14855*	Two ways to say that a subset has an empty interior. (Contributed by NM, 3-Oct-2007.) (Revised by Jim Kingdon, 11-Mar-2023.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( ( int ` J ) ` S ) = (/) <-> A. x e. J ( x C_ S -> x = (/) ) ) )
Theorem	cls0 14856	The closure of the empty set. (Contributed by NM, 2-Oct-2007.) (Proof shortened by Jim Kingdon, 12-Mar-2023.)
|- ( J e. Top -> ( ( cls ` J ) ` (/) ) = (/) )
Theorem	ntr0 14857	The interior of the empty set. (Contributed by NM, 2-Oct-2007.)
|- ( J e. Top -> ( ( int ` J ) ` (/) ) = (/) )
Theorem	isopn3i 14858	An open subset equals its own interior. (Contributed by Mario Carneiro, 30-Dec-2016.)
|- ( ( J e. Top /\ S e. J ) -> ( ( int ` J ) ` S ) = S )
Theorem	discld 14859	The open sets of a discrete topology are closed and its closed sets are open. (Contributed by FL, 7-Jun-2007.) (Revised by Mario Carneiro, 7-Apr-2015.)
|- ( A e. V -> ( Clsd ` ~P A ) = ~P A )
Theorem	sn0cld 14860	The closed sets of the topology { (/) }. (Contributed by FL, 5-Jan-2009.)
|- ( Clsd ` { (/) } ) = { (/) }
9.1.5  Neighborhoods
Syntax	cnei 14861	Extend class notation with neighborhood relation for topologies.
class nei
Definition	df-nei 14862*	Define a function on topologies whose value is a map from a subset to its neighborhoods. (Contributed by NM, 11-Feb-2007.)
|- nei = ( j e. Top |-> ( x e. ~P U. j |-> { y e. ~P U. j | E. g e. j ( x C_ g /\ g C_ y ) } ) )
Theorem	neifval 14863*	Value of the neighborhood function on the subsets of the base set of a topology. (Contributed by NM, 11-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( J e. Top -> ( nei ` J ) = ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) )
Theorem	neif 14864	The neighborhood function is a function from the set of the subsets of the base set of a topology. (Contributed by NM, 12-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( J e. Top -> ( nei ` J ) Fn ~P X )
Theorem	neiss2 14865	A set with a neighborhood is a subset of the base set of a topology. (This theorem depends on a function's value being empty outside of its domain, but it will make later theorems simpler to state.) (Contributed by NM, 12-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S C_ X )
Theorem	neival 14866*	Value of the set of neighborhoods of a subset of the base set of a topology. (Contributed by NM, 11-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( nei ` J ) ` S ) = { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } )
Theorem	isnei 14867*	The predicate "the class N is a neighborhood of S". (Contributed by FL, 25-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( N e. ( ( nei ` J ) ` S ) <-> ( N C_ X /\ E. g e. J ( S C_ g /\ g C_ N ) ) ) )
Theorem	neiint 14868	An intuitive definition of a neighborhood in terms of interior. (Contributed by Szymon Jaroszewicz, 18-Dec-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ N C_ X ) -> ( N e. ( ( nei ` J ) ` S ) <-> S C_ ( ( int ` J ) ` N ) ) )
Theorem	isneip 14869*	The predicate "the class N is a neighborhood of point P". (Contributed by NM, 26-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ P e. X ) -> ( N e. ( ( nei ` J ) ` { P } ) <-> ( N C_ X /\ E. g e. J ( P e. g /\ g C_ N ) ) ) )
Theorem	neii1 14870	A neighborhood is included in the topology's base set. (Contributed by NM, 12-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> N C_ X )
Theorem	neisspw 14871	The neighborhoods of any set are subsets of the base set. (Contributed by Stefan O'Rear, 6-Aug-2015.)
|- X = U. J   =>    |- ( J e. Top -> ( ( nei ` J ) ` S ) C_ ~P X )
Theorem	neii2 14872*	Property of a neighborhood. (Contributed by NM, 12-Feb-2007.)
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> E. g e. J ( S C_ g /\ g C_ N ) )
Theorem	neiss 14873	Any neighborhood of a set S is also a neighborhood of any subset R C_ S. Similar to Proposition 1 of [BourbakiTop1] p. I.2. (Contributed by FL, 25-Sep-2006.)
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> N e. ( ( nei ` J ) ` R ) )
Theorem	ssnei 14874	A set is included in any of its neighborhoods. Generalization to subsets of elnei 14875. (Contributed by FL, 16-Nov-2006.)
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S C_ N )
Theorem	elnei 14875	A point belongs to any of its neighborhoods. Property Viii of [BourbakiTop1] p. I.3. (Contributed by FL, 28-Sep-2006.)
|- ( ( J e. Top /\ P e. A /\ N e. ( ( nei ` J ) ` { P } ) ) -> P e. N )
Theorem	0nnei 14876	The empty set is not a neighborhood of a nonempty set. (Contributed by FL, 18-Sep-2007.)
|- ( ( J e. Top /\ S =/= (/) ) -> -. (/) e. ( ( nei ` J ) ` S ) )
Theorem	neipsm 14877*	A neighborhood of a set is a neighborhood of every point in the set. Proposition 1 of [BourbakiTop1] p. I.2. (Contributed by FL, 16-Nov-2006.) (Revised by Jim Kingdon, 22-Mar-2023.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ E. x x e. S ) -> ( N e. ( ( nei ` J ) ` S ) <-> A. p e. S N e. ( ( nei ` J ) ` { p } ) ) )
Theorem	opnneissb 14878	An open set is a neighborhood of any of its subsets. (Contributed by FL, 2-Oct-2006.)
|- X = U. J   =>    |- ( ( J e. Top /\ N e. J /\ S C_ X ) -> ( S C_ N <-> N e. ( ( nei ` J ) ` S ) ) )
Theorem	opnssneib 14879	Any superset of an open set is a neighborhood of it. (Contributed by NM, 14-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S e. J /\ N C_ X ) -> ( S C_ N <-> N e. ( ( nei ` J ) ` S ) ) )
Theorem	ssnei2 14880	Any subset M of X containing a neighborhood N of a set S is a neighborhood of this set. Generalization to subsets of Property Vi of [BourbakiTop1] p. I.3. (Contributed by FL, 2-Oct-2006.)
|- X = U. J   =>    |- ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( N C_ M /\ M C_ X ) ) -> M e. ( ( nei ` J ) ` S ) )
Theorem	opnneiss 14881	An open set is a neighborhood of any of its subsets. (Contributed by NM, 13-Feb-2007.)
|- ( ( J e. Top /\ N e. J /\ S C_ N ) -> N e. ( ( nei ` J ) ` S ) )
Theorem	opnneip 14882	An open set is a neighborhood of any of its members. (Contributed by NM, 8-Mar-2007.)
|- ( ( J e. Top /\ N e. J /\ P e. N ) -> N e. ( ( nei ` J ) ` { P } ) )
Theorem	tpnei 14883	The underlying set of a topology is a neighborhood of any of its subsets. Special case of opnneiss 14881. (Contributed by FL, 2-Oct-2006.)
|- X = U. J   =>    |- ( J e. Top -> ( S C_ X <-> X e. ( ( nei ` J ) ` S ) ) )
Theorem	neiuni 14884	The union of the neighborhoods of a set equals the topology's underlying set. (Contributed by FL, 18-Sep-2007.) (Revised by Mario Carneiro, 9-Apr-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> X = U. ( ( nei ` J ) ` S ) )
Theorem	topssnei 14885	A finer topology has more neighborhoods. (Contributed by Mario Carneiro, 9-Apr-2015.)
|- X = U. J   &    |- Y = U. K   =>    |- ( ( ( J e. Top /\ K e. Top /\ X = Y ) /\ J C_ K ) -> ( ( nei ` J ) ` S ) C_ ( ( nei ` K ) ` S ) )
Theorem	innei 14886	The intersection of two neighborhoods of a set is also a neighborhood of the set. Generalization to subsets of Property Vii of [BourbakiTop1] p. I.3 for binary intersections. (Contributed by FL, 28-Sep-2006.)
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ M e. ( ( nei ` J ) ` S ) ) -> ( N i^i M ) e. ( ( nei ` J ) ` S ) )
Theorem	opnneiid 14887	Only an open set is a neighborhood of itself. (Contributed by FL, 2-Oct-2006.)
|- ( J e. Top -> ( N e. ( ( nei ` J ) ` N ) <-> N e. J ) )
Theorem	neissex 14888*	For any neighborhood N of S, there is a neighborhood x of S such that N is a neighborhood of all subsets of x. Generalization to subsets of Property Viv of [BourbakiTop1] p. I.3. (Contributed by FL, 2-Oct-2006.)
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> E. x e. ( ( nei ` J ) ` S ) A. y ( y C_ x -> N e. ( ( nei ` J ) ` y ) ) )
Theorem	0nei 14889	The empty set is a neighborhood of itself. (Contributed by FL, 10-Dec-2006.)
|- ( J e. Top -> (/) e. ( ( nei ` J ) ` (/) ) )
9.1.6  Subspace topologies
Theorem	restrcl 14890	Reverse closure for the subspace topology. (Contributed by Mario Carneiro, 19-Mar-2015.) (Proof shortened by Jim Kingdon, 23-Mar-2023.)
|- ( ( J ↾t A ) e. Top -> ( J e. _V /\ A e. _V ) )
Theorem	restbasg 14891	A subspace topology basis is a basis. (Contributed by Mario Carneiro, 19-Mar-2015.)
|- ( ( B e. TopBases /\ A e. V ) -> ( B ↾t A ) e. TopBases )
Theorem	tgrest 14892	A subspace can be generated by restricted sets from a basis for the original topology. (Contributed by Mario Carneiro, 19-Mar-2015.) (Proof shortened by Mario Carneiro, 30-Aug-2015.)
|- ( ( B e. V /\ A e. W ) -> ( topGen ` ( B ↾t A ) ) = ( ( topGen ` B ) ↾t A ) )
Theorem	resttop 14893	A subspace topology is a topology. Definition of subspace topology in [Munkres] p. 89. A is normally a subset of the base set of J. (Contributed by FL, 15-Apr-2007.) (Revised by Mario Carneiro, 1-May-2015.)
|- ( ( J e. Top /\ A e. V ) -> ( J ↾t A ) e. Top )
Theorem	resttopon 14894	A subspace topology is a topology on the base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> ( J ↾t A ) e. (TopOn ` A ) )
Theorem	restuni 14895	The underlying set of a subspace topology. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 13-Aug-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X ) -> A = U. ( J ↾t A ) )
Theorem	stoig 14896	The topological space built with a subspace topology. (Contributed by FL, 5-Jan-2009.) (Proof shortened by Mario Carneiro, 1-May-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X ) -> { <. ( Base ` ndx ) , A >. , <. (TopSet ` ndx ) , ( J ↾t A ) >. } e. TopSp )
Theorem	restco 14897	Composition of subspaces. (Contributed by Mario Carneiro, 15-Dec-2013.) (Revised by Mario Carneiro, 1-May-2015.)
|- ( ( J e. V /\ A e. W /\ B e. X ) -> ( ( J ↾t A ) ↾t B ) = ( J ↾t ( A i^i B ) ) )
Theorem	restabs 14898	Equivalence of being a subspace of a subspace and being a subspace of the original. (Contributed by Jeff Hankins, 11-Jul-2009.) (Proof shortened by Mario Carneiro, 1-May-2015.)
|- ( ( J e. V /\ S C_ T /\ T e. W ) -> ( ( J ↾t T ) ↾t S ) = ( J ↾t S ) )
Theorem	restin 14899	When the subspace region is not a subset of the base of the topology, the resulting set is the same as the subspace restricted to the base. (Contributed by Mario Carneiro, 15-Dec-2013.)
|- X = U. J   =>    |- ( ( J e. V /\ A e. W ) -> ( J ↾t A ) = ( J ↾t ( A i^i X ) ) )
Theorem	restuni2 14900	The underlying set of a subspace topology. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ A e. V ) -> ( A i^i X ) = U. ( J ↾t A ) )