Home | Metamath
Proof Explorer Theorem List (p. 360 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
We are sad to report the passing of Metamath creator and long-time contributor Norm Megill (1950 - 2021). Norm of course was the author of the Metamath proof language, the specification, all of the early tools (and some of the later ones), and the foundational work in logic and set theory for set.mm. His tools, now at https://github.com/metamath/metamath-exe , include a proof verifier, a proof assistant, a proof minimizer, style checking and reformatting, and tools for searching and displaying proofs. One of his key insights was that formal proofs can exist not only to be verified by computers, but also to be read by humans. Both the specification of the proof format (which stores full proofs, as opposed to the proof templates used by most proof assistants) and the generated web display of Metamath proofs, one of its distinctive features, contribute to this double objective. Metamath innovated both by using a very simple substitution rule (and then using that to build more complicated notions like free and bound variables) and also by taking the axiom schemas found in many theories and taking them to the next level - by making all axioms, theorems and proofs operate in terms of schemas. Not content to create Metamath for his own amusement, he also published it for the world and encouraged the development of a community of people who contributed to it and created their own tools. He was an active participant in the Metamath mailing list and other forums until days before his passing. It is often our custom to supply a quote from someone memorialized in a mathbox entry. And it is difficult to select a quote for someone who has written so much about Metamath over the years. But here is one quote from the Metamath web page which illustrates not just his clear thinking about what Metamath can and cannot do but also his desire to encourage students at all levels: Q: Will Metamath help me learn abstract mathematics? A: Yes, but probably not by itself. In order to follow a proof in an advanced math textbook, you may need to know prerequisites that could take years to learn. Some people find this frustrating. In contrast, Metamath uses a single, simple substitution rule that allows you to follow any proof mechanically. You can actually jump in anywhere and be convinced that the symbol string you see in a proof step is a consequence of the symbol strings in the earlier steps that it references, even if you don't understand what the symbols mean. But this is quite different from understanding the meaning of the math that results. Metamath alone probably will not give you an intuitive feel for abstract math, in the same way it can be hard to grasp a large computer program just by reading its source code, even though you may understand each individual instruction. However, the Bibliographic Cross-Reference lets you compare informal proofs in math textbooks and see all the implicit missing details "left to the reader." | ||
These older axiom schemes are obsolete and should not be used outside of this section. They are proved above as theorems axc4 , sp 2172, axc7 2328, axc10 2396, axc11 2447, axc11n 2443, axc15 2438, axc9 2393, axc14 2481, and axc16 2253. | ||
Axiom | ax-c5 35901 |
Axiom of Specialization. A quantified wff implies the wff without a
quantifier (i.e. an instance, or special case, of the generalized wff).
In other words if something is true for all 𝑥, it is true for any
specific 𝑥 (that would typically occur as a free
variable in the wff
substituted for 𝜑). (A free variable is one that does
not occur in
the scope of a quantifier: 𝑥 and 𝑦 are both free in 𝑥 = 𝑦,
but only 𝑥 is free in ∀𝑦𝑥 = 𝑦.) Axiom scheme C5' in [Megill]
p. 448 (p. 16 of the preprint). Also appears as Axiom B5 of [Tarski]
p. 67 (under his system S2, defined in the last paragraph on p. 77).
Note that the converse of this axiom does not hold in general, but a weaker inference form of the converse holds and is expressed as rule ax-gen 1787. Conditional forms of the converse are given by ax-13 2383, ax-c14 35909, ax-c16 35910, and ax-5 1902. Unlike the more general textbook Axiom of Specialization, we cannot choose a variable different from 𝑥 for the special case. For use, that requires the assistance of equality axioms, and we deal with it later after we introduce the definition of proper substitution - see stdpc4 2064. An interesting alternate axiomatization uses axc5c711 35936 and ax-c4 35902 in place of ax-c5 35901, ax-4 1801, ax-10 2136, and ax-11 2151. This axiom is obsolete and should no longer be used. It is proved above as theorem sp 2172. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Axiom | ax-c4 35902 |
Axiom of Quantified Implication. This axiom moves a quantifier from
outside to inside an implication, quantifying 𝜓. Notice that 𝑥
must not be a free variable in the antecedent of the quantified
implication, and we express this by binding 𝜑 to "protect" the
axiom
from a 𝜑 containing a free 𝑥. Axiom
scheme C4' in [Megill]
p. 448 (p. 16 of the preprint). It is a special case of Lemma 5 of
[Monk2] p. 108 and Axiom 5 of [Mendelson] p. 69.
This axiom is obsolete and should no longer be used. It is proved above as theorem axc4 2332. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.) |
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) | ||
Axiom | ax-c7 35903 |
Axiom of Quantified Negation. This axiom is used to manipulate negated
quantifiers. Equivalent to axiom scheme C7' in [Megill] p. 448 (p. 16 of
the preprint). An alternate axiomatization could use axc5c711 35936 in place
of ax-c5 35901, ax-c7 35903, and ax-11 2151.
This axiom is obsolete and should no longer be used. It is proved above as theorem axc7 2328. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
Axiom | ax-c10 35904 |
A variant of ax6 2395. Axiom scheme C10' in [Megill] p. 448 (p. 16 of the
preprint).
This axiom is obsolete and should no longer be used. It is proved above as theorem axc10 2396. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑) | ||
Axiom | ax-c11 35905 |
Axiom ax-c11 35905 was the original version of ax-c11n 35906 ("n" for "new"),
before it was discovered (in May 2008) that the shorter ax-c11n 35906 could
replace it. It appears as Axiom scheme C11' in [Megill] p. 448 (p. 16 of
the preprint).
This axiom is obsolete and should no longer be used. It is proved above as theorem axc11 2447. (Contributed by NM, 10-May-1993.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Axiom | ax-c11n 35906 |
Axiom of Quantifier Substitution. One of the equality and substitution
axioms of predicate calculus with equality. Appears as Lemma L12 in
[Megill] p. 445 (p. 12 of the preprint).
The original version of this axiom was ax-c11 35905 and was replaced with this shorter ax-c11n 35906 ("n" for "new") in May 2008. The old axiom is proved from this one as theorem axc11 2447. Conversely, this axiom is proved from ax-c11 35905 as theorem axc11nfromc11 35944. This axiom was proved redundant in July 2015. See theorem axc11n 2443. This axiom is obsolete and should no longer be used. It is proved above as theorem axc11n 2443. (Contributed by NM, 16-May-2008.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Axiom | ax-c15 35907 |
Axiom ax-c15 35907 was the original version of ax-12 2167, before it was
discovered (in Jan. 2007) that the shorter ax-12 2167 could replace it. It
appears as Axiom scheme C15' in [Megill]
p. 448 (p. 16 of the preprint).
It is based on Lemma 16 of [Tarski] p. 70
and Axiom C8 of [Monk2] p. 105,
from which it can be proved by cases. To understand this theorem more
easily, think of "¬ ∀𝑥𝑥 = 𝑦 →..." as informally meaning
"if
𝑥 and 𝑦 are distinct variables
then..." The antecedent becomes
false if the same variable is substituted for 𝑥 and 𝑦,
ensuring
the theorem is sound whenever this is the case. In some later theorems,
we call an antecedent of the form ¬ ∀𝑥𝑥 = 𝑦 a "distinctor."
Interestingly, if the wff expression substituted for 𝜑 contains no wff variables, the resulting statement can be proved without invoking this axiom. This means that even though this axiom is metalogically independent from the others, it is not logically independent. Specifically, we can prove any wff-variable-free instance of axiom ax-c15 35907 (from which the ax-12 2167 instance follows by theorem ax12 2440.) The proof is by induction on formula length, using ax12eq 35959 and ax12el 35960 for the basis steps and ax12indn 35961, ax12indi 35962, and ax12inda 35966 for the induction steps. (This paragraph is true provided we use ax-c11 35905 in place of ax-c11n 35906.) This axiom is obsolete and should no longer be used. It is proved above as theorem axc15 2438, which should be used instead. (Contributed by NM, 14-May-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Axiom | ax-c9 35908 |
Axiom of Quantifier Introduction. One of the equality and substitution
axioms of predicate calculus with equality. Informally, it says that
whenever 𝑧 is distinct from 𝑥 and
𝑦,
and 𝑥 =
𝑦 is true,
then 𝑥 = 𝑦 quantified with 𝑧 is also
true. In other words, 𝑧
is irrelevant to the truth of 𝑥 = 𝑦. Axiom scheme C9' in [Megill]
p. 448 (p. 16 of the preprint). It apparently does not otherwise appear
in the literature but is easily proved from textbook predicate calculus by
cases.
This axiom is obsolete and should no longer be used. It is proved above as theorem axc9 2393. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) | ||
Axiom | ax-c14 35909 |
Axiom of Quantifier Introduction. One of the equality and substitution
axioms for a non-logical predicate in our predicate calculus with
equality. Axiom scheme C14' in [Megill]
p. 448 (p. 16 of the preprint).
It is redundant if we include ax-5 1902; see theorem axc14 2481. Alternately,
ax-5 1902 becomes unnecessary in principle with this
axiom, but we lose the
more powerful metalogic afforded by ax-5 1902.
We retain ax-c14 35909 here to
provide completeness for systems with the simpler metalogic that results
from omitting ax-5 1902, which might be easier to study for some
theoretical
purposes.
This axiom is obsolete and should no longer be used. It is proved above as theorem axc14 2481. (Contributed by NM, 24-Jun-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦))) | ||
Axiom | ax-c16 35910* |
Axiom of Distinct Variables. The only axiom of predicate calculus
requiring that variables be distinct (if we consider ax-5 1902
to be a
metatheorem and not an axiom). Axiom scheme C16' in [Megill] p. 448 (p.
16 of the preprint). It apparently does not otherwise appear in the
literature but is easily proved from textbook predicate calculus by
cases. It is a somewhat bizarre axiom since the antecedent is always
false in set theory (see dtru 5263), but nonetheless it is technically
necessary as you can see from its uses.
This axiom is redundant if we include ax-5 1902; see theorem axc16 2253. Alternately, ax-5 1902 becomes logically redundant in the presence of this axiom, but without ax-5 1902 we lose the more powerful metalogic that results from being able to express the concept of a setvar variable not occurring in a wff (as opposed to just two setvar variables being distinct). We retain ax-c16 35910 here to provide logical completeness for systems with the simpler metalogic that results from omitting ax-5 1902, which might be easier to study for some theoretical purposes. This axiom is obsolete and should no longer be used. It is proved above as theorem axc16 2253. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorems ax12fromc15 35923 and ax13fromc9 35924 require some intermediate theorems that are included in this section. | ||
Theorem | axc5 35911 | This theorem repeats sp 2172 under the name axc5 35911, so that the Metamath program "MM> VERIFY MARKUP" command will check that it matches axiom scheme ax-c5 35901. (Contributed by NM, 18-Aug-2017.) (Proof modification is discouraged.) Use sp 2172 instead. (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | ax4fromc4 35912 | Rederivation of axiom ax-4 1801 from ax-c4 35902, ax-c5 35901, ax-gen 1787 and minimal implicational calculus { ax-mp 5, ax-1 6, ax-2 7 }. See axc4 2332 for the derivation of ax-c4 35902 from ax-4 1801. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) Use ax-4 1801 instead. (New usage is discouraged.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) | ||
Theorem | ax10fromc7 35913 | Rederivation of axiom ax-10 2136 from ax-c7 35903, ax-c4 35902, ax-c5 35901, ax-gen 1787 and propositional calculus. See axc7 2328 for the derivation of ax-c7 35903 from ax-10 2136. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) Use ax-10 2136 instead. (New usage is discouraged.) |
⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑) | ||
Theorem | ax6fromc10 35914 | Rederivation of axiom ax-6 1961 from ax-c7 35903, ax-c10 35904, ax-gen 1787 and propositional calculus. See axc10 2396 for the derivation of ax-c10 35904 from ax-6 1961. Lemma L18 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) Use ax-6 1961 instead. (New usage is discouraged.) |
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 | ||
Theorem | hba1-o 35915 | The setvar 𝑥 is not free in ∀𝑥𝜑. Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114. (Contributed by NM, 24-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) | ||
Theorem | axc4i-o 35916 | Inference version of ax-c4 35902. (Contributed by NM, 3-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) | ||
Theorem | equid1 35917 | Proof of equid 2010 from our older axioms. This is often an axiom of equality in textbook systems, but we don't need it as an axiom since it can be proved from our other axioms (although the proof, as you can see below, is not as obvious as you might think). This proof uses only axioms without distinct variable conditions and requires no dummy variables. A simpler proof, similar to Tarski's, is possible if we make use of ax-5 1902; see the proof of equid 2010. See equid1ALT 35943 for an alternate proof. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑥 = 𝑥 | ||
Theorem | equcomi1 35918 | Proof of equcomi 2015 from equid1 35917, avoiding use of ax-5 1902 (the only use of ax-5 1902 is via ax7 2014, so using ax-7 2006 instead would remove dependency on ax-5 1902). (Contributed by BJ, 8-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) | ||
Theorem | aecom-o 35919 | Commutation law for identical variable specifiers. The antecedent and consequent are true when 𝑥 and 𝑦 are substituted with the same variable. Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). Version of aecom 2444 using ax-c11 35905. Unlike axc11nfromc11 35944, this version does not require ax-5 1902 (see comment of equcomi1 35918). (Contributed by NM, 10-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Theorem | aecoms-o 35920 | A commutation rule for identical variable specifiers. Version of aecoms 2445 using ax-c11 35905. (Contributed by NM, 10-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | hbae-o 35921 | All variables are effectively bound in an identical variable specifier. Version of hbae 2448 using ax-c11 35905. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦) | ||
Theorem | dral1-o 35922 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Version of dral1 2456 using ax-c11 35905. (Contributed by NM, 24-Nov-1994.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
Theorem | ax12fromc15 35923 |
Rederivation of axiom ax-12 2167 from ax-c15 35907, ax-c11 35905 (used through
dral1-o 35922), and other older axioms. See theorem axc15 2438 for the
derivation of ax-c15 35907 from ax-12 2167.
An open problem is whether we can prove this using ax-c11n 35906 instead of ax-c11 35905. This proof uses newer axioms ax-4 1801 and ax-6 1961, but since these are proved from the older axioms above, this is acceptable and lets us avoid having to reprove several earlier theorems to use ax-c4 35902 and ax-c10 35904. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | ax13fromc9 35924 |
Derive ax-13 2383 from ax-c9 35908 and other older axioms.
This proof uses newer axioms ax-4 1801 and ax-6 1961, but since these are proved from the older axioms above, this is acceptable and lets us avoid having to reprove several earlier theorems to use ax-c4 35902 and ax-c10 35904. (Contributed by NM, 21-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
These theorems were mostly intended to study properties of the older axiom schemes and are not useful outside of this section. They should not be used outside of this section. They may be deleted when they are deemed to no longer be of interest. | ||
Theorem | ax5ALT 35925* |
Axiom to quantify a variable over a formula in which it does not occur.
Axiom C5 in [Megill] p. 444 (p. 11 of
the preprint). Also appears as
Axiom B6 (p. 75) of system S2 of [Tarski] p. 77 and Axiom C5-1 of
[Monk2] p. 113.
(This theorem simply repeats ax-5 1902 so that we can include the following note, which applies only to the obsolete axiomatization.) This axiom is logically redundant in the (logically complete) predicate calculus axiom system consisting of ax-gen 1787, ax-c4 35902, ax-c5 35901, ax-11 2151, ax-c7 35903, ax-7 2006, ax-c9 35908, ax-c10 35904, ax-c11 35905, ax-8 2107, ax-9 2115, ax-c14 35909, ax-c15 35907, and ax-c16 35910: in that system, we can derive any instance of ax-5 1902 not containing wff variables by induction on formula length, using ax5eq 35950 and ax5el 35955 for the basis together with hbn 2295, hbal 2164, and hbim 2299. However, if we omit this axiom, our development would be quite inconvenient since we could work only with specific instances of wffs containing no wff variables - this axiom introduces the concept of a setvar variable not occurring in a wff (as opposed to just two setvar variables being distinct). (Contributed by NM, 19-Aug-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) | ||
Theorem | sps-o 35926 | Generalization of antecedent. (Contributed by NM, 5-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | hbequid 35927 | Bound-variable hypothesis builder for 𝑥 = 𝑥. This theorem tells us that any variable, including 𝑥, is effectively not free in 𝑥 = 𝑥, even though 𝑥 is technically free according to the traditional definition of free variable. (The proof does not use ax-c10 35904.) (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 23-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑥 → ∀𝑦 𝑥 = 𝑥) | ||
Theorem | nfequid-o 35928 | Bound-variable hypothesis builder for 𝑥 = 𝑥. This theorem tells us that any variable, including 𝑥, is effectively not free in 𝑥 = 𝑥, even though 𝑥 is technically free according to the traditional definition of free variable. (The proof uses only ax-4 1801, ax-7 2006, ax-c9 35908, and ax-gen 1787. This shows that this can be proved without ax6 2395, even though the theorem equid 2010 cannot be. A shorter proof using ax6 2395 is obtainable from equid 2010 and hbth 1795.) Remark added 2-Dec-2015 NM: This proof does implicitly use ax6v 1962, which is used for the derivation of axc9 2393, unless we consider ax-c9 35908 the starting axiom rather than ax-13 2383. (Contributed by NM, 13-Jan-2011.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑦 𝑥 = 𝑥 | ||
Theorem | axc5c7 35929 | Proof of a single axiom that can replace ax-c5 35901 and ax-c7 35903. See axc5c7toc5 35930 and axc5c7toc7 35931 for the rederivation of those axioms. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((∀𝑥 ¬ ∀𝑥𝜑 → ∀𝑥𝜑) → 𝜑) | ||
Theorem | axc5c7toc5 35930 | Rederivation of ax-c5 35901 from axc5c7 35929. Only propositional calculus is used for the rederivation. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | axc5c7toc7 35931 | Rederivation of ax-c7 35903 from axc5c7 35929. Only propositional calculus is used for the rederivation. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
Theorem | axc711 35932 | Proof of a single axiom that can replace both ax-c7 35903 and ax-11 2151. See axc711toc7 35934 and axc711to11 35935 for the rederivation of those axioms. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑦∀𝑥𝜑 → ∀𝑦𝜑) | ||
Theorem | nfa1-o 35933 | 𝑥 is not free in ∀𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥∀𝑥𝜑 | ||
Theorem | axc711toc7 35934 | Rederivation of ax-c7 35903 from axc711 35932. Note that ax-c7 35903 and ax-11 2151 are not used by the rederivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
Theorem | axc711to11 35935 | Rederivation of ax-11 2151 from axc711 35932. Note that ax-c7 35903 and ax-11 2151 are not used by the rederivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Theorem | axc5c711 35936 | Proof of a single axiom that can replace ax-c5 35901, ax-c7 35903, and ax-11 2151 in a subsystem that includes these axioms plus ax-c4 35902 and ax-gen 1787 (and propositional calculus). See axc5c711toc5 35937, axc5c711toc7 35938, and axc5c711to11 35939 for the rederivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 35929. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥𝜑) → 𝜑) | ||
Theorem | axc5c711toc5 35937 | Rederivation of ax-c5 35901 from axc5c711 35936. Only propositional calculus is used by the rederivation. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | axc5c711toc7 35938 | Rederivation of ax-c7 35903 from axc5c711 35936. Note that ax-c7 35903 and ax-11 2151 are not used by the rederivation. The use of alimi 1803 (which uses ax-c5 35901) is allowed since we have already proved axc5c711toc5 35937. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
Theorem | axc5c711to11 35939 | Rederivation of ax-11 2151 from axc5c711 35936. Note that ax-c7 35903 and ax-11 2151 are not used by the rederivation. The use of alimi 1803 (which uses ax-c5 35901) is allowed since we have already proved axc5c711toc5 35937. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Theorem | equidqe 35940 | equid 2010 with existential quantifier without using ax-c5 35901 or ax-5 1902. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ ∀𝑦 ¬ 𝑥 = 𝑥 | ||
Theorem | axc5sp1 35941 | A special case of ax-c5 35901 without using ax-c5 35901 or ax-5 1902. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑦 ¬ 𝑥 = 𝑥 → ¬ 𝑥 = 𝑥) | ||
Theorem | equidq 35942 | equid 2010 with universal quantifier without using ax-c5 35901 or ax-5 1902. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∀𝑦 𝑥 = 𝑥 | ||
Theorem | equid1ALT 35943 | Alternate proof of equid 2010 and equid1 35917 from older axioms ax-c7 35903, ax-c10 35904 and ax-c9 35908. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑥 = 𝑥 | ||
Theorem | axc11nfromc11 35944 |
Rederivation of ax-c11n 35906 from original version ax-c11 35905. See theorem
axc11 2447 for the derivation of ax-c11 35905 from ax-c11n 35906.
This theorem should not be referenced in any proof. Instead, use ax-c11n 35906 above so that uses of ax-c11n 35906 can be more easily identified, or use aecom-o 35919 when this form is needed for studies involving ax-c11 35905 and omitting ax-5 1902. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Theorem | naecoms-o 35945 | A commutation rule for distinct variable specifiers. Version of naecoms 2446 using ax-c11 35905. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | hbnae-o 35946 | All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). Version of hbnae 2449 using ax-c11 35905. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | dvelimf-o 35947 | Proof of dvelimh 2467 that uses ax-c11 35905 but not ax-c15 35907, ax-c11n 35906, or ax-12 2167. Version of dvelimh 2467 using ax-c11 35905 instead of axc11 2447. (Contributed by NM, 12-Nov-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑧𝜓) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | dral2-o 35948 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Version of dral2 2455 using ax-c11 35905. (Contributed by NM, 27-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧𝜑 ↔ ∀𝑧𝜓)) | ||
Theorem | aev-o 35949* | A "distinctor elimination" lemma with no restrictions on variables in the consequent, proved without using ax-c16 35910. Version of aev 2053 using ax-c11 35905. (Contributed by NM, 8-Nov-2006.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑤 = 𝑣) | ||
Theorem | ax5eq 35950* | Theorem to add distinct quantifier to atomic formula. (This theorem demonstrates the induction basis for ax-5 1902 considered as a metatheorem. Do not use it for later proofs - use ax-5 1902 instead, to avoid reference to the redundant axiom ax-c16 35910.) (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦) | ||
Theorem | dveeq2-o 35951* | Quantifier introduction when one pair of variables is distinct. Version of dveeq2 2389 using ax-c15 35907. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
Theorem | axc16g-o 35952* | A generalization of axiom ax-c16 35910. Version of axc16g 2252 using ax-c11 35905. (Contributed by NM, 15-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑)) | ||
Theorem | dveeq1-o 35953* | Quantifier introduction when one pair of variables is distinct. Version of dveeq1 2391 using ax-c11 . (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | dveeq1-o16 35954* | Version of dveeq1 2391 using ax-c16 35910 instead of ax-5 1902. (Contributed by NM, 29-Apr-2008.) TODO: Recover proof from older set.mm to remove use of ax-5 1902. (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | ax5el 35955* | Theorem to add distinct quantifier to atomic formula. This theorem demonstrates the induction basis for ax-5 1902 considered as a metatheorem.) (Contributed by NM, 22-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦) | ||
Theorem | axc11n-16 35956* | This theorem shows that, given ax-c16 35910, we can derive a version of ax-c11n 35906. However, it is weaker than ax-c11n 35906 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 27-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥) | ||
Theorem | dveel2ALT 35957* | Alternate proof of dveel2 2480 using ax-c16 35910 instead of ax-5 1902. (Contributed by NM, 10-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦)) | ||
Theorem | ax12f 35958 | Basis step for constructing a substitution instance of ax-c15 35907 without using ax-c15 35907. We can start with any formula 𝜑 in which 𝑥 is not free. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Theorem | ax12eq 35959 | Basis step for constructing a substitution instance of ax-c15 35907 without using ax-c15 35907. Atomic formula for equality predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))) | ||
Theorem | ax12el 35960 | Basis step for constructing a substitution instance of ax-c15 35907 without using ax-c15 35907. Atomic formula for membership predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))) | ||
Theorem | ax12indn 35961 | Induction step for constructing a substitution instance of ax-c15 35907 without using ax-c15 35907. Negation case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (¬ 𝜑 → ∀𝑥(𝑥 = 𝑦 → ¬ 𝜑)))) | ||
Theorem | ax12indi 35962 | Induction step for constructing a substitution instance of ax-c15 35907 without using ax-c15 35907. Implication case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) & ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜓 → ∀𝑥(𝑥 = 𝑦 → 𝜓)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → ((𝜑 → 𝜓) → ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))))) | ||
Theorem | ax12indalem 35963 | Lemma for ax12inda2 35965 and ax12inda 35966. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))) | ||
Theorem | ax12inda2ALT 35964* | Alternate proof of ax12inda2 35965, slightly more direct and not requiring ax-c16 35910. (Contributed by NM, 4-May-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))) | ||
Theorem | ax12inda2 35965* | Induction step for constructing a substitution instance of ax-c15 35907 without using ax-c15 35907. Quantification case. When 𝑧 and 𝑦 are distinct, this theorem avoids the dummy variables needed by the more general ax12inda 35966. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))) | ||
Theorem | ax12inda 35966* | Induction step for constructing a substitution instance of ax-c15 35907 without using ax-c15 35907. Quantification case. (When 𝑧 and 𝑦 are distinct, ax12inda2 35965 may be used instead to avoid the dummy variable 𝑤 in the proof.) (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑥 = 𝑤 → (𝜑 → ∀𝑥(𝑥 = 𝑤 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))) | ||
Theorem | ax12v2-o 35967* | Rederivation of ax-c15 35907 from ax12v 2168 (without using ax-c15 35907 or the full ax-12 2167). Thus, the hypothesis (ax12v 2168) provides an alternate axiom that can be used in place of ax-c15 35907. See also axc15 2438. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Theorem | ax12a2-o 35968* | Derive ax-c15 35907 from a hypothesis in the form of ax-12 2167, without using ax-12 2167 or ax-c15 35907. The hypothesis is weaker than ax-12 2167, with 𝑧 both distinct from 𝑥 and not occurring in 𝜑. Thus, the hypothesis provides an alternate axiom that can be used in place of ax-12 2167, if we also have ax-c11 35905, which this proof uses. As theorem ax12 2440 shows, the distinct variable conditions are optional. An open problem is whether we can derive this with ax-c11n 35906 instead of ax-c11 35905. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑧 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Theorem | axc11-o 35969 |
Show that ax-c11 35905 can be derived from ax-c11n 35906 and ax-12 2167. An open
problem is whether this theorem can be derived from ax-c11n 35906 and the
others when ax-12 2167 is replaced with ax-c15 35907 or ax12v 2168. See theorem
axc11nfromc11 35944 for the rederivation of ax-c11n 35906 from axc11 2447.
Normally, axc11 2447 should be used rather than ax-c11 35905 or axc11-o 35969, except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Theorem | fsumshftd 35970* | Index shift of a finite sum with a weaker "implicit substitution" hypothesis than fsumshft 15125. The proof demonstrates how this can be derived starting from from fsumshft 15125. (Contributed by NM, 1-Nov-2019.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑗 = (𝑘 − 𝐾)) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))𝐵) | ||
Axiom | ax-riotaBAD 35971 | Define restricted description binder. In case it doesn't exist, we return a set which is not a member of the domain of discourse 𝐴. See also comments for df-iota 6308. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) WARNING: THIS "AXIOM", WHICH IS THE OLD df-riota 7103, CONFLICTS WITH (THE NEW) df-riota 7103 AND MAKES THE SYSTEM IN set.mm INCONSISTENT. IT IS TEMPORARY AND WILL BE DELETED AFTER ALL USES ARE ELIMINATED. |
⊢ (℩𝑥 ∈ 𝐴 𝜑) = if(∃!𝑥 ∈ 𝐴 𝜑, (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)), (Undef‘{𝑥 ∣ 𝑥 ∈ 𝐴})) | ||
Theorem | riotaclbgBAD 35972* | Closure of restricted iota. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝐴 ∈ 𝑉 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴)) | ||
Theorem | riotaclbBAD 35973* | Closure of restricted iota. (Contributed by NM, 15-Sep-2011.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴) | ||
Theorem | riotasvd 35974* | Deduction version of riotasv 35977. (Contributed by NM, 4-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ (𝜑 → 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝑥 = 𝐶))) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → ((𝑦 ∈ 𝐵 ∧ 𝜓) → 𝐷 = 𝐶)) | ||
Theorem | riotasv2d 35975* | Value of description binder 𝐷 for a single-valued class expression 𝐶(𝑦) (as in e.g. reusv2 5295). Special case of riota2f 7127. (Contributed by NM, 2-Mar-2013.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝐹) & ⊢ (𝜑 → Ⅎ𝑦𝜒) & ⊢ (𝜑 → 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝑥 = 𝐶))) & ⊢ ((𝜑 ∧ 𝑦 = 𝐸) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑦 = 𝐸) → 𝐶 = 𝐹) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) & ⊢ (𝜑 → 𝐸 ∈ 𝐵) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → 𝐷 = 𝐹) | ||
Theorem | riotasv2s 35976* | The value of description binder 𝐷 for a single-valued class expression 𝐶(𝑦) (as in e.g. reusv2 5295) in the form of a substitution instance. Special case of riota2f 7127. (Contributed by NM, 3-Mar-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
⊢ 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝐴 ∧ (𝐸 ∈ 𝐵 ∧ [𝐸 / 𝑦]𝜑)) → 𝐷 = ⦋𝐸 / 𝑦⦌𝐶) | ||
Theorem | riotasv 35977* | Value of description binder 𝐷 for a single-valued class expression 𝐶(𝑦) (as in e.g. reusv2 5295). Special case of riota2f 7127. (Contributed by NM, 26-Jan-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)) ⇒ ⊢ ((𝐷 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑) → 𝐷 = 𝐶) | ||
Theorem | riotasv3d 35978* | A property 𝜒 holding for a representative of a single-valued class expression 𝐶(𝑦) (see e.g. reusv2 5295) also holds for its description binder 𝐷 (in the form of property 𝜃). (Contributed by NM, 5-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜃) & ⊢ (𝜑 → 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝑥 = 𝐶))) & ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → (𝜒 ↔ 𝜃)) & ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ∧ 𝜓) → 𝜒)) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) & ⊢ (𝜑 → ∃𝑦 ∈ 𝐵 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → 𝜃) | ||
Theorem | elimhyps 35979 | A version of elimhyp 4528 using explicit substitution. (Contributed by NM, 15-Jun-2019.) |
⊢ [𝐵 / 𝑥]𝜑 ⇒ ⊢ [if(𝜑, 𝑥, 𝐵) / 𝑥]𝜑 | ||
Theorem | dedths 35980 | A version of weak deduction theorem dedth 4521 using explicit substitution. (Contributed by NM, 15-Jun-2019.) |
⊢ [if(𝜑, 𝑥, 𝐵) / 𝑥]𝜓 ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | renegclALT 35981 | Closure law for negative of reals. Demonstrates use of weak deduction theorem with explicit substitution. The proof is much longer than that of renegcl 10938. (Contributed by NM, 15-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ) | ||
Theorem | elimhyps2 35982 | Generalization of elimhyps 35979 that is not useful unless we can separately prove ⊢ 𝐴 ∈ V. (Contributed by NM, 13-Jun-2019.) |
⊢ [𝐵 / 𝑥]𝜑 ⇒ ⊢ [if([𝐴 / 𝑥]𝜑, 𝐴, 𝐵) / 𝑥]𝜑 | ||
Theorem | dedths2 35983 | Generalization of dedths 35980 that is not useful unless we can separately prove ⊢ 𝐴 ∈ V. (Contributed by NM, 13-Jun-2019.) |
⊢ [if([𝐴 / 𝑥]𝜑, 𝐴, 𝐵) / 𝑥]𝜓 ⇒ ⊢ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓) | ||
Theorem | nfcxfrdf 35984 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by NM, 19-Nov-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥𝐴) | ||
Theorem | nfded 35985 | A deduction theorem that converts a not-free inference directly to deduction form. The first hypothesis is the hypothesis of the deduction form. The second is an equality deduction (e.g., (Ⅎ𝑥𝐴 → ∪ {𝑦 ∣ ∀𝑥𝑦 ∈ 𝐴} = ∪ 𝐴)) that starts from abidnf 3693. The last is assigned to the inference form (e.g., Ⅎ𝑥∪ {𝑦 ∣ ∀𝑥𝑦 ∈ 𝐴}) whose hypothesis is satisfied using nfaba1 2986. (Contributed by NM, 19-Nov-2020.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (Ⅎ𝑥𝐴 → 𝐵 = 𝐶) & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝜑 → Ⅎ𝑥𝐶) | ||
Theorem | nfded2 35986 | A deduction theorem that converts a not-free inference directly to deduction form. The first 2 hypotheses are the hypotheses of the deduction form. The third is an equality deduction (e.g., ((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝐵) → 〈{𝑦 ∣ ∀𝑥𝑦 ∈ 𝐴}, {𝑦 ∣ ∀𝑥𝑦 ∈ 𝐵}〉 = 〈𝐴, 𝐵〉) for nfopd 4814) that starts from abidnf 3693. The last is assigned to the inference form (e.g., Ⅎ𝑥〈{𝑦 ∣ ∀𝑥𝑦 ∈ 𝐴}, {𝑦 ∣ ∀𝑥𝑦 ∈ 𝐵}〉 for nfop 4813) whose hypotheses are satisfied using nfaba1 2986. (Contributed by NM, 19-Nov-2020.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) & ⊢ ((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝐵) → 𝐶 = 𝐷) & ⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (𝜑 → Ⅎ𝑥𝐷) | ||
Theorem | nfunidALT2 35987 | Deduction version of nfuni 4839. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴) | ||
Theorem | nfunidALT 35988 | Deduction version of nfuni 4839. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴) | ||
Theorem | nfopdALT 35989 | Deduction version of bound-variable hypothesis builder nfop 4813. This shows how the deduction version of a not-free theorem such as nfop 4813 can be created from the corresponding not-free inference theorem. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥〈𝐴, 𝐵〉) | ||
Theorem | cnaddcom 35990 | Recover the commutative law of addition for complex numbers from the Abelian group structure. (Contributed by NM, 17-Mar-2013.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Theorem | toycom 35991* | Show the commutative law for an operation 𝑂 on a toy structure class 𝐶 of commuatitive operations on ℂ. This illustrates how a structure class can be partially specialized. In practice, we would ordinarily define a new constant such as "CAbel" in place of 𝐶. (Contributed by NM, 17-Mar-2013.) (Proof modification is discouraged.) |
⊢ 𝐶 = {𝑔 ∈ Abel ∣ (Base‘𝑔) = ℂ} & ⊢ + = (+g‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐶 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Syntax | clsa 35992 | Extend class notation with all 1-dim subspaces (atoms) of a left module or left vector space. |
class LSAtoms | ||
Syntax | clsh 35993 | Extend class notation with all subspaces of a left module or left vector space that are hyperplanes. |
class LSHyp | ||
Definition | df-lsatoms 35994* | Define the set of all 1-dim subspaces (atoms) of a left module or left vector space. (Contributed by NM, 9-Apr-2014.) |
⊢ LSAtoms = (𝑤 ∈ V ↦ ran (𝑣 ∈ ((Base‘𝑤) ∖ {(0g‘𝑤)}) ↦ ((LSpan‘𝑤)‘{𝑣}))) | ||
Definition | df-lshyp 35995* | Define the set of all hyperplanes of a left module or left vector space. Also called co-atoms, these are subspaces that are one dimension less that the full space. (Contributed by NM, 29-Jun-2014.) |
⊢ LSHyp = (𝑤 ∈ V ↦ {𝑠 ∈ (LSubSp‘𝑤) ∣ (𝑠 ≠ (Base‘𝑤) ∧ ∃𝑣 ∈ (Base‘𝑤)((LSpan‘𝑤)‘(𝑠 ∪ {𝑣})) = (Base‘𝑤))}) | ||
Theorem | lshpset 35996* | The set of all hyperplanes of a left module or left vector space. The vector 𝑣 is called a generating vector for the hyperplane. (Contributed by NM, 29-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → 𝐻 = {𝑠 ∈ 𝑆 ∣ (𝑠 ≠ 𝑉 ∧ ∃𝑣 ∈ 𝑉 (𝑁‘(𝑠 ∪ {𝑣})) = 𝑉)}) | ||
Theorem | islshp 35997* | The predicate "is a hyperplane" (of a left module or left vector space). (Contributed by NM, 29-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → (𝑈 ∈ 𝐻 ↔ (𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃𝑣 ∈ 𝑉 (𝑁‘(𝑈 ∪ {𝑣})) = 𝑉))) | ||
Theorem | islshpsm 35998* | Hyperplane properties expressed with subspace sum. (Contributed by NM, 3-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → (𝑈 ∈ 𝐻 ↔ (𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃𝑣 ∈ 𝑉 (𝑈 ⊕ (𝑁‘{𝑣})) = 𝑉))) | ||
Theorem | lshplss 35999 | A hyperplane is a subspace. (Contributed by NM, 3-Jul-2014.) |
⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) ⇒ ⊢ (𝜑 → 𝑈 ∈ 𝑆) | ||
Theorem | lshpne 36000 | A hyperplane is not equal to the vector space. (Contributed by NM, 4-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) ⇒ ⊢ (𝜑 → 𝑈 ≠ 𝑉) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |