P. 147 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14601-14700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	psrbaglesuppg 14601*	The support of a dominated bag is smaller than the dominating bag. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝐺:𝐼⟶ℕ0 ∧ 𝐺 ∘𝑟 ≤ 𝐹)) → (◡𝐺 “ ℕ) ⊆ (◡𝐹 “ ℕ))
Theorem	psrbagfi 14602*	A finite index set gives a simpler expression for finite bags. (Contributed by Jim Kingdon, 23-Nov-2025.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ⊢ (𝐼 ∈ Fin → 𝐷 = (ℕ0 ↑𝑚 𝐼))
Theorem	psrbasg 14603*	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.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐵 = (𝐾 ↑𝑚 𝐷))
Theorem	psrelbas 14604*	An element of the set of power series is a function on the coefficients. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋:𝐷⟶𝐾)
Theorem	psrelbasfi 14605	Simpler form of psrelbas 14604 when the index set is finite. (Contributed by Jim Kingdon, 27-Nov-2025.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋:(ℕ0 ↑𝑚 𝐼)⟶𝐾)
Theorem	psrelbasfun 14606	An element of the set of power series is a function. (Contributed by AV, 17-Jul-2019.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝑋 ∈ 𝐵 → Fun 𝑋)
Theorem	psrplusgg 14607	The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ✚ = (+g‘𝑆)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ✚ = ( ∘𝑓 + ↾ (𝐵 × 𝐵)))
Theorem	psradd 14608	The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ✚ = (+g‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ✚ 𝑌) = (𝑋 ∘𝑓 + 𝑌))
Theorem	psraddcl 14609	Closure of the power series addition operation. (Contributed by Mario Carneiro, 28-Dec-2014.) Generalize to magmas. (Revised by SN, 12-Apr-2025.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Mgm)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	psr0cl 14610*	The zero element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝜑 → (𝐷 × { 0 }) ∈ 𝐵)
Theorem	psr0lid 14611*	The zero element of the ring of power series is a left identity. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐷 × { 0 }) + 𝑋) = 𝑋)
Theorem	psrnegcl 14612*	The negative function in the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑁 ∘ 𝑋) ∈ 𝐵)
Theorem	psrlinv 14613*	The negative function in the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ + = (+g‘𝑆)    ⇒   ⊢ (𝜑 → ((𝑁 ∘ 𝑋) + 𝑋) = (𝐷 × { 0 }))
Theorem	psrgrp 14614	The ring of power series is a group. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof shortened by SN, 7-Feb-2025.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    ⇒   ⊢ (𝜑 → 𝑆 ∈ Grp)
Theorem	psr0 14615*	The zero element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑂 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑆)    ⇒   ⊢ (𝜑 → 0 = (𝐷 × {𝑂}))
Theorem	psrneg 14616*	The negative function of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑀 = (invg‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑀‘𝑋) = (𝑁 ∘ 𝑋))
Theorem	psr1clfi 14617*	The identity element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑈 = (𝑥 ∈ 𝐷 ↦ if(𝑥 = (𝐼 × {0}), 1 , 0 ))    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝐵)
Theorem	reldmmpl 14618	The multivariate polynomial constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ Rel dom mPoly
Theorem	mplvalcoe 14619*	Value of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = {𝑓 ∈ 𝐵 ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝐼)∀𝑏 ∈ (ℕ0 ↑𝑚 𝐼)(∀𝑘 ∈ 𝐼 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = 0 )}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → 𝑃 = (𝑆 ↾s 𝑈))
Theorem	mplbascoe 14620*	Base set of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → 𝑈 = {𝑓 ∈ 𝐵 ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝐼)∀𝑏 ∈ (ℕ0 ↑𝑚 𝐼)(∀𝑘 ∈ 𝐼 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = 0 )})
Theorem	mplelbascoe 14621*	Property of being a polynomial. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝐼)∀𝑏 ∈ (ℕ0 ↑𝑚 𝐼)(∀𝑘 ∈ 𝐼 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑋‘𝑏) = 0 ))))
Theorem	fnmpl 14622	mPoly has universal domain. (Contributed by Jim Kingdon, 5-Nov-2025.)
⊢ mPoly Fn (V × V)
Theorem	mplrcl 14623	Reverse closure for the polynomial index set. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by Mario Carneiro, 30-Aug-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝑋 ∈ 𝐵 → 𝐼 ∈ V)
Theorem	mplval2g 14624	Self-referential expression for the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → 𝑃 = (𝑆 ↾s 𝑈))
Theorem	mplbasss 14625	The set of polynomials is a subset of the set of power series. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ 𝑈 ⊆ 𝐵
Theorem	mplelf 14626*	A polynomial is defined as a function on the coefficients. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋:𝐷⟶𝐾)
Theorem	mplsubgfilemm 14627*	Lemma for mplsubgfi 14630. There exists a polynomial. (Contributed by Jim Kingdon, 21-Nov-2025.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    ⇒   ⊢ (𝜑 → ∃𝑗 𝑗 ∈ 𝑈)
Theorem	mplsubgfilemcl 14628	Lemma for mplsubgfi 14630. The sum of two polynomials is a polynomial. (Contributed by Jim Kingdon, 26-Nov-2025.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    &   ⊢ + = (+g‘𝑆)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝑈)
Theorem	mplsubgfileminv 14629	Lemma for mplsubgfi 14630. The additive inverse of a polynomial is a polynomial. (Contributed by Jim Kingdon, 26-Nov-2025.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑈)    &   ⊢ 𝑁 = (invg‘𝑆)    ⇒   ⊢ (𝜑 → (𝑁‘𝑋) ∈ 𝑈)
Theorem	mplsubgfi 14630	The set of polynomials is closed under addition, i.e. it is a subgroup of the set of power series. (Contributed by Mario Carneiro, 8-Jan-2015.) (Proof shortened by AV, 16-Jul-2019.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    ⇒   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝑆))
Theorem	mpl0fi 14631*	The zero polynomial. (Contributed by Mario Carneiro, 9-Jan-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑂 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    ⇒   ⊢ (𝜑 → 0 = (𝑥 ∈ (ℕ0 ↑𝑚 𝐼) ↦ 𝑂))
Theorem	mplplusgg 14632	Value of addition in a polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑌 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ + = (+g‘𝑌)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → + = (+g‘𝑆))
Theorem	mpladd 14633	The addition operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ✚ = (+g‘𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ✚ 𝑌) = (𝑋 ∘𝑓 + 𝑌))
Theorem	mplnegfi 14634	The negative function on multivariate polynomials. (Contributed by SN, 25-May-2024.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 𝑀 = (invg‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑀‘𝑋) = (𝑁 ∘ 𝑋))
Theorem	mplgrpfi 14635	The polynomial ring is a group. (Contributed by Mario Carneiro, 9-Jan-2015.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    ⇒   ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ Grp) → 𝑃 ∈ Grp)
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 14636	Syntax for the class of topologies.
class Top
Definition	df-top 14637*	Define the class of topologies. It is a proper class. See istopg 14638 and istopfin 14639 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 = {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥)}
Theorem	istopg 14638*	Express the predicate "𝐽 is a topology". See istopfin 14639 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 𝑇 to represent linear transformations (operators). (Contributed by Stefan Allan, 3-Mar-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ (𝐽 ∈ 𝐴 → (𝐽 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽)))
Theorem	istopfin 14639*	Express the predicate "𝐽 is a topology" using nonempty finite intersections instead of binary intersections as in istopg 14638. 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.)
⊢ (𝐽 ∈ Top → (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥((𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐽)))
Theorem	uniopn 14640	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.)
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽) → ∪ 𝐴 ∈ 𝐽)
Theorem	iunopn 14641*	The indexed union of a subset of a topology is an open set. (Contributed by NM, 5-Oct-2006.)
⊢ ((𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)
Theorem	inopn 14642	The intersection of two open sets of a topology is an open set. (Contributed by NM, 17-Jul-2006.)
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∩ 𝐵) ∈ 𝐽)
Theorem	fiinopn 14643	The intersection of a nonempty finite family of open sets is open. (Contributed by FL, 20-Apr-2012.)
⊢ (𝐽 ∈ Top → ((𝐴 ⊆ 𝐽 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin) → ∩ 𝐴 ∈ 𝐽))
Theorem	unopn 14644	The union of two open sets is open. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∪ 𝐵) ∈ 𝐽)
Theorem	0opn 14645	The empty set is an open subset of any topology. (Contributed by Stefan Allan, 27-Feb-2006.)
⊢ (𝐽 ∈ Top → ∅ ∈ 𝐽)
Theorem	0ntop 14646	The empty set is not a topology. (Contributed by FL, 1-Jun-2008.)
⊢ ¬ ∅ ∈ Top
Theorem	topopn 14647	The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
Theorem	eltopss 14648	A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋)
9.1.1.2  Topologies on sets
Syntax	ctopon 14649	Syntax for the function of topologies on sets.
class TopOn
Definition	df-topon 14650*	Define the function that associates with a set the set of topologies on it. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ TopOn = (𝑏 ∈ V ↦ {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗})
Theorem	funtopon 14651	The class TopOn is a function. (Contributed by BJ, 29-Apr-2021.)
⊢ Fun TopOn
Theorem	istopon 14652	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.)
⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽))
Theorem	topontop 14653	A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
Theorem	toponuni 14654	The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)
Theorem	topontopi 14655	A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐽 ∈ (TopOn‘𝐵)    ⇒   ⊢ 𝐽 ∈ Top
Theorem	toponunii 14656	The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐽 ∈ (TopOn‘𝐵)    ⇒   ⊢ 𝐵 = ∪ 𝐽
Theorem	toptopon 14657	Alternative definition of Top in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
Theorem	toptopon2 14658	A topology is the same thing as a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))
Theorem	topontopon 14659	A topology on a set is a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ (TopOn‘∪ 𝐽))
Theorem	toponrestid 14660	Given a topology on a set, restricting it to that same set has no effect. (Contributed by Jim Kingdon, 6-Jul-2022.)
⊢ 𝐴 ∈ (TopOn‘𝐵)    ⇒   ⊢ 𝐴 = (𝐴 ↾t 𝐵)
Theorem	toponsspwpwg 14661	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.)
⊢ (𝐴 ∈ 𝑉 → (TopOn‘𝐴) ⊆ 𝒫 𝒫 𝐴)
Theorem	dmtopon 14662	The domain of TopOn is V. (Contributed by BJ, 29-Apr-2021.)
⊢ dom TopOn = V
Theorem	fntopon 14663	The class TopOn is a function with domain V. (Contributed by BJ, 29-Apr-2021.)
⊢ TopOn Fn V
Theorem	toponmax 14664	The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽)
Theorem	toponss 14665	A member of a topology is a subset of its underlying set. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋)
Theorem	toponcom 14666	If 𝐾 is a topology on the base set of topology 𝐽, then 𝐽 is a topology on the base of 𝐾. (Contributed by Mario Carneiro, 22-Aug-2015.)
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ (TopOn‘∪ 𝐽)) → 𝐽 ∈ (TopOn‘∪ 𝐾))
Theorem	toponcomb 14667	Biconditional form of toponcom 14666. (Contributed by BJ, 5-Dec-2021.)
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 ∈ (TopOn‘∪ 𝐾) ↔ 𝐾 ∈ (TopOn‘∪ 𝐽)))
Theorem	topgele 14668	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.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → ({∅, 𝑋} ⊆ 𝐽 ∧ 𝐽 ⊆ 𝒫 𝑋))
9.1.1.3  Topological spaces
Syntax	ctps 14669	Syntax for the class of topological spaces.
class TopSp
Definition	df-topsp 14670	Define the class of topological spaces (as extensible structures). (Contributed by Stefan O'Rear, 13-Aug-2015.)
⊢ TopSp = {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))}
Theorem	istps 14671	Express the predicate "is a topological space". (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐴 = (Base‘𝐾)    &   ⊢ 𝐽 = (TopOpen‘𝐾)    ⇒   ⊢ (𝐾 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐴))
Theorem	istps2 14672	Express the predicate "is a topological space". (Contributed by NM, 20-Oct-2012.)
⊢ 𝐴 = (Base‘𝐾)    &   ⊢ 𝐽 = (TopOpen‘𝐾)    ⇒   ⊢ (𝐾 ∈ TopSp ↔ (𝐽 ∈ Top ∧ 𝐴 = ∪ 𝐽))
Theorem	tpsuni 14673	The base set of a topological space. (Contributed by FL, 27-Jun-2014.)
⊢ 𝐴 = (Base‘𝐾)    &   ⊢ 𝐽 = (TopOpen‘𝐾)    ⇒   ⊢ (𝐾 ∈ TopSp → 𝐴 = ∪ 𝐽)
Theorem	tpstop 14674	The topology extractor on a topological space is a topology. (Contributed by FL, 27-Jun-2014.)
⊢ 𝐽 = (TopOpen‘𝐾)    ⇒   ⊢ (𝐾 ∈ TopSp → 𝐽 ∈ Top)
Theorem	tpspropd 14675	A topological space depends only on the base and topology components. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 13-Aug-2015.)
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿))    &   ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))    ⇒   ⊢ (𝜑 → (𝐾 ∈ TopSp ↔ 𝐿 ∈ TopSp))
Theorem	topontopn 14676	Express the predicate "is a topological space". (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐴 = (Base‘𝐾)    &   ⊢ 𝐽 = (TopSet‘𝐾)    ⇒   ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐽 = (TopOpen‘𝐾))
Theorem	tsettps 14677	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.)
⊢ 𝐴 = (Base‘𝐾)    &   ⊢ 𝐽 = (TopSet‘𝐾)    ⇒   ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐾 ∈ TopSp)
Theorem	istpsi 14678	Properties that determine a topological space. (Contributed by NM, 20-Oct-2012.)
⊢ (Base‘𝐾) = 𝐴    &   ⊢ (TopOpen‘𝐾) = 𝐽    &   ⊢ 𝐴 = ∪ 𝐽    &   ⊢ 𝐽 ∈ Top    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	eltpsg 14679	Properties that determine a topological space from a construction (using no explicit indices). (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐾 = {⟨(Base‘ndx), 𝐴⟩, ⟨(TopSet‘ndx), 𝐽⟩}    ⇒   ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐾 ∈ TopSp)
Theorem	eltpsi 14680	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.)
⊢ 𝐾 = {⟨(Base‘ndx), 𝐴⟩, ⟨(TopSet‘ndx), 𝐽⟩}    &   ⊢ 𝐴 = ∪ 𝐽    &   ⊢ 𝐽 ∈ Top    ⇒   ⊢ 𝐾 ∈ TopSp
9.1.2  Topological bases
Syntax	ctb 14681	Syntax for the class of topological bases.
class TopBases
Definition	df-bases 14682*	Define the class of topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 14684). Note that "bases" is the plural of "basis". (Contributed by NM, 17-Jul-2006.)
⊢ TopBases = {𝑥 ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ⊆ ∪ (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))}
Theorem	isbasisg 14683*	Express the predicate "the set 𝐵 is a basis for a topology". (Contributed by NM, 17-Jul-2006.)
⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦))))
Theorem	isbasis2g 14684*	Express the predicate "the set 𝐵 is a basis for a topology". (Contributed by NM, 17-Jul-2006.)
⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ (𝑥 ∩ 𝑦)∃𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑥 ∩ 𝑦))))
Theorem	isbasis3g 14685*	Express the predicate "the set 𝐵 is a basis for a topology". Definition of basis in [Munkres] p. 78. (Contributed by NM, 17-Jul-2006.)
⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ (∀𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ ∪ 𝐵∃𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ (𝑥 ∩ 𝑦)∃𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑥 ∩ 𝑦)))))
Theorem	basis1 14686	Property of a basis. (Contributed by NM, 16-Jul-2006.)
⊢ ((𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵) → (𝐶 ∩ 𝐷) ⊆ ∪ (𝐵 ∩ 𝒫 (𝐶 ∩ 𝐷)))
Theorem	basis2 14687*	Property of a basis. (Contributed by NM, 17-Jul-2006.)
⊢ (((𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵) ∧ (𝐷 ∈ 𝐵 ∧ 𝐴 ∈ (𝐶 ∩ 𝐷))) → ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷)))
Theorem	fiinbas 14688*	If a set is closed under finite intersection, then it is a basis for a topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐵 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ∈ 𝐵) → 𝐵 ∈ TopBases)
Theorem	baspartn 14689*	A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝑃 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) → 𝑃 ∈ TopBases)
Theorem	tgval2 14690*	Definition of a topology generated by a basis in [Munkres] p. 78. Later we show (in tgcl 14703) that (topGen‘𝐵) is indeed a topology (on ∪ 𝐵, see unitg 14701). See also tgval 13261 and tgval3 14697. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ (𝑥 ⊆ ∪ 𝐵 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐵 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))})
Theorem	eltg 14691	Membership in a topology generated by a basis. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ 𝐴 ⊆ ∪ (𝐵 ∩ 𝒫 𝐴)))
Theorem	eltg2 14692*	Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ (𝐴 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴))))
Theorem	eltg2b 14693*	Membership in a topology generated by a basis. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Mario Carneiro, 10-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴)))
Theorem	eltg4i 14694	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.)
⊢ (𝐴 ∈ (topGen‘𝐵) → 𝐴 = ∪ (𝐵 ∩ 𝒫 𝐴))
Theorem	eltg3i 14695	The union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → ∪ 𝐴 ∈ (topGen‘𝐵))
Theorem	eltg3 14696*	Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Jim Kingdon, 4-Mar-2023.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∃𝑥(𝑥 ⊆ 𝐵 ∧ 𝐴 = ∪ 𝑥)))
Theorem	tgval3 14697*	Alternate expression for the topology generated by a basis. Lemma 2.1 of [Munkres] p. 80. See also tgval 13261 and tgval2 14690. (Contributed by NM, 17-Jul-2006.) (Revised by Mario Carneiro, 30-Aug-2015.)
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦)})
Theorem	tg1 14698	Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.)
⊢ (𝐴 ∈ (topGen‘𝐵) → 𝐴 ⊆ ∪ 𝐵)
Theorem	tg2 14699*	Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.)
⊢ ((𝐴 ∈ (topGen‘𝐵) ∧ 𝐶 ∈ 𝐴) → ∃𝑥 ∈ 𝐵 (𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴))
Theorem	bastg 14700	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.)
⊢ (𝐵 ∈ 𝑉 → 𝐵 ⊆ (topGen‘𝐵))