 Home Metamath Proof ExplorerTheorem List (p. 330 of 437) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

 Color key: Metamath Proof Explorer (1-28347) Hilbert Space Explorer (28348-29872) Users' Mathboxes (29873-43657)

Theorem List for Metamath Proof Explorer - 32901-33000   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremfinminlem 32901* 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 𝜑 → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦𝑥𝜓) → 𝑥 = 𝑦)))

Theoremgtinf 32902* 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(𝑆, ℝ, < ) < 𝐴)) → ∃𝑧𝑆 𝑧 < 𝐴)

Theoremopnrebl 32903* 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 (,)) ↔ (𝐴 ⊆ ℝ ∧ ∀𝑥𝐴𝑦 ∈ ℝ+ ((𝑥𝑦)(,)(𝑥 + 𝑦)) ⊆ 𝐴))

Theoremopnrebl2 32904* 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 (,)) ↔ (𝐴 ⊆ ℝ ∧ ∀𝑥𝐴𝑦 ∈ ℝ+𝑧 ∈ ℝ+ (𝑧𝑦 ∧ ((𝑥𝑧)(,)(𝑥 + 𝑧)) ⊆ 𝐴)))

Theoremnn0prpwlem 32905* Lemma for nn0prpw 32906. Use strong induction to show that every positive integer has unique prime power divisors. (Contributed by Jeff Hankins, 28-Sep-2013.)
(𝐴 ∈ ℕ → ∀𝑘 ∈ ℕ (𝑘 < 𝐴 → ∃𝑝 ∈ ℙ ∃𝑛 ∈ ℕ ¬ ((𝑝𝑛) ∥ 𝑘 ↔ (𝑝𝑛) ∥ 𝐴)))

Theoremnn0prpw 32906* 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

Theoremtopbnd 32907 Two equivalent expressions for the boundary of a topology. (Contributed by Jeff Hankins, 23-Sep-2009.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝐴𝑋) → (((cls‘𝐽)‘𝐴) ∩ ((cls‘𝐽)‘(𝑋𝐴))) = (((cls‘𝐽)‘𝐴) ∖ ((int‘𝐽)‘𝐴)))

Theoremopnbnd 32908 A set is open iff it is disjoint from its boundary. (Contributed by Jeff Hankins, 23-Sep-2009.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝐴𝑋) → (𝐴𝐽 ↔ (𝐴 ∩ (((cls‘𝐽)‘𝐴) ∩ ((cls‘𝐽)‘(𝑋𝐴)))) = ∅))

Theoremcldbnd 32909 A set is closed iff it contains its boundary. (Contributed by Jeff Hankins, 1-Oct-2009.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝐴𝑋) → (𝐴 ∈ (Clsd‘𝐽) ↔ (((cls‘𝐽)‘𝐴) ∩ ((cls‘𝐽)‘(𝑋𝐴))) ⊆ 𝐴))

Theoremntruni 32910* 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‘𝐽)‘ 𝑂))

Theoremclsun 32911 A pairwise union of closures is the closure of the union. (Contributed by Jeff Hankins, 31-Aug-2009.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝑋) → ((cls‘𝐽)‘(𝐴𝐵)) = (((cls‘𝐽)‘𝐴) ∪ ((cls‘𝐽)‘𝐵)))

Theoremclsint2 32912* The closure of an intersection is a subset of the intersection of the closures. (Contributed by Jeff Hankins, 31-Aug-2009.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝐶 ⊆ 𝒫 𝑋) → ((cls‘𝐽)‘ 𝐶) ⊆ 𝑐𝐶 ((cls‘𝐽)‘𝑐))

Theoremopnregcld 32913* 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‘𝐽)‘𝑜)))

Theoremcldregopn 32914* 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‘𝐽)‘𝑐)))

Theoremneiin 32915 Two neighborhoods intersect to form a neighborhood of the intersection. (Contributed by Jeff Hankins, 31-Aug-2009.)
((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → (𝑀𝑁) ∈ ((nei‘𝐽)‘(𝐴𝐵)))

Theoremhmeoclda 32916 Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009.) (Revised by Mario Carneiro, 3-Jun-2014.)
(((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ (𝐽Homeo𝐾)) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝐹𝑆) ∈ (Clsd‘𝐾))

Theoremhmeocldb 32917 Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009.)
(((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ (𝐽Homeo𝐾)) ∧ 𝑆 ∈ (Clsd‘𝐾)) → (𝐹𝑆) ∈ (Clsd‘𝐽))

20.9.3  Topology of the real numbers

TheoremivthALT 32918* An alternate proof of the Intermediate Value Theorem ivth 23658 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

Syntaxcfne 32919 Extend class definition to include the "finer than" relation.
class Fne

Definitiondf-fne 32920* Define the fineness relation for covers. (Contributed by Jeff Hankins, 28-Sep-2009.)
Fne = {⟨𝑥, 𝑦⟩ ∣ ( 𝑥 = 𝑦 ∧ ∀𝑧𝑥 𝑧 (𝑦 ∩ 𝒫 𝑧))}

Theoremfnerel 32921 Fineness is a relation. (Contributed by Jeff Hankins, 28-Sep-2009.)
Rel Fne

Theoremisfne 32922* 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𝐵 ↔ (𝑋 = 𝑌 ∧ ∀𝑥𝐴 𝑥 (𝐵 ∩ 𝒫 𝑥))))

Theoremisfne4 32923 The predicate "𝐵 is finer than 𝐴 " in terms of the topology generation function. (Contributed by Mario Carneiro, 11-Sep-2015.)
𝑋 = 𝐴    &   𝑌 = 𝐵       (𝐴Fne𝐵 ↔ (𝑋 = 𝑌𝐴 ⊆ (topGen‘𝐵)))

Theoremisfne4b 32924 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‘𝐵))))

Theoremisfne2 32925* The predicate "𝐵 is finer than 𝐴". (Contributed by Jeff Hankins, 28-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
𝑋 = 𝐴    &   𝑌 = 𝐵       (𝐵𝐶 → (𝐴Fne𝐵 ↔ (𝑋 = 𝑌 ∧ ∀𝑥𝐴𝑦𝑥𝑧𝐵 (𝑦𝑧𝑧𝑥))))

Theoremisfne3 32926* The predicate "𝐵 is finer than 𝐴". (Contributed by Jeff Hankins, 11-Oct-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
𝑋 = 𝐴    &   𝑌 = 𝐵       (𝐵𝐶 → (𝐴Fne𝐵 ↔ (𝑋 = 𝑌 ∧ ∀𝑥𝐴𝑦(𝑦𝐵𝑥 = 𝑦))))

Theoremfnebas 32927 A finer cover covers the same set as the original. (Contributed by Jeff Hankins, 28-Sep-2009.)
𝑋 = 𝐴    &   𝑌 = 𝐵       (𝐴Fne𝐵𝑋 = 𝑌)

Theoremfnetg 32928 A finer cover generates a topology finer than the original set. (Contributed by Mario Carneiro, 11-Sep-2015.)
(𝐴Fne𝐵𝐴 ⊆ (topGen‘𝐵))

Theoremfnessex 32929* 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𝐵𝑆𝐴𝑃𝑆) → ∃𝑥𝐵 (𝑃𝑥𝑥𝑆))

Theoremfneuni 32930* If 𝐵 is finer than 𝐴, every element of 𝐴 is a union of elements of 𝐵. (Contributed by Jeff Hankins, 11-Oct-2009.)
((𝐴Fne𝐵𝑆𝐴) → ∃𝑥(𝑥𝐵𝑆 = 𝑥))

Theoremfneint 32931* If a cover is finer than another, every point can be approached more closely by intersections. (Contributed by Jeff Hankins, 11-Oct-2009.)
(𝐴Fne𝐵 {𝑥𝐵𝑃𝑥} ⊆ {𝑥𝐴𝑃𝑥})

Theoremfness 32932 A cover is finer than its subcovers. (Contributed by Jeff Hankins, 11-Oct-2009.)
𝑋 = 𝐴    &   𝑌 = 𝐵       ((𝐵𝐶𝐴𝐵𝑋 = 𝑌) → 𝐴Fne𝐵)

Theoremfneref 32933 Reflexivity of the fineness relation. (Contributed by Jeff Hankins, 12-Oct-2009.)
(𝐴𝑉𝐴Fne𝐴)

Theoremfnetr 32934 Transitivity of the fineness relation. (Contributed by Jeff Hankins, 5-Oct-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
((𝐴Fne𝐵𝐵Fne𝐶) → 𝐴Fne𝐶)

Theoremfneval 32935 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‘𝐵)))

Theoremfneer 32936 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

Theoremtopfne 32937 Fineness for covers corresponds precisely with fineness for topologies. (Contributed by Jeff Hankins, 29-Sep-2009.)
𝑋 = 𝐽    &   𝑌 = 𝐾       ((𝐾 ∈ Top ∧ 𝑋 = 𝑌) → (𝐽𝐾𝐽Fne𝐾))

Theoremtopfneec 32938 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‘𝐴) = 𝐽))

Theoremtopfneec2 32939 A topology is precisely identified with its equivalence class. (Contributed by Jeff Hankins, 12-Oct-2009.)
= (Fne ∩ Fne)       ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → ([𝐽] = [𝐾] 𝐽 = 𝐾))

Theoremfnessref 32940* 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𝐴))))

Theoremrefssfne 32941* 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

Theoremneibastop1 32942* 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‘𝑋))

Theoremneibastop2lem 32943* Lemma for neibastop2 32944. (Contributed by Jeff Hankins, 12-Sep-2009.)
(𝜑𝑋𝑉)    &   (𝜑𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))    &   ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥) ∧ 𝑤 ∈ (𝐹𝑥))) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ≠ ∅)    &   𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅}    &   ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥))) → 𝑥𝑣)    &   ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥))) → ∃𝑡 ∈ (𝐹𝑥)∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)    &   (𝜑𝑃𝑋)    &   (𝜑𝑁𝑋)    &   (𝜑𝑈 ∈ (𝐹𝑃))    &   (𝜑𝑈𝑁)    &   𝐺 = (rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)    &   𝑆 = {𝑦𝑋 ∣ ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅}       (𝜑 → ∃𝑢𝐽 (𝑃𝑢𝑢𝑁))

Theoremneibastop2 32944* 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‘𝐽)‘{𝑃}) ↔ (𝑁𝑋 ∧ ((𝐹𝑃) ∩ 𝒫 𝑁) ≠ ∅)))

Theoremneibastop3 32945* 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

Theoremtopmtcl 32946 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‘𝑋))

Theoremtopmeet 32947* 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‘𝑋) ∣ ∀𝑗𝑆 𝑘𝑗})

Theoremtopjoin 32948* 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‘𝑋) ∣ ∀𝑗𝑆 𝑗𝑘})

Theoremfnemeet1 32949* 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𝐴)

Theoremfnemeet2 32950* 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𝑥)))

Theoremfnejoin1 32951* 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(𝑆 = ∅, {𝑋}, 𝑆))

Theoremfnejoin2 32952* 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

Theoremfgmin 32953 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𝐵) ⊆ 𝐹))

Theoremneifg 32954* The neighborhood filter of a nonempty set is generated by its open supersets. See comments for opnfbas 22054. (Contributed by Jeff Hankins, 3-Sep-2009.)
𝑋 = 𝐽       ((𝐽 ∈ Top ∧ 𝑆𝑋𝑆 ≠ ∅) → (𝑋filGen{𝑥𝐽𝑆𝑥}) = ((nei‘𝐽)‘𝑆))

20.9.8  Directed sets, nets

Theoremtailfval 32955* The tail function for a directed set. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 24-Nov-2013.)
𝑋 = dom 𝐷       (𝐷 ∈ DirRel → (tail‘𝐷) = (𝑥𝑋 ↦ (𝐷 “ {𝑥})))

Theoremtailval 32956 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‘𝐷)‘𝐴) = (𝐷 “ {𝐴}))

Theoremeltail 32957 An element of a tail. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 24-Nov-2013.)
𝑋 = dom 𝐷       ((𝐷 ∈ DirRel ∧ 𝐴𝑋𝐵𝐶) → (𝐵 ∈ ((tail‘𝐷)‘𝐴) ↔ 𝐴𝐷𝐵))

Theoremtailf 32958 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‘𝐷):𝑋⟶𝒫 𝑋)

Theoremtailini 32959 A tail contains its initial element. (Contributed by Jeff Hankins, 25-Nov-2009.)
𝑋 = dom 𝐷       ((𝐷 ∈ DirRel ∧ 𝐴𝑋) → 𝐴 ∈ ((tail‘𝐷)‘𝐴))

Theoremtailfb 32960 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‘𝑋))

Theoremfilnetlem1 32961* Lemma for filnet 32965. Change variables. (Contributed by Jeff Hankins, 13-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.)
𝐻 = 𝑛𝐹 ({𝑛} × 𝑛)    &   𝐷 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐻𝑦𝐻) ∧ (1st𝑦) ⊆ (1st𝑥))}    &   𝐴 ∈ V    &   𝐵 ∈ V       (𝐴𝐷𝐵 ↔ ((𝐴𝐻𝐵𝐻) ∧ (1st𝐵) ⊆ (1st𝐴)))

Theoremfilnetlem2 32962* Lemma for filnet 32965. The field of the direction. (Contributed by Jeff Hankins, 13-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.)
𝐻 = 𝑛𝐹 ({𝑛} × 𝑛)    &   𝐷 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐻𝑦𝐻) ∧ (1st𝑦) ⊆ (1st𝑥))}       (( I ↾ 𝐻) ⊆ 𝐷𝐷 ⊆ (𝐻 × 𝐻))

Theoremfilnetlem3 32963* Lemma for filnet 32965. (Contributed by Jeff Hankins, 13-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.)
𝐻 = 𝑛𝐹 ({𝑛} × 𝑛)    &   𝐷 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐻𝑦𝐻) ∧ (1st𝑦) ⊆ (1st𝑥))}       (𝐻 = 𝐷 ∧ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel)))

Theoremfilnetlem4 32964* Lemma for filnet 32965. (Contributed by Jeff Hankins, 15-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.)
𝐻 = 𝑛𝐹 ({𝑛} × 𝑛)    &   𝐷 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐻𝑦𝐻) ∧ (1st𝑦) ⊆ (1st𝑥))}       (𝐹 ∈ (Fil‘𝑋) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))

Theoremfilnet 32965* 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

Theoremtb-ax1 32966 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.)
((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒)))

Theoremtb-ax2 32967 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.)
(𝜑 → (𝜓𝜑))

Theoremtb-ax3 32968 The third of three axioms in the Tarski-Bernays axiom system.

This axiom, along with ax-mp 5, tb-ax1 32966, and tb-ax2 32967, 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.)

(((𝜑𝜓) → 𝜑) → 𝜑)

Theoremtbsyl 32969 The weak syllogism from Tarski-Bernays'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝜑𝜓)    &   (𝜓𝜒)       (𝜑𝜒)

Theoremre1ax2lem 32970 Lemma for re1ax2 32971. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
((𝜑 → (𝜓𝜒)) → (𝜓 → (𝜑𝜒)))

Theoremre1ax2 32971 ax-2 7 rederived from the Tarski-Bernays axiom system. Often tb-ax1 32966 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.)
((𝜑 → (𝜓𝜒)) → ((𝜑𝜓) → (𝜑𝜒)))

Theoremnaim1 32972 Constructor theorem for . (Contributed by Anthony Hart, 1-Sep-2011.)
((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒)))

Theoremnaim2 32973 Constructor theorem for . (Contributed by Anthony Hart, 1-Sep-2011.)
((𝜑𝜓) → ((𝜒𝜓) → (𝜒𝜑)))

Theoremnaim1i 32974 Constructor rule for . (Contributed by Anthony Hart, 2-Sep-2011.)
(𝜑𝜓)    &   (𝜓𝜒)       (𝜑𝜒)

Theoremnaim2i 32975 Constructor rule for . (Contributed by Anthony Hart, 2-Sep-2011.)
(𝜑𝜓)    &   (𝜒𝜓)       (𝜒𝜑)

Theoremnaim12i 32976 Constructor rule for . (Contributed by Anthony Hart, 2-Sep-2011.)
(𝜑𝜓)    &   (𝜒𝜃)    &   (𝜓𝜃)       (𝜑𝜒)

Theoremnabi1i 32977 Constructor rule for . (Contributed by Anthony Hart, 2-Sep-2011.)
(𝜑𝜓)    &   (𝜓𝜒)       (𝜑𝜒)

Theoremnabi2i 32978 Constructor rule for . (Contributed by Anthony Hart, 2-Sep-2011.)
(𝜑𝜓)    &   (𝜒𝜓)       (𝜒𝜑)

Theoremnabi12i 32979 Constructor rule for . (Contributed by Anthony Hart, 2-Sep-2011.)
(𝜑𝜓)    &   (𝜒𝜃)    &   (𝜓𝜃)       (𝜑𝜒)

Syntaxw3nand 32980 The double nand.
wff (𝜑𝜓𝜒)

Definitiondf-3nand 32981 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.)
((𝜑𝜓𝜒) ↔ (𝜑 → (𝜓 → ¬ 𝜒)))

Theoremdf3nandALT1 32982 The double nand expressed in terms of pure nand. (Contributed by Anthony Hart, 2-Sep-2011.)
((𝜑𝜓𝜒) ↔ (𝜑 ⊼ ((𝜓𝜒) ⊼ (𝜓𝜒))))

Theoremdf3nandALT2 32983 The double nand expressed in terms of negation and and not. (Contributed by Anthony Hart, 13-Sep-2011.)
((𝜑𝜓𝜒) ↔ ¬ (𝜑𝜓𝜒))

Theoremandnand1 32984 Double and in terms of double nand. (Contributed by Anthony Hart, 2-Sep-2011.)
((𝜑𝜓𝜒) ↔ ((𝜑𝜓𝜒) ⊼ (𝜑𝜓𝜒)))

Theoremimnand2 32985 An nand relation. (Contributed by Anthony Hart, 2-Sep-2011.)
((¬ 𝜑𝜓) ↔ ((𝜑𝜑) ⊼ (𝜓𝜓)))

20.10.2  Predicate Calculus

Theoremnalfal 32986 Not all sets hold as true. (Contributed by Anthony Hart, 13-Sep-2011.)
¬ ∀𝑥

Theoremnexntru 32987 There does not exist a set such that is not true. (Contributed by Anthony Hart, 13-Sep-2011.)
¬ ∃𝑥 ¬ ⊤

Theoremnexfal 32988 There does not exist a set such that is true. (Contributed by Anthony Hart, 13-Sep-2011.)
¬ ∃𝑥

Theoremneufal 32989 There does not exist exactly one set such that is true. (Contributed by Anthony Hart, 13-Sep-2011.)
¬ ∃!𝑥

Theoremneutru 32990 There does not exist exactly one set such that is true. (Contributed by Anthony Hart, 13-Sep-2011.)
¬ ∃!𝑥

Theoremnmotru 32991 There does not exist at most one set such that is true. (Contributed by Anthony Hart, 13-Sep-2011.)
¬ ∃*𝑥

Theoremmofal 32992 There exist at most one set such that is true. (Contributed by Anthony Hart, 13-Sep-2011.)
∃*𝑥

20.10.3  Miscellaneous single axioms

Theoremmeran1 32993 A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011.)
(¬ (¬ (¬ 𝜑𝜓) ∨ (𝜒 ∨ (𝜃𝜏))) ∨ (¬ (¬ 𝜃𝜑) ∨ (𝜒 ∨ (𝜏𝜑))))

Theoremmeran2 32994 A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011.)
(¬ (¬ (¬ 𝜑𝜓) ∨ (𝜒 ∨ (𝜃𝜏))) ∨ (¬ (¬ 𝜏𝜃) ∨ (𝜒 ∨ (𝜑𝜃))))

Theoremmeran3 32995 A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011.)
(¬ (¬ (¬ 𝜑𝜓) ∨ (𝜒 ∨ (𝜃𝜏))) ∨ (¬ (¬ 𝜒𝜑) ∨ (𝜏 ∨ (𝜃𝜑))))

Theoremwaj-ax 32996 A single axiom for propositional calculus discovered by Mordchaj Wajsberg (Logical Works, Polish Academy of Sciences, 1977). See: Fitelson, Some recent results in algebra and logical calculi obtained using automated reasoning, 2003 (axiom W on slide 8). (Contributed by Anthony Hart, 13-Aug-2011.)
((𝜑 ⊼ (𝜓𝜒)) ⊼ (((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃))) ⊼ (𝜑 ⊼ (𝜑𝜓))))

Theoremlukshef-ax2 32997 A single axiom for propositional calculus discovered by Jan Lukasiewicz. See: Fitelson, Some recent results in algebra and logical calculi obtained using automated reasoning, 2003 (axiom L2 on slide 8). (Contributed by Anthony Hart, 14-Aug-2011.)
((𝜑 ⊼ (𝜓𝜒)) ⊼ ((𝜑 ⊼ (𝜒𝜑)) ⊼ ((𝜃𝜓) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃)))))

Theoremarg-ax 32998 A single axiom for propositional calculus discovered by Ken Harris and Branden Fitelson. See: Fitelson, Some recent results in algebra and logical calculi obtained using automated reasoning, 2003 (axiom HF1 on slide 8). (Contributed by Anthony Hart, 14-Aug-2011.)
((𝜑 ⊼ (𝜓𝜒)) ⊼ ((𝜑 ⊼ (𝜓𝜒)) ⊼ ((𝜃𝜒) ⊼ ((𝜒𝜃) ⊼ (𝜑𝜃)))))

20.10.4  Connective Symmetry

Theoremnegsym1 32999 In the paper "On Variable Functors of Propositional Arguments", Lukasiewicz introduced a system that can handle variable connectives. This was done by introducing a variable, marked with a lowercase delta, which takes a wff as input. In the system, "delta 𝜑 " means that "something is true of 𝜑". The expression "delta 𝜑 " can be substituted with ¬ 𝜑, 𝜓𝜑, 𝑥𝜑, etc.

Later on, Meredith discovered a single axiom, in the form of ( delta delta ⊥ → delta 𝜑 ). This represents the shortest theorem in the extended propositional calculus that cannot be derived as an instance of a theorem in propositional calculus.

A symmetry with ¬. (Contributed by Anthony Hart, 4-Sep-2011.)

(¬ ¬ ⊥ → ¬ 𝜑)

Theoremimsym1 33000 A symmetry with .