mmtheorems28 - 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-10487

Statement List for Metamath Proof Explorer - 2701-2800 - Page 28 of 105

Type	Label	Description
Statement
Theorem	intabs 2701	Absorption of a redundant conjunct in the intersection of a class abstraction.
|- (x = y -> (ph <-> ps))   &   |- (x = |^|{y | ps} -> (ph <-> ch))   &   |- (|^|{y | ps} (_ A /\ ch)   =>   |- |^|{x | (x (_ A /\ ph)} = |^|{x | ph}
Theorems requiring empty set existence
Theorem	class2set 2702	Construct, from any class A, a set equal to it when the class exists and equal to the empty set when the class is proper. This theorem shows that the constructed set always exists.
|- {x e. A | A e. V} e. V
Theorem	class2seteq 2703	Equality theorem based on class2set 2702. (The proof was shortened by Raph Levien, 30-Jun-2006.)
|- (A e. B -> {x e. A | A e. V} = A)
Theorem	0elpw 2704	Every power class contains the empty set.
|- (/) e. P~A
Theorem	0nep0 2705	The empty set and its power set are not equal.
|- (/) =/= {(/)}
Theorem	0inp0 2706	Something cannot be equal to both the null set and the power set of the null set.
|- (A = (/) -> -. A = {(/)})
Theorem	unidif0 2707	The removal of the empty set from a class does not affect its union.
|- U.(A \ {(/)}) = U.A
Theorem	iin0 2708	An indexed intersection of the empty set, with a non-empty index set, is empty.
|- (A =/= (/) <-> |^|_x e. A (/) = (/))
Theorem	notzfaus 2709	In the Separation Scheme zfauscl 2673, we require that y not occur in ph (which can be generalized to "not be free in"). Here we show that a contradiction can result if we omit this requirement.
|- A = {(/)}   &   |- (ph <-> -. x e. y)   =>   |- -. E.yA.x(x e. y <-> (x e. A /\ ph))
ZF Set Theory - add the Axiom of Power Sets
Introduce the Axiom of Power Sets
Axiom	ax-pow 2710	Axiom of Power Sets. An axiom of Zermelo-Fraenkel set theory. It states that a set y exists that includes the power set of a given set x i.e. the collection of all subsets of x. The variant axpow2 2712 states that the power set itself exists. A version using class notation is pwex 2713.
|- E.yA.z(A.w(w e. z -> w e. x) -> z e. y)
Theorem	axpow 2711	Axiom of Power Sets expressed with fewest number of different variables.
|- E.xA.y(A.x(x e. y -> x e. z) -> y e. x)
Theorem	axpow2 2712	A variant of the Axiom of Power Sets ax-pow 2710. For any set x, there exists a set y whose members are exactly the subsets of x i.e. the power set of x. Axiom Pow of [BellMachover] p. 466.
|- E.yA.z(z e. y <-> A.w(w e. z -> w e. x))
Theorem	pwex 2713	Power set axiom expressed in class notation. Axiom 4 of [TakeutiZaring] p. 17.
|- A e. V   =>   |- P~A e. V
Theorem	pwexg 2714	Power set axiom expressed in class notation, with the sethood requirement as an antecedent. Axiom 4 of [TakeutiZaring] p. 17.
|- (A e. B -> P~A e. V)
Theorem	abssexg 2715	Existence of a class of subsets.
|- (A e. B -> {x | (x (_ A /\ ph)} e. V)
Theorem	dtruALT 2716	A version of dtru 2740 ("two things exist") proved directly from the axioms (no set theory definitions).
|- -. A.x x = y
Theorem	ax16b 2717	This theorem shows that axiom ax-16 1194 is redundant in the presence of theorem dtruALT 2716, which states simply that at least two things exist. This justifies the remark at http://us.metamath.org/mpegif/mmzfcnd.html#twoness (which links to this theorem).
|- (A.x x = y -> (ph -> A.xph))
Theorem	snex 2718	A singleton is a set. Theorem 7.13 of [Quine] p. 51, but proved using only Extensionality, Power Set, and Separation. Unlike the proof of zfpair 2745, Replacement is not needed.
|- {A} e. V
Theorem	el 2719	Every set is an element of some other set.
|- E.y x e. y
Theorem	snelpw 2720	A singleton of a set belongs to the power class of a class containing the set.
|- A e. V   =>   |- (A e. B <-> {A} e. P~B)
Theorem	sbcsng 2721	Substitution expressed in terms of quantification over a singleton.
|- (A e. B -> ([A / x]ph <-> A.x e. {A}ph))
Theorem	rext 2722	A theorem similar to extensionality, requiring the existence of a singleton. Exercise 8 of [TakeutiZaring] p. 16.
|- (A.z(x e. z -> y e. z) -> x = y)
Theorem	sspwb 2723	Classes are subclasses if and only if their power classes are subclasses. Exercise 18 of [TakeutiZaring] p. 18.
|- (A (_ B <-> P~A (_ P~B)
Theorem	unipw 2724	A class equals the union of its power class. Exercise 6(a) of [Enderton] p. 38.
|- U.P~A = A
Theorem	pwuni 2725	A class is a subclass of the power class of its union. Exercise 6(b) of [Enderton] p. 38.
|- A (_ P~U.A
Theorem	sspwuni 2726	Subclass relationship for power class and union.
|- (A (_ P~B <-> U.A (_ B)
Theorem	pwel 2727	Membership of a power class. Exercise 10 of [Enderton] p. 26.
|- (A e. B -> P~A e. P~P~U.B)
Theorem	pwssb 2728	Two ways to express a collection of subclasses.
|- (A (_ P~B <-> A.x e. A x (_ B)
Theorem	elpwuni 2729	Relationship for power class and union.
|- (B e. A -> (A (_ P~B <-> U.A = B))
Theorem	ssextss 2730	An extensionality-like principle defining subclass in terms of subsets.
|- (A (_ B <-> A.x(x (_ A -> x (_ B))
Theorem	ssext 2731	An extensionality-like principle that uses the subset instead of the membership relation: two classes are equal iff they have the same subsets.
|- (A = B <-> A.x(x (_ A <-> x (_ B))
Theorem	nssss 2732	Negation of subclass relationship. Compare nss 2084.
|- (-. A (_ B <-> E.x(x (_ A /\ -. x (_ B))
Theorem	pweqb 2733	Classes are equal if and only if their power classes are equal. Exercise 19 of [TakeutiZaring] p. 18.
|- (A = B <-> P~A = P~B)
Theorem	moabex 2734	"At most one" existence implies a class abstraction exists.
|- (E*xph -> {x | ph} e. V)
Theorem	euabex 2735	The abstraction of a wff with existential uniqueness exists.
|- (E!xph -> {x | ph} e. V)
Theorem	nnullss 2736	A non-empty class (even if proper) has a non-empty subset.
|- (A =/= (/) -> E.x(x (_ A /\ x =/= (/)))
Theorem	exss 2737	Restricted existence in a class (even if proper) implies restricted existence in a subset.
|- (E.x e. A ph -> E.y(y (_ A /\ E.x e. y ph))
Theorem	p0ex 2738	The power set of the empty set is a set.
|- {(/)} e. V
Theorem	pp0ex 2739	The power set of the power set of the empty set is a set.
|- {(/), {(/)}} e. V
Theorem	dtru 2740	At least two sets exist (or in terms of first-order logic, the universe of discourse has two or more objects). Note that we may not substitute the same variable for both x and y (as indicated by the distinct variable requirement), for otherwise we would contradict stdpc6 1114. Assuming that ZF set theory is consistent, we cannot prove this theorem unless we specify that x and y be distinct. Specifically, theorem cla4ev 1842 requires that x must not occur in the subexpression -. y = {(/)} in step 4 nor in the subexpression -. y = (/) in step 9. The proof verifier will require that x and y be in a distinct variable group to ensure this. You can check this by deleting the $d statement in set.mm and rerunning the verifier, which will print a detailed explanation of the distinct variable violation. See dtruALT 2716 for a version proved without using ax-16 1194, ax-ext 1436, or ax-sep 2671.
|- -. A.x x = y
Theorem	dtrucor 2741	Corollary of dtru 2740. This example illustrates the danger of blindly trusting the standard Deduction Theorem without accounting for free variables: the theorem form of this deduction is not valid, as shown by dtrucor2 2742.
|- x = y   =>   |- x =/= y
Theorem	dtrucor2 2742	The theorem form of the deduction dtrucor 2741 leads to a contradiction, as mentioned in the "Wrong!" example at http://us.metamath.org/mpegif/mmdeduction.html#bad.
|- (x = y -> x =/= y)   =>   |- (ph /\ -. ph)
Theorem	dvdemo1 2743	Demonstration of a theorem that requires x and y to be distinct, but no others. Compare dvdemo2 2744.
|- E.x(x = y -> z e. x)
Theorem	dvdemo2 2744	Demonstration of a theorem that requires x and z to be distinct, but no others. Compare dvdemo1 2743.
|- E.x(x = y -> z e. x)
Derive the Axiom of Pairing
Theorem	zfpair 2745	The Axiom of Pairing of Zermelo-Fraenkel set theory. Axiom 2 of [TakeutiZaring] p. 15. In some textbooks this is stated as a separate axiom; here we show it is redundant since it can be derived from the other axioms. This theorem should not be referenced by any proof other than axpr 2746. Instead, use zfpair2 2748 below so that the uses of the Axiom of Pairing can be more easily identified.
|- {x, y} e. V
Theorem	axpr 2746	Unabbreviated version of the Axiom of Pairing of ZF set theory, derived as a theorem from the other axioms. . This theorem should not be referenced by any proof. Instead, use ax-pr 2747 below so that the uses of the Axiom of Pairing can be more easily identified.
|- E.zA.w((w = x \/ w = y) -> w e. z)
Axiom	ax-pr 2747	The Axiom of Pairing of ZF set theory. It was derived as theorem axpr 2746 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily.
|- E.zA.w((w = x \/ w = y) -> w e. z)
Theorem	zfpair2 2748	Derive the abbreviated version of the Axiom of Pairing from ax-pr 2747. See zfpair 2745 for its derivation from the other axioms.
|- {x, y} e. V
Theorem	prex 2749	The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51. By virtue of its definition, an unordered pair remains a set (even though no longer a pair) even when its components are proper classes (see prprc 2424), so we can dispense with hypotheses requiring them to be sets.
|- {A, B} e. V
Theorem	opex 2750	An ordered pair of classes is a set. Exercise 7 of [TakeutiZaring] p. 16.
|- <.A, B>. e. V
Theorem	elop 2751	An ordered pair has two elements. Exercise 3 of [TakeutiZaring] p. 15.
|- A e. V   =>   |- (A e. <.B, C>. <-> (A = {B} \/ A = {B, C}))
Theorem	opi1 2752	One of the two elements in an ordered pair.
|- {A} e. <.A, B>.
Theorem	opi2 2753	One of the two elements of an ordered pair.
|- {A, B} e. <.A, B>.
Ordered pair theorem
Theorem	opth 2754	The ordered pair theorem. If two ordered pairs are equal, their first elements are equal and their second elements are equal. Exercise 6 of [TakeutiZaring] p. 16. Note that C is not required to be a set due to a peculiarity of our specific ordered pair definition.
|- A e. V   &   |- B e. V   &   |- D e. V   =>   |- (<.A, B>. = <.C, D>. <-> (A = C /\ B = D))
Theorem	opthg 2755	Ordered pair theorem.
|- A e. V   &   |- B e. V   =>   |- (D e. R -> (<.A, B>. = <.C, D>. <-> (A = C /\ B = D)))
Theorem	opthgg 2756	Ordered pair theorem. C is not required to be a set under our specific ordered pair definition.
|- ((A e. R /\ B e. S /\ D e. T) -> (<.A, B>. = <.C, D>. <-> (A = C /\ B = D)))
Theorem	otthg 2757	Ordered triple theorem.
|- A e. V   &   |- B e. V   &   |- R e. V   =>   |- ((D e. F /\ S e. G) -> (<.<.A, B>., R>. = <.<.C, D>., S>. <-> (A = C /\ B = D /\ R = S)))
Theorem	eqvinop 2758	A variable introduction law for ordered pairs. Analogue of Lemma 15 of [Monk2] p. 109.
|- B e. V   &   |- C e. V   =>   |- (A = <.B, C>. <-> E.xE.y(A = <.x, y>. /\ <.x, y>. = <.B, C>.))
Theorem	copsexg 2759	Substitution of class A for ordered pair <.x, y>..
|- (A = <.x, y>. -> (ph <-> E.xE.y(A = <.x, y>. /\ ph)))
Theorem	copsex2g 2760	Implicit substitution inference for ordered pairs.
|- ((x = A /\ y = B) -> (ph <-> ps))   =>   |- ((A e. C /\ B e. D) -> (E.xE.y(<.A, B>. = <.x, y>. /\ ph) <-> ps))
Theorem	copsex4g 2761	An implicit substitution inference for 2 ordered pairs.
|- (((x = A /\ y = B) /\ (z = C /\ w = D)) -> (ph <-> ps))   =>   |- (((A e. R /\ B e. S) /\ (C e. R /\ D e. S)) -> (E.xE.yE.zE.w((<.A, B>. = <.x, y>. /\ <.C, D>. = <.z, w>.) /\ ph) <-> ps))
Theorem	opnz 2762	An ordered pair is not empty.
|- -. <.A, B>. = (/)
Theorem	opprc1b 2763	A property of an ordered pair of proper classes (due to our particular definition of ordered pair).
|- (-. A e. V <-> (/) e. <.A, B>.)
Theorem	opprc3 2764	A property of an ordered pair of proper classes (due to our particular definition of ordered pair).
|- ((-. A e. V /\ -. B e. V) <-> <.A, B>. = {(/)})
Theorem	opth2 2765	Equality of the second members of equal ordered pairs. Because of our particular ordered pair definition, equality holds whether or not the first members are sets.
|- B e. V   &   |- D e. V   =>   |- (<.A, B>. = <.C, D>. -> B = D)
Theorem	moop2 2766	"At most one" property of an ordered pair. The proof is a little tricky because we do not place any restrictions on class B.
|- E*x A = <.B, x>.
Theorem	mosubopt 2767	"At most one" remains true inside ordered pair quantification.
|- (A.yA.zE*xph -> E*xE.yE.z(A = <.y, z>. /\ ph))
Theorem	mosubop 2768	"At most one" remains true inside ordered pair quantification.
|- E*xph   =>   |- E*xE.yE.<