Home | Metamath
Proof Explorer Theorem List (p. 326 of 410) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-26627) |
Hilbert Space Explorer
(26628-28150) |
Users' Mathboxes
(28151-40909) |
Type | Label | Description |
---|---|---|
Statement | ||
Note: A label suffixed with "N" (after the "Atoms..." section below), such as lshpnel2N 32597, means that the definition or theorem is not used for the derivation of hlathil 35578. This is a temporary renaming to assist cleaning up the theorems needed by hlathil 35578. | ||
These older axiom schemes are obsolete and should not be used outside of this section. They are proved above as theorems axc4 , sp 1948, axc7 1950, axc10 2107, axc11 2159, axc11n 2154, axc15 2188, axc9 2151, axc14 2212, and axc16 2035. | ||
Axiom | ax-c5 32501 |
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 1680. Conditional forms of the converse are given by ax-13 2102, ax-c14 32509, ax-c16 32510, and ax-5 1769. 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 2195. An interesting alternate axiomatization uses axc5c711 32535 and ax-c4 32502 in place of ax-c5 32501, ax-4 1693, ax-10 1926, and ax-11 1931. This axiom is obsolete and should no longer be used. It is proved above as theorem sp 1948. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.) |
Axiom | ax-c4 32502 |
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 1949. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.) |
Axiom | ax-c7 32503 |
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 32535 in place
of ax-c5 32501, ax-c7 32503, and ax-11 1931.
This axiom is obsolete and should no longer be used. It is proved above as theorem axc7 1950. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
Axiom | ax-c10 32504 |
A variant of ax6 2106. 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 2107. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
Axiom | ax-c11 32505 |
Axiom ax-c11 32505 was the original version of ax-c11n 32506 ("n" for "new"),
before it was discovered (in May 2008) that the shorter ax-c11n 32506 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 2159. (Contributed by NM, 10-May-1993.) (New usage is discouraged.) |
Axiom | ax-c11n 32506 |
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 32505 and was replaced with this shorter ax-c11n 32506 ("n" for "new") in May 2008. The old axiom is proved from this one as theorem axc11 2159. Conversely, this axiom is proved from ax-c11 32505 as theorem axc11nfromc11 32543. This axiom was proved redundant in July 2015. See theorem axc11n 2154. This axiom is obsolete and should no longer be used. It is proved above as theorem axc11n 2154. (Contributed by NM, 16-May-2008.) (New usage is discouraged.) |
Axiom | ax-c15 32507 |
Axiom ax-c15 32507 was the original version of ax-12 1944, before it was
discovered (in Jan. 2007) that the shorter ax-12 1944 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 32507 (from which the ax-12 1944 instance follows by theorem ax12 32521.) The proof is by induction on formula length, using ax12eq 32558 and ax12el 32559 for the basis steps and ax12indn 32560, ax12indi 32561, and ax12inda 32565 for the induction steps. (This paragraph is true provided we use ax-c11 32505 in place of ax-c11n 32506.) This axiom is obsolete and should no longer be used. It is proved above as theorem axc15 2188, which should be used instead. (Contributed by NM, 14-May-1993.) (New usage is discouraged.) |
Axiom | ax-c9 32508 |
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 2151. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
Axiom | ax-c14 32509 |
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 1769; see theorem axc14 2212. Alternately,
ax-5 1769 becomes unnecessary in principle with this
axiom, but we lose the
more powerful metalogic afforded by ax-5 1769.
We retain ax-c14 32509 here to
provide completeness for systems with the simpler metalogic that results
from omitting ax-5 1769, 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 2212. (Contributed by NM, 24-Jun-1993.) (New usage is discouraged.) |
Axiom | ax-c16 32510* |
Axiom of Distinct Variables. The only axiom of predicate calculus
requiring that variables be distinct (if we consider ax-5 1769
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 4611), but nonetheless it is technically
necessary as you can see from its uses.
This axiom is redundant if we include ax-5 1769; see theorem axc16 2035. Alternately, ax-5 1769 becomes logically redundant in the presence of this axiom, but without ax-5 1769 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 32510 here to provide logical completeness for systems with the simpler metalogic that results from omitting ax-5 1769, 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 2035. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
Theorems ax12 32521 and ax13fromc9 32522 require some intermediate theorems that are included in this section. | ||
Theorem | axc5 32511 | This theorem repeats sp 1948 under the name axc5 32511, so that the metamath program's "verify markup" command will check that it matches axiom scheme ax-c5 32501. It is preferred that references to this theorem use the name sp 1948. (Contributed by NM, 18-Aug-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | ax4 32512 | Rederivation of axiom ax-4 1693 from ax-c4 32502 and other older axioms. See axc4 1949 for the derivation of ax-c4 32502 from ax-4 1693. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ax10 32513 | Rederivation of axiom ax-10 1926 from ax-c7 32503 and other older axioms. See axc7 1950 for the derivation of ax-c7 32503 from ax-10 1926. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ax6fromc10 32514 | Rederivation of axiom ax-6 1816 from ax-c10 32504 and other older axioms. See axc10 2107 for the derivation of ax-c10 32504 from ax-6 1816. Lemma L18 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | hba1-o 32515 | 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.) (New usage is discouraged.) |
Theorem | axc4i-o 32516 | Inference version of ax-c4 32502. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.) |
Theorem | aecom-o 32517 | 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 2156 using ax-c11 32505. Unlike axc11nfromc11 32543, this version does not require ax-5 1769. (Contributed by NM, 10-May-1993.) (New usage is discouraged.) |
Theorem | aecoms-o 32518 | A commutation rule for identical variable specifiers. Version of aecoms 2157 using ax-c11 . (Contributed by NM, 10-May-1993.) (New usage is discouraged.) |
Theorem | hbae-o 32519 | All variables are effectively bound in an identical variable specifier. Version of hbae 2160 using ax-c11 32505. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | dral1-o 32520 | 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 2170 using ax-c11 32505. (Contributed by NM, 24-Nov-1994.) (New usage is discouraged.) |
Theorem | ax12 32521 |
Rederivation of axiom ax-12 1944 from ax-c15 32507, ax-c11 32505, and other older
axioms. See theorem axc15 2188 for the derivation of ax-c15 32507 from ax-12 1944.
An open problem is whether we can prove this using ax-c11n 32506 instead of ax-c11 32505. This proof uses newer axioms ax-4 1693 and ax-6 1816, 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 32502 and ax-c10 32504. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ax13fromc9 32522 |
Derive ax-13 2102 from ax-c9 32508 and other older axioms.
This proof uses newer axioms ax-4 1693 and ax-6 1816, 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 32502 and ax-c10 32504. (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 32523* |
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 1769 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 1680, ax-c4 32502, ax-c5 32501, ax-11 1931, ax-c7 32503, ax-7 1862, ax-c9 32508, ax-c10 32504, ax-c11 32505, ax-8 1900, ax-9 1907, ax-c14 32509, ax-c15 32507, and ax-c16 32510: in that system, we can derive any instance of ax-5 1769 not containing wff variables by induction on formula length, using ax5eq 32549 and ax5el 32554 for the basis together hbn 1988, hbal 1933, and hbim 2016. 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 | equid1 32524 | Proof of equid 1866 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 1769; see the proof of equid 1866. See equid1ALT 32542 for an alternate proof. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | sps-o 32525 | Generalization of antecedent. (Contributed by NM, 5-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | hbequid 32526 | 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 32504.) (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 32527 | 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 1693, ax-7 1862, ax-c9 32508, and ax-gen 1680. This shows that this can be proved without ax6 2106, even though the theorem equid 1866 cannot be. A shorter proof using ax6 2106 is obtainable from equid 1866 and hbth 1686.) Remark added 2-Dec-2015 NM: This proof does implicitly use ax6v 1817, which is used for the derivation of axc9 2151, unless we consider ax-c9 32508 the starting axiom rather than ax-13 2102. (Contributed by NM, 13-Jan-2011.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | axc5c7 32528 | Proof of a single axiom that can replace ax-c5 32501 and ax-c7 32503. See axc5c7toc5 32529 and axc5c7toc7 32530 for the re-derivation of those axioms. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | axc5c7toc5 32529 | Re-derivation of ax-c5 32501 from axc5c7 32528. Only propositional calculus is used for the re-derivation. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | axc5c7toc7 32530 | Re-derivation of ax-c7 32503 from axc5c7 32528. Only propositional calculus is used for the re-derivation. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | axc711 32531 | Proof of a single axiom that can replace both ax-c7 32503 and ax-11 1931. See axc711toc7 32533 and axc711to11 32534 for the re-derivation of those axioms. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | nfa1-o 32532 | is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | axc711toc7 32533 | Re-derivation of ax-c7 32503 from axc711 32531. Note that ax-c7 32503 and ax-11 1931 are not used by the re-derivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | axc711to11 32534 | Re-derivation of ax-11 1931 from axc711 32531. Note that ax-c7 32503 and ax-11 1931 are not used by the re-derivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | axc5c711 32535 | Proof of a single axiom that can replace ax-c5 32501, ax-c7 32503, and ax-11 1931 in a subsystem that includes these axioms plus ax-c4 32502 and ax-gen 1680 (and propositional calculus). See axc5c711toc5 32536, axc5c711toc7 32537, and axc5c711to11 32538 for the re-derivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 32528. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | axc5c711toc5 32536 | Re-derivation of ax-c5 32501 from axc5c711 32535. Only propositional calculus is used by the re-derivation. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | axc5c711toc7 32537 | Re-derivation of ax-c7 32503 from axc5c711 32535. Note that ax-c7 32503 and ax-11 1931 are not used by the re-derivation. The use of alimi 1695 (which uses ax-c5 32501) is allowed since we have already proved axc5c711toc5 32536. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | axc5c711to11 32538 | Re-derivation of ax-11 1931 from axc5c711 32535. Note that ax-c7 32503 and ax-11 1931 are not used by the re-derivation. The use of alimi 1695 (which uses ax-c5 32501) is allowed since we have already proved axc5c711toc5 32536. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | equidqe 32539 | equid 1866 with existential quantifier without using ax-c5 32501 or ax-5 1769. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | axc5sp1 32540 | A special case of ax-c5 32501 without using ax-c5 32501 or ax-5 1769. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | equidq 32541 | equid 1866 with universal quantifier without using ax-c5 32501 or ax-5 1769. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | equid1ALT 32542 | Alternate proof of equid 1866 and equid1 32524 from older axioms ax-c7 32503, ax-c10 32504 and ax-c9 32508. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | axc11nfromc11 32543 |
Rederivation of ax-c11n 32506 from original version ax-c11 32505. See theorem
axc11 2159 for the derivation of ax-c11 32505 from ax-c11n 32506.
This theorem should not be referenced in any proof. Instead, use ax-c11n 32506 above so that uses of ax-c11n 32506 can be more easily identified, or use aecom-o 32517 when this form is needed for studies involving ax-c11 32505 and omitting ax-5 1769. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | naecoms-o 32544 | A commutation rule for distinct variable specifiers. Version of naecoms 2158 using ax-c11 32505. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | hbnae-o 32545 | All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). Version of hbnae 2162 using ax-c11 32505. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | dvelimf-o 32546 | Proof of dvelimh 2181 that uses ax-c11 32505 but not ax-c15 32507, ax-c11n 32506, or ax-12 1944. Version of dvelimh 2181 using ax-c11 32505 instead of axc11 2159. (Contributed by NM, 12-Nov-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | dral2-o 32547 | 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 2169 using ax-c11 32505. (Contributed by NM, 27-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | aev-o 32548* | A "distinctor elimination" lemma with no restrictions on variables in the consequent, proved without using ax-c16 32510. Version of aev 2037 using ax-c11 32505. (Contributed by NM, 8-Nov-2006.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ax5eq 32549* | Theorem to add distinct quantifier to atomic formula. (This theorem demonstrates the induction basis for ax-5 1769 considered as a metatheorem. Do not use it for later proofs - use ax-5 1769 instead, to avoid reference to the redundant axiom ax-c16 32510.) (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | dveeq2-o 32550* | Quantifier introduction when one pair of variables is distinct. Version of dveeq2 2147 using ax-c15 32507. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | axc16g-o 32551* | A generalization of axiom ax-c16 32510. Version of axc16g 2034 using ax-c11 32505. (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 32552* | Quantifier introduction when one pair of variables is distinct. Version of dveeq1 2149 using ax-c11 . (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | dveeq1-o16 32553* | Version of dveeq1 2149 using ax-c16 32510 instead of ax-5 1769. (Contributed by NM, 29-Apr-2008.) TODO: Recover proof from older set.mm to remove use of ax-5 1769. (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ax5el 32554* | Theorem to add distinct quantifier to atomic formula. This theorem demonstrates the induction basis for ax-5 1769 considered as a metatheorem.) (Contributed by NM, 22-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | axc11n-16 32555* | This theorem shows that, given ax-c16 32510, we can derive a version of ax-c11n 32506. However, it is weaker than ax-c11n 32506 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 27-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | dveel2ALT 32556* | Alternate proof of dveel2 2211 using ax-c16 32510 instead of ax-5 1769. (Contributed by NM, 10-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ax12f 32557 | Basis step for constructing a substitution instance of ax-c15 32507 without using ax-c15 32507. 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 32558 | Basis step for constructing a substitution instance of ax-c15 32507 without using ax-c15 32507. Atomic formula for equality predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ax12el 32559 | Basis step for constructing a substitution instance of ax-c15 32507 without using ax-c15 32507. Atomic formula for membership predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ax12indn 32560 | Induction step for constructing a substitution instance of ax-c15 32507 without using ax-c15 32507. Negation case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ax12indi 32561 | Induction step for constructing a substitution instance of ax-c15 32507 without using ax-c15 32507. Implication case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ax12indalem 32562 | Lemma for ax12inda2 32564 and ax12inda 32565. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ax12inda2ALT 32563* | Alternate proof of ax12inda2 32564, slightly more direct and not requiring ax-c16 32510. (Contributed by NM, 4-May-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ax12inda2 32564* | Induction step for constructing a substitution instance of ax-c15 32507 without using ax-c15 32507. Quantification case. When and are distinct, this theorem avoids the dummy variables needed by the more general ax12inda 32565. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ax12inda 32565* | Induction step for constructing a substitution instance of ax-c15 32507 without using ax-c15 32507. Quantification case. (When and are distinct, ax12inda2 32564 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 32566* | Recovery of ax-c15 32507 from ax12v 1945 without using ax-c15 32507. The hypothesis is even weaker than ax12v 1945, with both distinct from and not occurring in . Thus, the hypothesis provides an alternate axiom that can be used in place of ax-c15 32507. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ax12a2-o 32567* | Derive ax-c15 32507 from a hypothesis in the form of ax-12 1944, without using ax-12 1944 or ax-c15 32507. The hypothesis is even weaker than ax-12 1944, with both distinct from and not occurring in . Thus, the hypothesis provides an alternate axiom that can be used in place of ax-12 1944, if we also hvae ax-c11 32505 which this proof uses . As theorem ax12 32521 shows, the distinct variable conditions are optional. An open problem is whether we can derive this with ax-c11n 32506 instead of ax-c11 32505. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | axc11-o 32568 |
Show that ax-c11 32505 can be derived from ax-c11n 32506. An open problem is
whether this theorem can be derived from ax-c11n 32506 and the others when
ax-12 1944 is replaced with ax-c15 32507. See theorem axc11nfromc11 32543 for the
rederivation of ax-c11n 32506 from axc11 2159.
Normally, axc11 2159 should be used rather than ax-c11 32505 or axc11-o 32568, 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 32569* | Index shift of a finite sum with a weaker "implicit substitution" hypothesis than fsumshft 13896. The proof demonstrates how this can be derived starting from from fsumshft 13896. (Contributed by NM, 1-Nov-2019.) |
Theorem | fsumshftdOLD 32570* | Obsolete version of fsumshftd 32569 as of 1-Nov-2019. (Contributed by NM, 1-Nov-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
Axiom | ax-riotaBAD 32571 | 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 5569. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) WARNING: THIS "AXIOM", WHICH IS THE OLD df-riota 6282, CONFLICTS WITH (THE NEW) df-riota 6282 AND MAKES THE SYSTEM IN set.mm INCONSISTENT. IT IS TEMPORARY AND WILL BE DELETED AFTER ALL USES ARE ELIMINATED. |
Theorem | riotaclbgBAD 32572* | Closure of restricted iota. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 24-Dec-2016.) |
Theorem | riotaclbBAD 32573* | Closure of restricted iota. (Contributed by NM, 15-Sep-2011.) |
Theorem | riotasvd 32574* | Deduction version of riotasv 32577. (Contributed by NM, 4-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | riotasv2d 32575* | Value of description binder for a single-valued class expression (as in e.g. reusv2 4626). Special case of riota2f 6303. (Contributed by NM, 2-Mar-2013.) |
Theorem | riotasv2s 32576* | The value of description binder for a single-valued class expression (as in e.g. reusv2 4626) in the form of a substitution instance. Special case of riota2f 6303. (Contributed by NM, 3-Mar-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
Theorem | riotasv 32577* | Value of description binder for a single-valued class expression (as in e.g. reusv2 4626). Special case of riota2f 6303. (Contributed by NM, 26-Jan-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
Theorem | riotasv3d 32578* | A property holding for a representative of a single-valued class expression (see e.g. reusv2 4626) 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 32579 | A version of elimhyp 3951 using explicit substitution. (Contributed by NM, 15-Jun-2019.) |
Theorem | dedths 32580 | A version of weak deduction theorem dedth 3944 using explicit substitution. (Contributed by NM, 15-Jun-2019.) |
Theorem | renegclALT 32581 | Closure law for negative of reals. Demonstrates use of weak deduction theorem with explicit substitution. The proof is much longer than that of renegcl 9968. (Contributed by NM, 15-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | elimhyps2 32582 | Generalization of elimhyps 32579 that is not useful unless we can separately prove . (Contributed by NM, 13-Jun-2019.) |
Theorem | dedths2 32583 | Generalization of dedths 32580 that is not useful unless we can separately prove . (Contributed by NM, 13-Jun-2019.) |
Theorem | cnaddcom 32584 | 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 32585* | 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.) |
Syntax | clsa 32586 | Extend class notation with all 1-dim subspaces (atoms) of a left module or left vector space. |
LSAtoms | ||
Syntax | clsh 32587 | Extend class notation with all subspaces of a left module or left vector space that are hyperplanes. |
LSHyp | ||
Definition | df-lsatoms 32588* | Define the set of all 1-dim subspaces (atoms) of a left module or left vector space. (Contributed by NM, 9-Apr-2014.) |
LSAtoms | ||
Definition | df-lshyp 32589* | 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 | ||
Theorem | lshpset 32590* | 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.) |
LSHyp | ||
Theorem | islshp 32591* | The predicate "is a hyperplane" (of a left module or left vector space). (Contributed by NM, 29-Jun-2014.) |
LSHyp | ||
Theorem | islshpsm 32592* | Hyperplane properties expressed with subspace sum. (Contributed by NM, 3-Jul-2014.) |
LSHyp | ||
Theorem | lshplss 32593 | A hyperplane is a subspace. (Contributed by NM, 3-Jul-2014.) |
LSHyp | ||
Theorem | lshpne 32594 | A hyperplane is not equal to the vector space. (Contributed by NM, 4-Jul-2014.) |
LSHyp | ||
Theorem | lshpnel 32595 | A hyperplane's generating vector does not belong to the hyperplane. (Contributed by NM, 3-Jul-2014.) |
LSHyp | ||
Theorem | lshpnelb 32596 | The subspace sum of a hyperplane and the span of an element equals the vector space iff the element is not in the hyperplane. (Contributed by NM, 2-Oct-2014.) |
LSHyp | ||
Theorem | lshpnel2N 32597 | Condition that determines a hyperplane. (Contributed by NM, 3-Oct-2014.) (New usage is discouraged.) |
LSHyp | ||
Theorem | lshpne0 32598 | The member of the span in the hyperplane definition does not belong to the hyperplane. (Contributed by NM, 14-Jul-2014.) |
LSHyp | ||
Theorem | lshpdisj 32599 | A hyperplane and the span in the hyperplane definition are disjoint. (Contributed by NM, 3-Jul-2014.) |
LSHyp | ||
Theorem | lshpcmp 32600 | If two hyperplanes are comparable, they are equal. (Contributed by NM, 9-Oct-2014.) |
LSHyp |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |