mmtheorems20 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10697

Statement List for Metamath Proof Explorer - 1901-2000 - Page 20 of 107

Type	Label	Description
Statement
Theorem	elab3 1901	Membership in a class abstraction using implicit substitution.
|- (ps -> A e. V)   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. {x | ph} <-> ps)
Theorem	elrabf 1902	Membership in a restricted class abstraction with implicit substitution. This version has bound-variable hypotheses in place of distinct variable restrictions.
|- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   &   |- (ps -> A.xps)   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. {x e. B | ph} <-> (A e. B /\ ps))
Theorem	elrab 1903	Membership in a restricted class abstraction with implicit substitution.
|- (x = A -> (ph <-> ps))   =>   |- (A e. {x e. B | ph} <-> (A e. B /\ ps))
Theorem	elrab3 1904	Membership in a restricted class abstraction with implicit substitution.
|- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (A e. {x e. B | ph} <-> ps))
Theorem	elrab2 1905	Membership in a class abstraction, using implicit substitution.
|- (x = A -> (ph <-> ps))   &   |- C = {x e. B | ph}   =>   |- (A e. C <-> (A e. B /\ ps))
Theorem	cbvab 1906	Rule used to change bound variables with implicit substitution.
|- (ph -> A.yph)   &   |- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- {x | ph} = {y | ps}
Theorem	cbvabv 1907	Rule used to change bound variables with implicit substitution.
|- (x = y -> (ph <-> ps))   =>   |- {x | ph} = {y | ps}
Theorem	cbvrab 1908	Rule to change the bound variable in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions.
|- (z e. A -> A.x z e. A)   &   |- (z e. A -> A.y z e. A)   &   |- (ph -> A.yph)   &   |- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- {x e. A | ph} = {y e. A | ps}
Theorem	cbvrabv 1909	Rule to change the bound variable in a restricted class abstraction, using implicit substitution.
|- (x = y -> (ph <-> ps))   =>   |- {x e. A | ph} = {y e. A | ps}
Theorem	abidhb 1910	Identity used to create closed-form versions of bound-variable hypothesis builders for class expressions.
|- (A.y(y e. A -> A.x y e. A) -> {z | A.x z e. A} = A)
Theorem	hbeqd 1911	Deduction version of bound-variable hypothesis builder hbeq 1564.
|- (ph -> A.xph)   &   |- (ph -> (y e. A -> A.x y e. A))   &   |- (ph -> (y e. B -> A.x y e. B))   =>   |- (ph -> (A = B -> A.x A = B))
Theorem	hbeld 1912	Deduction version of bound-variable hypothesis builder hbel 1565.
|- (ph -> A.xph)   &   |- (ph -> (y e. A -> A.x y e. A))   &   |- (ph -> (y e. B -> A.x y e. B))   =>   |- (ph -> (A e. B -> A.x A e. B))
Theorem	dedhb 1913	A deduction theorem for converting the inference |- (y e. A -> A.xy e. A) => |- ph into a closed theorem. Use hba1 1003 and hbab 1467 to eliminate the hypothesis of the substitution instance ps of the inference.
|- (A = {z | A.x z e. A} -> (ph <-> ps))   &   |- ps   =>   |- (A.y(y e. A -> A.x y e. A) -> ph)
Theorem	eueq 1914	Equality has existential uniqueness.
|- (A e. V <-> E!x x = A)
Theorem	eueq1 1915	Equality has existential uniqueness.
|- A e. V   =>   |- E!x x = A
Theorem	eueq2 1916	Equality has existential uniqueness (split into 2 cases).
|- A e. V   &   |- B e. V   =>   |- E!x((ph /\ x = A) \/ (-. ph /\ x = B))
Theorem	eueq3 1917	Equality has existential uniqueness (split into 3 cases).
|- A e. V   &   |- B e. V   &   |- C e. V   &   |- -. (ph /\ ps)   =>   |- E!x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))
Theorem	moeq 1918	There is at most one set equal to a class.
|- E*x x = A
Theorem	moeq3 1919	"At most one" property of equality (split into 3 cases). (The first 2 hypotheses could be eliminated with longer proof.)
|- B e. V   &   |- C e. V   &   |- -. (ph /\ ps)   =>   |- E*x((ph /\ x = A) \/ (-. (ph \/ ps) /\ x = B) \/ (ps /\ x = C))
Theorem	mosub 1920	"At most one" remains true after substitution.
|- E*xph   =>   |- E*xE.y(y = A /\ ph)
Theorem	mo2icl 1921	Theorem for inferring "at most one."
|- (A.x(ph -> x = A) -> E*xph)
Theorem	moi2 1922	Consequence of "at most one."
|- (x = A -> (ph <-> ps))   =>   |- (((A e. B /\ E*xph) /\ (ph /\ ps)) -> x = A)
Theorem	moi 1923	Equality implied by "at most one."
|- (x = A -> (ph <-> ps))   &   |- (x = B -> (ph <-> ch))   =>   |- (((A e. C /\ B e. D) /\ E*xph /\ (ps /\ ch)) -> A = B)
Theorem	euxfr2 1924	Transfer existential uniqueness from a variable x to another variable y contained in expression A.
|- A e. V   &   |- E*y x = A   =>   |- (E!xE.y(x = A /\ ph) <-> E!yph)
Theorem	euxfr 1925	Transfer existential uniqueness from a variable x to another variable y contained in expression A.
|- A e. V   &   |- E!y x = A   &   |- (x = A -> (ph <-> ps))   =>   |- (E!xph <-> E!yps)
Theorem	reurex 1926	Restricted unique existence implies restricted existence.
|- (E!x e. A ph -> E.x e. A ph)
Theorem	reu5 1927	Restricted uniqueness in terms of "at most one."
|- (E!x e. A ph <-> (E.x e. A ph /\ E*x(x e. A /\ ph)))
Theorem	reu2 1928	A way to express restricted uniqueness.
|- (E!x e. A ph <-> (E.x e. A ph /\ A.x e. A A.y e. A ((ph /\ [y / x]ph) -> x = y)))
Theorem	reu3 1929	A way to express restricted uniqueness.
|- (E!x e. A ph <-> E.y e. A A.x e. A (ph <-> x = y))
Theorem	reu6 1930	A way to express restricted uniqueness.
|- (E!x e. A ph <-> (E.x e. A ph /\ E.y e. A A.x e. A (ph -> x = y)))
Theorem	rmo4 1931	Restricted "at most one" using implicit substitution.
|- (x = y -> (ph <-> ps))   =>   |- (E*x(x e. A /\ ph) <-> A.x e. A A.y e. A ((ph /\ ps) -> x = y))
Theorem	reu4 1932	Restricted uniqueness using implicit substitution.
|- (x = y -> (ph <-> ps))   =>   |- (E!x e. A ph <-> (E.x e. A ph /\ A.x e. A A.y e. A ((ph /\ ps) -> x = y)))
Theorem	reu7 1933	Restricted uniqueness using implicit substitution.
|- (x = y -> (ph <-> ps))   =>   |- (E!x e. A ph <-> (E.x e. A ph /\ E.x e. A A.y e. A (ps -> x = y)))
Theorem	reu8 1934	Restricted uniqueness using implicit substitution.
|- (x = y -> (ph <-> ps))   =>   |- (E!x e. A ph <-> E.x e. A (ph /\ A.y e. A (ps -> x = y)))
Theorem	2reuswap 1935	A condition allowing swap of uniqueness and existential quantifiers.
|- (A.x e. A E*y(y e. A /\ ph) -> (E!x e. A E.y e. A ph -> E!y e. A E.x e. A ph))
Russell's Paradox
Theorem	ru 1936	Russell's Paradox. Proposition 4.14 of [TakeutiZaring] p. 14. Frege's Axiom of (unrestricted) Comprehension, expressed in our notation as A e. V, asserted that any collection of sets A is a set i.e. belongs to the universe V of all sets. In particular, by substituting {x | x e/ x} (the "Russell class") for A, it asserted {x | x e/ x} e. V, meaning that the "collection of all sets which are not members of themselves" is a set. However, here we prove {x | x e/ x} e/ V. This contradiction was discovered by Russell in 1901 (published in 1903), invalidating Comprehension and leading to the collapse of Frege's system. In 1908 Zermelo rectified this fatal flaw by replacing Comprehension with a weaker Subset (or Separation) Axiom ssex 2717 asserting that A is a set only when it is smaller than some other set B. However, Zermelo was then faced with a "chicken and egg" problem of how to show B is a set, leading him to introduce the set-building axioms of Null Set 0ex 2709, Pairing prex 2779, Union uniex 2868, Power Set pwex 2743, and Infinity omex 4615 to give him some starting sets to work with (all of which, before Russell's Paradox, were immediate consequences of Frege's Comprehension). In 1922 Fraenkel strengthened the Subset Axiom with our present Replacement Axiom funimaex 3574 (whose modern formalization is due to Skolem, also in 1922). Thus in a very real sense Russell's Paradox spawned the invention of ZF set theory and completely revised the foundations of mathematics! Another mainstream formalization of set theory, devised by von Neumann, Bernays, and Goedel, uses class variables rather than set variables as its primitives. The axiom system NBG in [Mendelson] p. 225 is suitable for a Metamath encoding. NBG is a conservative extension of ZF in that it proves exactly the same theorems as ZF that are expressible in the language of ZF. An advantage of NBG is that it is finitely axiomatizable - the Axiom of Replacement can be broken down into a finite set of formulas that eliminate its wff metavariable. Finite axiomatizability is required by some proof languages (although not by Metamath). There is a stronger version of NBG called Morse-Kelley (axiom system MK in [Mendelson] p. 287). Russell himself continued in a different direction, avoiding the paradox with his "theory of types." Quine extended Russell's ideas to formulate the very strong New Foundations set theory (axiom system NF of [Quine] p. 331). In NF, the collection of all sets is a set, contradicting ZF and NBG set theories, and it has other bizarre consequences: when sets become too huge (beyond the size of those used in standard mathematics), the Axiom of Choice ac4 4738 and Cantor's Theorem canth 3905 are provably false! (See ncanth 3906 for some intuition behind the latter.) Nonetheless, NF has not been shown to be inconsistent and has its advocates - who's to say which set theory is "right"? NF is finitely axiomatizable and can be encoded in Metamath using the axioms from T. Hailperin, "A set of axioms for logic," J. Symb. Logic 9:1-19 (1944). Under our ZF set theory, every set is a member of the Russell class by elirrv 4586 (derived from the Axiom of Regularity), so for us the Russell class equals the universe V.
|- {x | x e/ x} e/ V
Proper substitution of classes for sets
Theorem	sbhypf 1937	Introduce an explicit substitution into an implicit substitution hypothesis.
|- (ps -> A.xps)   &   |- (x = A -> (ph <-> ps))   =>   |- (y = A -> ([y / x]ph <-> ps))
Theorem	sbhyp 1938	Change variable of an implicit substitution hypothesis, introducing an explicit substitution. (Contributed by Raph Levien, 10-Apr-2004.)
|- (x = A -> (ph <-> ps))   =>   |- (y = A -> ([y / x]ph <-> ps))
Theorem	sbralie 1939	Implicit to explicit substitution that swaps variables in a quantified expression.
|- (x = y -> (ph <-> ps))   =>   |- ([x / y]A.x e. y ph <-> A.y e. x ps)
Definition	df-sbc 1940	Define the proper substitution of a class for a set. This definition applies to proper classes but is not meaningful in that case (and does not produce the same results as Definition 6.6 of [Quine] p. 42). This definition is somewhat arbitrary in how it behaves with proper classes - e.g., we could have used sbc6 1955, which yields a different result for proper classes. In order to allow for a possible alternate but conflicting definition in the future, we will not commit to any specific proper class behavior. Instead, we will use this definition only to prove dfsbcq 1941, which will in turn serve as the starting point for all theorems based on the definition. Note: this definition extends or "overloads" df-sb 1172 which (via df-clab 1464) becomes a special case of it, so a careful metalogical soundness justification, outside of Metamath, is needed for complete rigor; alternately, we could treat this definition as a new axiom. The related definition df-csb 2000 defines proper substitution into a class variable (as opposed to a wff variable).
|- ([A / x]ph <-> A e. {x | ph})
Theorem	dfsbcq 1941	This theorem, which is similar to Theorem 6.7 of [Quine] p. 42, provides us a weak definition of the proper substitution of a class for a set that we will use in place of df-sbc 1940 above. We derive all our results from starting from here instead of df-sbc 1940. As a consequence we can derive elabs 1964, which is a weaker version of df-sbc 1940 that leaves substitution undefined when A is a proper class. We thus leave unspecified the "official" behavior for proper classes, which could be as in the sbc5 1954 assertion (always false) or as in sbc6 1955 (always true) or some more meaningful possibility in the future, that some clever person may discover, that is closer to Quine's definition. (Quine's actual definition cannot be expressed directly in our formal system.)
|- (A = B -> ([A / x]ph <-> [B / x]ph))
Theorem	sbceq1a 1942	Equality theorem for class substitution.
|- (x = A -> (ph <-> [A / x]ph))
Theorem	a4sbc 1943	Specialization: if a formula is true for all sets, it is true for any class which is a set. Similar to Theorem 6.11 of [Quine] p. 44. See also stdpc4 1185 and ra4sbc