Home | Metamath
Proof Explorer Theorem List (p. 338 of 449) | < 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-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44900) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | refssfne 33701* | 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𝐴)))) | ||
Theorem | neibastop1 33702* | 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 33703* | Lemma for neibastop2 33704. (Contributed by Jeff Hankins, 12-Sep-2009.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅})) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥) ∧ 𝑤 ∈ (𝐹‘𝑥))) → ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅) & ⊢ 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅} & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → 𝑥 ∈ 𝑣) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) & ⊢ (𝜑 → 𝑁 ⊆ 𝑋) & ⊢ (𝜑 → 𝑈 ∈ (𝐹‘𝑃)) & ⊢ (𝜑 → 𝑈 ⊆ 𝑁) & ⊢ 𝐺 = (rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω) & ⊢ 𝑆 = {𝑦 ∈ 𝑋 ∣ ∃𝑓 ∈ ∪ ran 𝐺((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅} ⇒ ⊢ (𝜑 → ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁)) | ||
Theorem | neibastop2 33704* | 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 33705* | 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‘𝑗)‘{𝑥}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((𝐹‘𝑥) ∩ 𝒫 𝑛) ≠ ∅}) | ||
Theorem | topmtcl 33706 | 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 33707* | 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 33708* | 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 33709* | 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 33710* | 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 33711* | 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 33712* | 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𝑇))) | ||
Theorem | fgmin 33713 | 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 33714* | The neighborhood filter of a nonempty set is generated by its open supersets. See comments for opnfbas 22444. (Contributed by Jeff Hankins, 3-Sep-2009.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → (𝑋filGen{𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}) = ((nei‘𝐽)‘𝑆)) | ||
Theorem | tailfval 33715* | 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 33716 | 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 33717 | An element of a tail. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ 𝑋 = dom 𝐷 ⇒ ⊢ ((𝐷 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝐶) → (𝐵 ∈ ((tail‘𝐷)‘𝐴) ↔ 𝐴𝐷𝐵)) | ||
Theorem | tailf 33718 | 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 33719 | A tail contains its initial element. (Contributed by Jeff Hankins, 25-Nov-2009.) |
⊢ 𝑋 = dom 𝐷 ⇒ ⊢ ((𝐷 ∈ DirRel ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ ((tail‘𝐷)‘𝐴)) | ||
Theorem | tailfb 33720 | 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 33721* | Lemma for filnet 33725. Change variables. (Contributed by Jeff Hankins, 13-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.) |
⊢ 𝐻 = ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) & ⊢ 𝐷 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ (1st ‘𝑦) ⊆ (1st ‘𝑥))} & ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴𝐷𝐵 ↔ ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) ∧ (1st ‘𝐵) ⊆ (1st ‘𝐴))) | ||
Theorem | filnetlem2 33722* | Lemma for filnet 33725. The field of the direction. (Contributed by Jeff Hankins, 13-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.) |
⊢ 𝐻 = ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) & ⊢ 𝐷 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ (1st ‘𝑦) ⊆ (1st ‘𝑥))} ⇒ ⊢ (( I ↾ 𝐻) ⊆ 𝐷 ∧ 𝐷 ⊆ (𝐻 × 𝐻)) | ||
Theorem | filnetlem3 33723* | Lemma for filnet 33725. (Contributed by Jeff Hankins, 13-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.) |
⊢ 𝐻 = ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) & ⊢ 𝐷 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ (1st ‘𝑦) ⊆ (1st ‘𝑥))} ⇒ ⊢ (𝐻 = ∪ ∪ 𝐷 ∧ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel))) | ||
Theorem | filnetlem4 33724* | Lemma for filnet 33725. (Contributed by Jeff Hankins, 15-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.) |
⊢ 𝐻 = ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) & ⊢ 𝐷 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ (1st ‘𝑦) ⊆ (1st ‘𝑥))} ⇒ ⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)))) | ||
Theorem | filnet 33725* | 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‘𝑑)))) | ||
Theorem | tb-ax1 33726 | 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 33727 | 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 33728 |
The third of three axioms in the Tarski-Bernays axiom system.
This axiom, along with ax-mp 5, tb-ax1 33726, and tb-ax2 33727, 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 33729 | The weak syllogism from Tarski-Bernays'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | re1ax2lem 33730 | Lemma for re1ax2 33731. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒))) | ||
Theorem | re1ax2 33731 | ax-2 7 rederived from the Tarski-Bernays axiom system. Often tb-ax1 33726 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 33732 | Constructor theorem for ⊼. (Contributed by Anthony Hart, 1-Sep-2011.) |
⊢ ((𝜑 → 𝜓) → ((𝜓 ⊼ 𝜒) → (𝜑 ⊼ 𝜒))) | ||
Theorem | naim2 33733 | Constructor theorem for ⊼. (Contributed by Anthony Hart, 1-Sep-2011.) |
⊢ ((𝜑 → 𝜓) → ((𝜒 ⊼ 𝜓) → (𝜒 ⊼ 𝜑))) | ||
Theorem | naim1i 33734 | Constructor rule for ⊼. (Contributed by Anthony Hart, 2-Sep-2011.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜓 ⊼ 𝜒) ⇒ ⊢ (𝜑 ⊼ 𝜒) | ||
Theorem | naim2i 33735 | Constructor rule for ⊼. (Contributed by Anthony Hart, 2-Sep-2011.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 ⊼ 𝜓) ⇒ ⊢ (𝜒 ⊼ 𝜑) | ||
Theorem | naim12i 33736 | Constructor rule for ⊼. (Contributed by Anthony Hart, 2-Sep-2011.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ (𝜓 ⊼ 𝜃) ⇒ ⊢ (𝜑 ⊼ 𝜒) | ||
Theorem | nabi1i 33737 | Constructor rule for ⊼. (Contributed by Anthony Hart, 2-Sep-2011.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜓 ⊼ 𝜒) ⇒ ⊢ (𝜑 ⊼ 𝜒) | ||
Theorem | nabi2i 33738 | Constructor rule for ⊼. (Contributed by Anthony Hart, 2-Sep-2011.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ⊼ 𝜓) ⇒ ⊢ (𝜒 ⊼ 𝜑) | ||
Theorem | nabi12i 33739 | Constructor rule for ⊼. (Contributed by Anthony Hart, 2-Sep-2011.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) & ⊢ (𝜓 ⊼ 𝜃) ⇒ ⊢ (𝜑 ⊼ 𝜒) | ||
Syntax | w3nand 33740 | The double nand. |
wff (𝜑 ⊼ 𝜓 ⊼ 𝜒) | ||
Definition | df-3nand 33741 | 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 33742 | The double nand expressed in terms of pure nand. (Contributed by Anthony Hart, 2-Sep-2011.) |
⊢ ((𝜑 ⊼ 𝜓 ⊼ 𝜒) ↔ (𝜑 ⊼ ((𝜓 ⊼ 𝜒) ⊼ (𝜓 ⊼ 𝜒)))) | ||
Theorem | df3nandALT2 33743 | The double nand expressed in terms of negation and and not. (Contributed by Anthony Hart, 13-Sep-2011.) |
⊢ ((𝜑 ⊼ 𝜓 ⊼ 𝜒) ↔ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒)) | ||
Theorem | andnand1 33744 | Double and in terms of double nand. (Contributed by Anthony Hart, 2-Sep-2011.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ⊼ 𝜓 ⊼ 𝜒) ⊼ (𝜑 ⊼ 𝜓 ⊼ 𝜒))) | ||
Theorem | imnand2 33745 | An → nand relation. (Contributed by Anthony Hart, 2-Sep-2011.) |
⊢ ((¬ 𝜑 → 𝜓) ↔ ((𝜑 ⊼ 𝜑) ⊼ (𝜓 ⊼ 𝜓))) | ||
Theorem | nalfal 33746 | Not all sets hold ⊥ as true. (Contributed by Anthony Hart, 13-Sep-2011.) |
⊢ ¬ ∀𝑥⊥ | ||
Theorem | nexntru 33747 | There does not exist a set such that ⊤ is not true. (Contributed by Anthony Hart, 13-Sep-2011.) |
⊢ ¬ ∃𝑥 ¬ ⊤ | ||
Theorem | nexfal 33748 | There does not exist a set such that ⊥ is true. (Contributed by Anthony Hart, 13-Sep-2011.) |
⊢ ¬ ∃𝑥⊥ | ||
Theorem | neufal 33749 | There does not exist exactly one set such that ⊥ is true. (Contributed by Anthony Hart, 13-Sep-2011.) |
⊢ ¬ ∃!𝑥⊥ | ||
Theorem | neutru 33750 | There does not exist exactly one set such that ⊤ is true. (Contributed by Anthony Hart, 13-Sep-2011.) |
⊢ ¬ ∃!𝑥⊤ | ||
Theorem | nmotru 33751 | There does not exist at most one set such that ⊤ is true. (Contributed by Anthony Hart, 13-Sep-2011.) |
⊢ ¬ ∃*𝑥⊤ | ||
Theorem | mofal 33752 | There exist at most one set such that ⊥ is true. (Contributed by Anthony Hart, 13-Sep-2011.) |
⊢ ∃*𝑥⊥ | ||
Theorem | nrmo 33753 | "At most one" restricted existential quantifier for a statement which is never true. (Contributed by Thierry Arnoux, 27-Nov-2023.) |
⊢ (𝑥 ∈ 𝐴 → ¬ 𝜑) ⇒ ⊢ ∃*𝑥 ∈ 𝐴 𝜑 | ||
Theorem | meran1 33754 | A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011.) |
⊢ (¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) ∨ (¬ (¬ 𝜃 ∨ 𝜑) ∨ (𝜒 ∨ (𝜏 ∨ 𝜑)))) | ||
Theorem | meran2 33755 | A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011.) |
⊢ (¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) ∨ (¬ (¬ 𝜏 ∨ 𝜃) ∨ (𝜒 ∨ (𝜑 ∨ 𝜃)))) | ||
Theorem | meran3 33756 | A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011.) |
⊢ (¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) ∨ (¬ (¬ 𝜒 ∨ 𝜑) ∨ (𝜏 ∨ (𝜃 ∨ 𝜑)))) | ||
Theorem | waj-ax 33757 | 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.) |
⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ (((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))) ⊼ (𝜑 ⊼ (𝜑 ⊼ 𝜓)))) | ||
Theorem | lukshef-ax2 33758 | 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.) |
⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜑)) ⊼ ((𝜃 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))) | ||
Theorem | arg-ax 33759 | 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.) |
⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜒 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))) | ||
Theorem | negsym1 33760 |
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.) |
⊢ (¬ ¬ ⊥ → ¬ 𝜑) | ||
Theorem | imsym1 33761 |
A symmetry with →.
See negsym1 33760 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
⊢ ((𝜓 → (𝜓 → ⊥)) → (𝜓 → 𝜑)) | ||
Theorem | bisym1 33762 |
A symmetry with ↔.
See negsym1 33760 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
⊢ ((𝜓 ↔ (𝜓 ↔ ⊥)) → (𝜓 ↔ 𝜑)) | ||
Theorem | consym1 33763 |
A symmetry with ∧.
See negsym1 33760 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
⊢ ((𝜓 ∧ (𝜓 ∧ ⊥)) → (𝜓 ∧ 𝜑)) | ||
Theorem | dissym1 33764 |
A symmetry with ∨.
See negsym1 33760 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
⊢ ((𝜓 ∨ (𝜓 ∨ ⊥)) → (𝜓 ∨ 𝜑)) | ||
Theorem | nandsym1 33765 |
A symmetry with ⊼.
See negsym1 33760 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
⊢ ((𝜓 ⊼ (𝜓 ⊼ ⊥)) → (𝜓 ⊼ 𝜑)) | ||
Theorem | unisym1 33766 |
A symmetry with ∀.
See negsym1 33760 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
⊢ (∀𝑥∀𝑥⊥ → ∀𝑥𝜑) | ||
Theorem | exisym1 33767 |
A symmetry with ∃.
See negsym1 33760 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) |
⊢ (∃𝑥∃𝑥⊥ → ∃𝑥𝜑) | ||
Theorem | unqsym1 33768 |
A symmetry with ∃!.
See negsym1 33760 for more information. (Contributed by Anthony Hart, 6-Sep-2011.) |
⊢ (∃!𝑥∃!𝑥⊥ → ∃!𝑥𝜑) | ||
Theorem | amosym1 33769 |
A symmetry with ∃*.
See negsym1 33760 for more information. (Contributed by Anthony Hart, 13-Sep-2011.) |
⊢ (∃*𝑥∃*𝑥⊥ → ∃*𝑥𝜑) | ||
Theorem | subsym1 33770 |
A symmetry with [𝑥 / 𝑦].
See negsym1 33760 for more information. (Contributed by Anthony Hart, 11-Sep-2011.) |
⊢ ([𝑦 / 𝑥][𝑦 / 𝑥]⊥ → [𝑦 / 𝑥]𝜑) | ||
Theorem | ontopbas 33771 | An ordinal number is a topological basis. (Contributed by Chen-Pang He, 8-Oct-2015.) |
⊢ (𝐵 ∈ On → 𝐵 ∈ TopBases) | ||
Theorem | onsstopbas 33772 | The class of ordinal numbers is a subclass of the class of topological bases. (Contributed by Chen-Pang He, 8-Oct-2015.) |
⊢ On ⊆ TopBases | ||
Theorem | onpsstopbas 33773 | The class of ordinal numbers is a proper subclass of the class of topological bases. (Contributed by Chen-Pang He, 9-Oct-2015.) |
⊢ On ⊊ TopBases | ||
Theorem | ontgval 33774 | The topology generated from an ordinal number 𝐵 is suc ∪ 𝐵. (Contributed by Chen-Pang He, 10-Oct-2015.) |
⊢ (𝐵 ∈ On → (topGen‘𝐵) = suc ∪ 𝐵) | ||
Theorem | ontgsucval 33775 | The topology generated from a successor ordinal number is itself. (Contributed by Chen-Pang He, 11-Oct-2015.) |
⊢ (𝐴 ∈ On → (topGen‘suc 𝐴) = suc 𝐴) | ||
Theorem | onsuctop 33776 | A successor ordinal number is a topology. (Contributed by Chen-Pang He, 11-Oct-2015.) |
⊢ (𝐴 ∈ On → suc 𝐴 ∈ Top) | ||
Theorem | onsuctopon 33777 | One of the topologies on an ordinal number is its successor. (Contributed by Chen-Pang He, 7-Nov-2015.) |
⊢ (𝐴 ∈ On → suc 𝐴 ∈ (TopOn‘𝐴)) | ||
Theorem | ordtoplem 33778 | Membership of the class of successor ordinals. (Contributed by Chen-Pang He, 1-Nov-2015.) |
⊢ (∪ 𝐴 ∈ On → suc ∪ 𝐴 ∈ 𝑆) ⇒ ⊢ (Ord 𝐴 → (𝐴 ≠ ∪ 𝐴 → 𝐴 ∈ 𝑆)) | ||
Theorem | ordtop 33779 | An ordinal is a topology iff it is not its supremum (union), proven without the Axiom of Regularity. (Contributed by Chen-Pang He, 1-Nov-2015.) |
⊢ (Ord 𝐽 → (𝐽 ∈ Top ↔ 𝐽 ≠ ∪ 𝐽)) | ||
Theorem | onsucconni 33780 | A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015.) |
⊢ 𝐴 ∈ On ⇒ ⊢ suc 𝐴 ∈ Conn | ||
Theorem | onsucconn 33781 | A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015.) |
⊢ (𝐴 ∈ On → suc 𝐴 ∈ Conn) | ||
Theorem | ordtopconn 33782 | An ordinal topology is connected. (Contributed by Chen-Pang He, 1-Nov-2015.) |
⊢ (Ord 𝐽 → (𝐽 ∈ Top ↔ 𝐽 ∈ Conn)) | ||
Theorem | onintopssconn 33783 | An ordinal topology is connected, expressed in constants. (Contributed by Chen-Pang He, 16-Oct-2015.) |
⊢ (On ∩ Top) ⊆ Conn | ||
Theorem | onsuct0 33784 | A successor ordinal number is a T0 space. (Contributed by Chen-Pang He, 8-Nov-2015.) |
⊢ (𝐴 ∈ On → suc 𝐴 ∈ Kol2) | ||
Theorem | ordtopt0 33785 | An ordinal topology is T0. (Contributed by Chen-Pang He, 8-Nov-2015.) |
⊢ (Ord 𝐽 → (𝐽 ∈ Top ↔ 𝐽 ∈ Kol2)) | ||
Theorem | onsucsuccmpi 33786 | The successor of a successor ordinal number is a compact topology, proven without the Axiom of Regularity. (Contributed by Chen-Pang He, 18-Oct-2015.) |
⊢ 𝐴 ∈ On ⇒ ⊢ suc suc 𝐴 ∈ Comp | ||
Theorem | onsucsuccmp 33787 | The successor of a successor ordinal number is a compact topology. (Contributed by Chen-Pang He, 18-Oct-2015.) |
⊢ (𝐴 ∈ On → suc suc 𝐴 ∈ Comp) | ||
Theorem | limsucncmpi 33788 | The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015.) |
⊢ Lim 𝐴 ⇒ ⊢ ¬ suc 𝐴 ∈ Comp | ||
Theorem | limsucncmp 33789 | The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015.) |
⊢ (Lim 𝐴 → ¬ suc 𝐴 ∈ Comp) | ||
Theorem | ordcmp 33790 | An ordinal topology is compact iff the underlying set is its supremum (union) only when the ordinal is 1o. (Contributed by Chen-Pang He, 1-Nov-2015.) |
⊢ (Ord 𝐴 → (𝐴 ∈ Comp ↔ (∪ 𝐴 = ∪ ∪ 𝐴 → 𝐴 = 1o))) | ||
Theorem | ssoninhaus 33791 | The ordinal topologies 1o and 2o are Hausdorff. (Contributed by Chen-Pang He, 10-Nov-2015.) |
⊢ {1o, 2o} ⊆ (On ∩ Haus) | ||
Theorem | onint1 33792 | The ordinal T1 spaces are 1o and 2o, proven without the Axiom of Regularity. (Contributed by Chen-Pang He, 9-Nov-2015.) |
⊢ (On ∩ Fre) = {1o, 2o} | ||
Theorem | oninhaus 33793 | The ordinal Hausdorff spaces are 1o and 2o. (Contributed by Chen-Pang He, 10-Nov-2015.) |
⊢ (On ∩ Haus) = {1o, 2o} | ||
Theorem | fveleq 33794 | Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.) |
⊢ (𝐴 = 𝐵 → ((𝜑 → (𝐹‘𝐴) ∈ 𝑃) ↔ (𝜑 → (𝐹‘𝐵) ∈ 𝑃))) | ||
Theorem | findfvcl 33795* | Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.) |
⊢ (𝜑 → (𝐹‘∅) ∈ 𝑃) & ⊢ (𝑦 ∈ ω → (𝜑 → ((𝐹‘𝑦) ∈ 𝑃 → (𝐹‘suc 𝑦) ∈ 𝑃))) ⇒ ⊢ (𝐴 ∈ ω → (𝜑 → (𝐹‘𝐴) ∈ 𝑃)) | ||
Theorem | findreccl 33796* | Please add description here. (Contributed by Jeff Hoffman, 19-Feb-2008.) |
⊢ (𝑧 ∈ 𝑃 → (𝐺‘𝑧) ∈ 𝑃) ⇒ ⊢ (𝐶 ∈ ω → (𝐴 ∈ 𝑃 → (rec(𝐺, 𝐴)‘𝐶) ∈ 𝑃)) | ||
Theorem | findabrcl 33797* | Please add description here. (Contributed by Jeff Hoffman, 16-Feb-2008.) (Revised by Mario Carneiro, 11-Sep-2015.) |
⊢ (𝑧 ∈ 𝑃 → (𝐺‘𝑧) ∈ 𝑃) ⇒ ⊢ ((𝐶 ∈ ω ∧ 𝐴 ∈ 𝑃) → ((𝑥 ∈ V ↦ (rec(𝐺, 𝐴)‘𝑥))‘𝐶) ∈ 𝑃) | ||
Theorem | nnssi2 33798 | Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
⊢ ℕ ⊆ 𝐷 & ⊢ (𝐵 ∈ ℕ → 𝜑) & ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝜑) → 𝜓) ⇒ ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝜓) | ||
Theorem | nnssi3 33799 | Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
⊢ ℕ ⊆ 𝐷 & ⊢ (𝐶 ∈ ℕ → 𝜑) & ⊢ (((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) ∧ 𝜑) → 𝜓) ⇒ ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝜓) | ||
Theorem | nndivsub 33800 | Please add description here. (Contributed by Jeff Hoffman, 17-Jun-2008.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴 / 𝐶) ∈ ℕ ∧ 𝐴 < 𝐵)) → ((𝐵 / 𝐶) ∈ ℕ ↔ ((𝐵 − 𝐴) / 𝐶) ∈ ℕ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |