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.)
⊢ ((𝜑 ∧ (((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp511 32302	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ ((𝜑 ∧ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp512 32303	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏))) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	3com12d 32304	Commutation in consequent. Swap 1st and 2nd. (Contributed by Jeff Hankins, 17-Nov-2009.)
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → (𝜒 ∧ 𝜓 ∧ 𝜃))
Theorem	imp5p 32305	A triple importation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜂)))
Theorem	imp5q 32306	A triple importation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜂))
Theorem	ecase13d 32307	Deduction for elimination by cases. (Contributed by Jeff Hankins, 18-Aug-2009.)
⊢ (𝜑 → ¬ 𝜒)    &   ⊢ (𝜑 → ¬ 𝜃)    &   ⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	subtr 32308	Transitivity of implicit substitution. (Contributed by Jeff Hankins, 13-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝑌    &   ⊢ Ⅎ𝑥𝑍    &   ⊢ (𝑥 = 𝐴 → 𝑋 = 𝑌)    &   ⊢ (𝑥 = 𝐵 → 𝑋 = 𝑍)    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 = 𝐵 → 𝑌 = 𝑍))
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.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 = 𝐵 → (𝜓 ↔ 𝜒)))
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.)
⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ( ≤ ∩ ◡ ≤ ) Er dom ( ≤ ∩ ◡ ≤ ))
Theorem	elicc3 32311	An equivalent membership condition for closed intervals. (Contributed by Jeff Hankins, 14-Jul-2009.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ (𝐶 = 𝐴 ∨ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵) ∨ 𝐶 = 𝐵))))
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.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ Fin 𝜑 → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦)))
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.)
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∧ (𝐴 ∈ ℝ ∧ inf(𝑆, ℝ, < ) < 𝐴)) → ∃𝑧 ∈ 𝑆 𝑧 < 𝐴)
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.)
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∧ (𝐴 ∈ ℝ ∧ sup(𝑆, ℝ, ◡ < ) < 𝐴)) → ∃𝑧 ∈ 𝑆 𝑧 < 𝐴)
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.)
⊢ (𝐴 ∈ (topGen‘ran (,)) ↔ (𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ℝ+ ((𝑥 − 𝑦)(,)(𝑥 + 𝑦)) ⊆ 𝐴))
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.)
⊢ (𝐴 ∈ (topGen‘ran (,)) ↔ (𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ (𝑧 ≤ 𝑦 ∧ ((𝑥 − 𝑧)(,)(𝑥 + 𝑧)) ⊆ 𝐴)))
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.)
⊢ (𝐴 ∈ ℕ → ∀𝑘 ∈ ℕ (𝑘 < 𝐴 → ∃𝑝 ∈ ℙ ∃𝑛 ∈ ℕ ¬ ((𝑝↑𝑛) ∥ 𝑘 ↔ (𝑝↑𝑛) ∥ 𝐴)))
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.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 = 𝐵 ↔ ∀𝑝 ∈ ℙ ∀𝑛 ∈ ℕ ((𝑝↑𝑛) ∥ 𝐴 ↔ (𝑝↑𝑛) ∥ 𝐵)))
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.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (((cls‘𝐽)‘𝐴) ∩ ((cls‘𝐽)‘(𝑋 ∖ 𝐴))) = (((cls‘𝐽)‘𝐴) ∖ ((int‘𝐽)‘𝐴)))
Theorem	opnbnd 32320	A set is open iff it is disjoint from its boundary. (Contributed by Jeff Hankins, 23-Sep-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ 𝐽 ↔ (𝐴 ∩ (((cls‘𝐽)‘𝐴) ∩ ((cls‘𝐽)‘(𝑋 ∖ 𝐴)))) = ∅))
Theorem	cldbnd 32321	A set is closed iff it contains its boundary. (Contributed by Jeff Hankins, 1-Oct-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ (Clsd‘𝐽) ↔ (((cls‘𝐽)‘𝐴) ∩ ((cls‘𝐽)‘(𝑋 ∖ 𝐴))) ⊆ 𝐴))
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.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑂 ⊆ 𝒫 𝑋) → ∪ 𝑜 ∈ 𝑂 ((int‘𝐽)‘𝑜) ⊆ ((int‘𝐽)‘∪ 𝑂))
Theorem	clsun 32323	A pairwise union of closures is the closure of the union. (Contributed by Jeff Hankins, 31-Aug-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) → ((cls‘𝐽)‘(𝐴 ∪ 𝐵)) = (((cls‘𝐽)‘𝐴) ∪ ((cls‘𝐽)‘𝐵)))
Theorem	clsint2 32324*	The closure of an intersection is a subset of the intersection of the closures. (Contributed by Jeff Hankins, 31-Aug-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐶 ⊆ 𝒫 𝑋) → ((cls‘𝐽)‘∩ 𝐶) ⊆ ∩ 𝑐 ∈ 𝐶 ((cls‘𝐽)‘𝑐))
Theorem	opnregcld 32325*	A set is regularly closed iff it is the closure of some open set. (Contributed by Jeff Hankins, 27-Sep-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (((cls‘𝐽)‘((int‘𝐽)‘𝐴)) = 𝐴 ↔ ∃𝑜 ∈ 𝐽 𝐴 = ((cls‘𝐽)‘𝑜)))
Theorem	cldregopn 32326*	A set if regularly open iff it is the interior of some closed set. (Contributed by Jeff Hankins, 27-Sep-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴 ↔ ∃𝑐 ∈ (Clsd‘𝐽)𝐴 = ((int‘𝐽)‘𝑐)))
Theorem	neiin 32327	Two neighborhoods intersect to form a neighborhood of the intersection. (Contributed by Jeff Hankins, 31-Aug-2009.)
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → (𝑀 ∩ 𝑁) ∈ ((nei‘𝐽)‘(𝐴 ∩ 𝐵)))
Theorem	hmeoclda 32328	Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009.) (Revised by Mario Carneiro, 3-Jun-2014.)
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ (𝐽Homeo𝐾)) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝐹 “ 𝑆) ∈ (Clsd‘𝐾))
Theorem	hmeocldb 32329	Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009.)
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ (𝐽Homeo𝐾)) ∧ 𝑆 ∈ (Clsd‘𝐾)) → (◡𝐹 “ 𝑆) ∈ (Clsd‘𝐽))
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.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷–cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹‘𝐴)(,)(𝐹‘𝐵))))) → ∃𝑥 ∈ (𝐴(,)𝐵)(𝐹‘𝑥) = 𝑈)
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 = {⟨𝑥, 𝑦⟩ ∣ (∪ 𝑥 = ∪ 𝑦 ∧ ∀𝑧 ∈ 𝑥 𝑧 ⊆ ∪ (𝑦 ∩ 𝒫 𝑧))}
Theorem	fnerel 32333	Fineness is a relation. (Contributed by Jeff Hankins, 28-Sep-2009.)
⊢ Rel Fne
Theorem	isfne 32334*	The predicate "𝐵 is finer than 𝐴." 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.)
⊢ 𝑋 = ∪ 𝐴    &   ⊢ 𝑌 = ∪ 𝐵    ⇒   ⊢ (𝐵 ∈ 𝐶 → (𝐴Fne𝐵 ↔ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥))))
Theorem	isfne4 32335	The predicate "𝐵 is finer than 𝐴 " in terms of the topology generation function. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ 𝑋 = ∪ 𝐴    &   ⊢ 𝑌 = ∪ 𝐵    ⇒   ⊢ (𝐴Fne𝐵 ↔ (𝑋 = 𝑌 ∧ 𝐴 ⊆ (topGen‘𝐵)))
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.)
⊢ 𝑋 = ∪ 𝐴    &   ⊢ 𝑌 = ∪ 𝐵    ⇒   ⊢ (𝐵 ∈ 𝑉 → (𝐴Fne𝐵 ↔ (𝑋 = 𝑌 ∧ (topGen‘𝐴) ⊆ (topGen‘𝐵))))
Theorem	isfne2 32337*	The predicate "𝐵 is finer than 𝐴." (Contributed by Jeff Hankins, 28-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
⊢ 𝑋 = ∪ 𝐴    &   ⊢ 𝑌 = ∪ 𝐵    ⇒   ⊢ (𝐵 ∈ 𝐶 → (𝐴Fne𝐵 ↔ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐵 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))))
Theorem	isfne3 32338*	The predicate "𝐵 is finer than 𝐴." (Contributed by Jeff Hankins, 11-Oct-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
⊢ 𝑋 = ∪ 𝐴    &   ⊢ 𝑌 = ∪ 𝐵    ⇒   ⊢ (𝐵 ∈ 𝐶 → (𝐴Fne𝐵 ↔ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦))))
Theorem	fnebas 32339	A finer cover covers the same set as the original. (Contributed by Jeff Hankins, 28-Sep-2009.)
⊢ 𝑋 = ∪ 𝐴    &   ⊢ 𝑌 = ∪ 𝐵    ⇒   ⊢ (𝐴Fne𝐵 → 𝑋 = 𝑌)
Theorem	fnetg 32340	A finer cover generates a topology finer than the original set. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ (𝐴Fne𝐵 → 𝐴 ⊆ (topGen‘𝐵))
Theorem	fnessex 32341*	If 𝐵 is finer than 𝐴 and 𝑆 is an element of 𝐴, every point in 𝑆 is an element of a subset of 𝑆 which is in 𝐵. (Contributed by Jeff Hankins, 28-Sep-2009.)
⊢ ((𝐴Fne𝐵 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝑆) → ∃𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑆))
Theorem	fneuni 32342*	If 𝐵 is finer than 𝐴, every element of 𝐴 is a union of elements of 𝐵. (Contributed by Jeff Hankins, 11-Oct-2009.)
⊢ ((𝐴Fne𝐵 ∧ 𝑆 ∈ 𝐴) → ∃𝑥(𝑥 ⊆ 𝐵 ∧ 𝑆 = ∪ 𝑥))
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.)
⊢ (𝐴Fne𝐵 → ∩ {𝑥 ∈ 𝐵 ∣ 𝑃 ∈ 𝑥} ⊆ ∩ {𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥})
Theorem	fness 32344	A cover is finer than its subcovers. (Contributed by Jeff Hankins, 11-Oct-2009.)
⊢ 𝑋 = ∪ 𝐴    &   ⊢ 𝑌 = ∪ 𝐵    ⇒   ⊢ ((𝐵 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐵 ∧ 𝑋 = 𝑌) → 𝐴Fne𝐵)
Theorem	fneref 32345	Reflexivity of the fineness relation. (Contributed by Jeff Hankins, 12-Oct-2009.)
⊢ (𝐴 ∈ 𝑉 → 𝐴Fne𝐴)
Theorem	fnetr 32346	Transitivity of the fineness relation. (Contributed by Jeff Hankins, 5-Oct-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
⊢ ((𝐴Fne𝐵 ∧ 𝐵Fne𝐶) → 𝐴Fne𝐶)
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 ∩ ◡Fne)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∼ 𝐵 ↔ (topGen‘𝐴) = (topGen‘𝐵)))
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 ∩ ◡Fne)    ⇒   ⊢ ∼ Er V
Theorem	topfne 32349	Fineness for covers corresponds precisely with fineness for topologies. (Contributed by Jeff Hankins, 29-Sep-2009.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ ((𝐾 ∈ Top ∧ 𝑋 = 𝑌) → (𝐽 ⊆ 𝐾 ↔ 𝐽Fne𝐾))
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 ∩ ◡Fne)    ⇒   ⊢ (𝐽 ∈ Top → (𝐴 ∈ [𝐽] ∼ ↔ (topGen‘𝐴) = 𝐽))
Theorem	topfneec2 32351	A topology is precisely identified with its equivalence class. (Contributed by Jeff Hankins, 12-Oct-2009.)
⊢ ∼ = (Fne ∩ ◡Fne)    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → ([𝐽] ∼ = [𝐾] ∼ ↔ 𝐽 = 𝐾))
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.)
⊢ 𝑋 = ∪ 𝐴    &   ⊢ 𝑌 = ∪ 𝐵    ⇒   ⊢ (𝑋 = 𝑌 → (𝐴Fne𝐵 ↔ ∃𝑐(𝑐 ⊆ 𝐵 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴))))
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.)
⊢ 𝑋 = ∪ 𝐴    &   ⊢ 𝑌 = ∪ 𝐵    ⇒   ⊢ (𝑋 = 𝑌 → (𝐵Ref𝐴 ↔ ∃𝑐(𝐵 ⊆ 𝑐 ∧ (𝐴Fne𝑐 ∧ 𝑐Ref𝐴))))
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.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥) ∧ 𝑤 ∈ (𝐹‘𝑥))) → ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅)    &   ⊢ 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅}    ⇒   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
Theorem	neibastop2lem 32355*	Lemma for neibastop2 32356. (Contributed by Jeff Hankins, 12-Sep-2009.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥) ∧ 𝑤 ∈ (𝐹‘𝑥))) → ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅)    &   ⊢ 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅}    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → 𝑥 ∈ 𝑣)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)    &   ⊢ (𝜑 → 𝑃 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑁 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑈 ∈ (𝐹‘𝑃))    &   ⊢ (𝜑 → 𝑈 ⊆ 𝑁)    &   ⊢ 𝐺 = (rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)    &   ⊢ 𝑆 = {𝑦 ∈ 𝑋 ∣ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅}    ⇒   ⊢ (𝜑 → ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))
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.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥) ∧ 𝑤 ∈ (𝐹‘𝑥))) → ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅)    &   ⊢ 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅}    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → 𝑥 ∈ 𝑣)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)    ⇒   ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ 𝑋 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
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.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥) ∧ 𝑤 ∈ (𝐹‘𝑥))) → ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅)    &   ⊢ 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅}    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → 𝑥 ∈ 𝑣)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)    ⇒   ⊢ (𝜑 → ∃!𝑗 ∈ (TopOn‘𝑋)∀𝑥 ∈ 𝑋 ((nei‘𝑗)‘{𝑥}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((𝐹‘𝑥) ∩ 𝒫 𝑛) ≠ ∅})
20.9.6  Lattice structure of topologies
Theorem	topmtcl 32358	The meet of a collection of topologies on 𝑋 is again a topology on 𝑋. (Contributed by Jeff Hankins, 5-Oct-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → (𝒫 𝑋 ∩ ∩ 𝑆) ∈ (TopOn‘𝑋))
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.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → (𝒫 𝑋 ∩ ∩ 𝑆) = ∪ {𝑘 ∈ (TopOn‘𝑋) ∣ ∀𝑗 ∈ 𝑆 𝑘 ⊆ 𝑗})
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.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ (TopOn‘𝑋)) → (topGen‘(fi‘({𝑋} ∪ ∪ 𝑆))) = ∩ {𝑘 ∈ (TopOn‘𝑋) ∣ ∀𝑗 ∈ 𝑆 𝑗 ⊆ 𝑘})
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.)
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) → (𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 (topGen‘𝑡))Fne𝐴)
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.)
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) → (𝑇Fne(𝒫 𝑋 ∩ ∩ 𝑡 ∈ 𝑆 (topGen‘𝑡)) ↔ (𝑋 = ∪ 𝑇 ∧ ∀𝑥 ∈ 𝑆 𝑇Fne𝑥)))
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.)
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦 ∧ 𝐴 ∈ 𝑆) → 𝐴Fneif(𝑆 = ∅, {𝑋}, ∪ 𝑆))
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.)
⊢ ((𝑋 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝑆 𝑋 = ∪ 𝑦) → (if(𝑆 = ∅, {𝑋}, ∪ 𝑆)Fne𝑇 ↔ (𝑋 = ∪ 𝑇 ∧ ∀𝑥 ∈ 𝑆 𝑥Fne𝑇)))
20.9.7  Filter bases
Theorem	fgmin 32365	Minimality property of a generated filter: every filter that contains 𝐵 contains its generated filter. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Mario Carneiro, 7-Aug-2015.)
⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐵 ⊆ 𝐹 ↔ (𝑋filGen𝐵) ⊆ 𝐹))
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.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → (𝑋filGen{𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}) = ((nei‘𝐽)‘𝑆))
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.)
⊢ 𝑋 = dom 𝐷    ⇒   ⊢ (𝐷 ∈ DirRel → (tail‘𝐷) = (𝑥 ∈ 𝑋 ↦ (𝐷 “ {𝑥})))
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.)
⊢ 𝑋 = dom 𝐷    ⇒   ⊢ ((𝐷 ∈ DirRel ∧ 𝐴 ∈ 𝑋) → ((tail‘𝐷)‘𝐴) = (𝐷 “ {𝐴}))
Theorem	eltail 32369	An element of a tail. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 24-Nov-2013.)
⊢ 𝑋 = dom 𝐷    ⇒   ⊢ ((𝐷 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝐶) → (𝐵 ∈ ((tail‘𝐷)‘𝐴) ↔ 𝐴𝐷𝐵))
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.)
⊢ 𝑋 = dom 𝐷    ⇒   ⊢ (𝐷 ∈ DirRel → (tail‘𝐷):𝑋⟶𝒫 𝑋)
Theorem	tailini 32371	A tail contains its initial element. (Contributed by Jeff Hankins, 25-Nov-2009.)
⊢ 𝑋 = dom 𝐷    ⇒   ⊢ ((𝐷 ∈ DirRel ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ ((tail‘𝐷)‘𝐴))
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.)
⊢ 𝑋 = dom 𝐷    ⇒   ⊢ ((𝐷 ∈ DirRel ∧ 𝑋 ≠ ∅) → ran (tail‘𝐷) ∈ (fBas‘𝑋))
Theorem	filnetlem1 32373*	Lemma for filnet 32377. Change variables. (Contributed by Jeff Hankins, 13-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.)
⊢ 𝐻 = ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛)    &   ⊢ 𝐷 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ (1st ‘𝑦) ⊆ (1st ‘𝑥))}    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴𝐷𝐵 ↔ ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) ∧ (1st ‘𝐵) ⊆ (1st ‘𝐴)))
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.)
⊢ 𝐻 = ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛)    &   ⊢ 𝐷 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ (1st ‘𝑦) ⊆ (1st ‘𝑥))}    ⇒   ⊢ (( I ↾ 𝐻) ⊆ 𝐷 ∧ 𝐷 ⊆ (𝐻 × 𝐻))
Theorem	filnetlem3 32375*	Lemma for filnet 32377. (Contributed by Jeff Hankins, 13-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.)
⊢ 𝐻 = ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛)    &   ⊢ 𝐷 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ (1st ‘𝑦) ⊆ (1st ‘𝑥))}    ⇒   ⊢ (𝐻 = ∪ ∪ 𝐷 ∧ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel)))
Theorem	filnetlem4 32376*	Lemma for filnet 32377. (Contributed by Jeff Hankins, 15-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.)
⊢ 𝐻 = ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛)    &   ⊢ 𝐷 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ (1st ‘𝑦) ⊆ (1st ‘𝑥))}    ⇒   ⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))
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.)
⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))
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.)
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
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.)
⊢ (𝜑 → (𝜓 → 𝜑))
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.)
⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜑)
Theorem	tbsyl 32381	The weak syllogism from Tarski-Bernays'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	re1ax2lem 32382	Lemma for re1ax2 32383. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))
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.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
Theorem	naim1 32384	Constructor theorem for ⊼. (Contributed by Anthony Hart, 1-Sep-2011.)
⊢ ((𝜑 → 𝜓) → ((𝜓 ⊼ 𝜒) → (𝜑 ⊼ 𝜒)))
Theorem	naim2 32385	Constructor theorem for ⊼. (Contributed by Anthony Hart, 1-Sep-2011.)
⊢ ((𝜑 → 𝜓) → ((𝜒 ⊼ 𝜓) → (𝜒 ⊼ 𝜑)))
Theorem	naim1i 32386	Constructor rule for ⊼. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 ⊼ 𝜒)    ⇒   ⊢ (𝜑 ⊼ 𝜒)
Theorem	naim2i 32387	Constructor rule for ⊼. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 ⊼ 𝜓)    ⇒   ⊢ (𝜒 ⊼ 𝜑)
Theorem	naim12i 32388	Constructor rule for ⊼. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜓 ⊼ 𝜃)    ⇒   ⊢ (𝜑 ⊼ 𝜒)
Theorem	nabi1 32389	Constructor theorem for ⊼. (Contributed by Anthony Hart, 1-Sep-2011.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ⊼ 𝜒) ↔ (𝜓 ⊼ 𝜒)))
Theorem	nabi2 32390	Constructor theorem for ⊼. (Contributed by Anthony Hart, 1-Sep-2011.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ⊼ 𝜑) ↔ (𝜒 ⊼ 𝜓)))
Theorem	nabi1i 32391	Constructor rule for ⊼. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 ⊼ 𝜒)    ⇒   ⊢ (𝜑 ⊼ 𝜒)
Theorem	nabi2i 32392	Constructor rule for ⊼. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ⊼ 𝜓)    ⇒   ⊢ (𝜒 ⊼ 𝜑)
Theorem	nabi12i 32393	Constructor rule for ⊼. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    &   ⊢ (𝜓 ⊼ 𝜃)    ⇒   ⊢ (𝜑 ⊼ 𝜒)
Syntax	w3nand 32394	The double nand.
wff (𝜑 ⊼ 𝜓 ⊼ 𝜒)
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.)
⊢ ((𝜑 ⊼ 𝜓 ⊼ 𝜒) ↔ (𝜑 → (𝜓 → ¬ 𝜒)))
Theorem	df3nandALT1 32396	The double nand expressed in terms of pure nand. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ ((𝜑 ⊼ 𝜓 ⊼ 𝜒) ↔ (𝜑 ⊼ ((𝜓 ⊼ 𝜒) ⊼ (𝜓 ⊼ 𝜒))))
Theorem	df3nandALT2 32397	The double nand expressed in terms of negation and and not. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ((𝜑 ⊼ 𝜓 ⊼ 𝜒) ↔ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒))
Theorem	andnand1 32398	Double and in terms of double nand. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ⊼ 𝜓 ⊼ 𝜒) ⊼ (𝜑 ⊼ 𝜓 ⊼ 𝜒)))
Theorem	imnand2 32399	An → nand relation. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ ((¬ 𝜑 → 𝜓) ↔ ((𝜑 ⊼ 𝜑) ⊼ (𝜓 ⊼ 𝜓)))
20.10.2  Predicate Calculus
Theorem	allt 32400	For all sets, ⊤ is true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ∀𝑥⊤