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-10500 106 10501-10600 107 10601-10670

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

Type	Label	Description
Statement
Theorem	zfauscl 2701	Separation Scheme using a class variable. To derive this from ax-sep 2699, we invoke the Axiom of Extensionality (indirectly via vtocl 1839), which is needed for the justification of class variable notation. If we omit the requirement that y not occur in ph, we can derive a contradiction, as notzfaus 2737 shows.
|- A e. V   =>   |- E.yA.x(x e. y <-> (x e. A /\ ph))
Theorem	bm1.3ii 2702	Convert implication to equivalence using Aussonderung. Similar to Theorem 1.3ii of [BellMachover] p. 463.
|- E.xA.y(ph -> y e. x)   =>   |- E.xA.y(y e. x <-> ph)
Derive the Null Set Axiom
Theorem	zfnuleu 2703	Show the uniqueness of the empty set (using the Axiom of Extensionality via bm1.1 1461 to strengthen axnul 2705).
|- E.xA.y -. y e. x   =>   |- E!xA.y -. y e. x
Theorem	axnul2 2704	Prove axnul 2705 directly from ax-rep 2689 without using any equality axioms (ax-9 964 thru ax-16 1209). The wff x = x substituted for ph in the ax-rep 2689 instance is arbitrary. Here, we don't need to know if x = x is true or false, only that it's not both. (Contributed by Jeff Hoffman, 4-Feb-2008.)
|- E.xA.y -. y e. x
Theorem	axnul 2705	The Null Set Axiom of ZF set theory: there exists a set with no elements. Axiom of Empty Set of [Enderton] p. 18. In some textbooks, this is presented as a separate axiom; here we show it can be derived from Separation ax-sep 2699. This version of the Null Set Axiom tells us that at least one empty set exists, but does not tells us that it is unique - we need the Axiom of Extensionality to do that (see zfnuleu 2703). This proof, suggested by Jeff Hoffman (3-Feb-2008), does not require the set existence axiom ax-9 964, unlike some empty set existence proofs (such as the remark in [Kunen] p. 11). However, it uses ax-4 972, which also presupposes the existence of at least one set, i.e it does not hold in a "free logic" valid in empty domains. Theorem ax4 971, which shows the redundancy of ax-4 972, depends on ax-9 964 for its proof. See axnul2 2704 for a similar proof directly from ax-rep 2689. This theorem should not be referenced by any proof. Instead, use ax-nul 2706 below so that the uses of the Null Set Axiom can be more easily identified.
|- E.xA.y -. y e. x
Axiom	ax-nul 2706	The Null Set Axiom of ZF set theory. It was derived as axnul 2705 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily.
|- E.xA.y -. y e. x
Theorem	0ex 2707	The Null Set Axiom of ZF set theory: the empty set exists. Corollary 5.16 of [TakeutiZaring] p. 20. For the unabbreviated version, see ax-nul 2706.
|- (/) e. V
Theorems requiring subset and intersection existence
Theorem	nalset 2708	No set contains all sets. Theorem 41 of [Suppes] p. 30.
|- -. E.xA.y y e. x
Theorem	nvelv 2709	The universal class is not a member of itself (and thus is not a set). Proposition 5.21 of [TakeutiZaring] p. 21; our proof, however, does not depend on the Axiom of Regularity.
|- -. V e. V
Theorem	nvel 2710	The universal class doesn't belong to any class. (Contributed by FL, 31-Dec-2006.)
|- -. V e. A
Theorem	vnex 2711	The universal class does not exist.
|- -. E.x x = V
Theorem	inex1 2712	Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22.
|- A e. V   =>   |- (A i^i B) e. V
Theorem	inex2 2713	Separation Scheme (Aussonderung) using class notation.
|- A e. V   =>   |- (B i^i A) e. V
Theorem	inex1g 2714	Closed-form, generalized Separation Scheme.
|- (A e. C -> (A i^i B) e. V)
Theorem	ssex 2715	The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22. This is one way to express the Axiom of Separation ax-sep 2699 (a.k.a. Subset Axiom).
|- B e. V   =>   |- (A (_ B -> A e. V)
Theorem	ssexi 2716	The subset of a set is also a set.
|- B e. V   &   |- A (_ B   =>   |- A e. V
Theorem	ssexg 2717	The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized).
|- ((A (_ B /\ B e. C) -> A e. V)
Theorem	difexg 2718	Existence of a difference.
|- (A e. C -> (A \ B) e. V)
Theorem	zfausab 2719	Separation Scheme in terms of a class abstraction.
|- A e. V   =>   |- {x | (x e. A /\ ph)} e. V
Theorem	rabexg 2720	Separation Scheme in terms of a restricted class abstraction.
|- (A e. B -> {x e. A | ph} e. V)
Theorem	rabex 2721	Separation Scheme in terms of a restricted class abstraction.
|- A e. V   =>   |- {x e. A | ph} e. V
Theorem	elssabg 2722	Membership in a class abstraction involving a subset. Unlike elabg 1896, A does not have to be a set.
|- (x = A -> (ph <-> ps))   =>   |- (B e. C -> (A e. {x | (x (_ B /\ ph)} <-> (A (_ B /\ ps)))
Theorem	elpw2g 2723	Membership in a power class. Theorem 86 of [Suppes] p. 47.
|- (B e. C -> (A e. P~B <-> A (_ B))
Theorem	elpw2 2724	Membership in a power class. Theorem 86 of [Suppes] p. 47.
|- B e. V   =>   |- (A e. P~B <-> A (_ B)
Theorem	intex 2725	The intersection of a non-empty class exists. Exercise 5 of [TakeutiZaring] p. 44 and its converse.
|- (A =/= (/) <-> |^|A e. V)
Theorem	intnex 2726	If a class intersection is not a set, it must be the universe.
|- (-. |^|A e. V <-> |^|A = V)
Theorem	intexab 2727	The intersection of a non-empty class abstraction exists.
|- (E.xph <-> |^|{x | ph} e. V)
Theorem	intexrab 2728	The intersection of a non-empty restricted class abstraction exists.
|- (E.x e. A ph <-> |^|{x e. A | ph} e. V)
Theorem	intabs 2729	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 2730	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 2731	Equality theorem based on class2set 2730. (The proof was shortened by Raph Levien, 30-Jun-2006.)
|- (A e. B -> {x e. A | A e. V} = A)
Theorem	0elpw 2732	Every power class contains the empty set.
|- (/) e. P~A
Theorem	0nep0 2733	The empty set and its power set are not equal.
|- (/) =/= {(/)}
Theorem	0inp0 2734	Something cannot be equal to both the null set and the power set of the null set.
|- (A = (/) -> -. A = {(/)})
Theorem	unidif0 2735	The removal of the empty set from a class does not affect its union.
|- U.(A \ {(/)}) = U.A
Theorem	iin0 2736	An indexed intersection of the empty set, with a non-empty index set, is empty.
|- (A =/= (/) <-> |^|_x e. A (/) = (/))
Theorem	notzfaus 2737	In the Separation Scheme zfauscl 2701, 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 2738	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 2740 states that the power set itself exists. A version using class notation is pwex 2741.
|- E.yA.z(A.w(w e. z -> w e. x) -> z e. y)
Theorem	axpow 2739	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 2740	A variant of the Axiom of Power Sets ax-pow 2738. 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 2741	Power set axiom expressed in class notation. Axiom 4 of [TakeutiZaring] p. 17.
|- A e. V   =>   |- P~A e. V
Theorem	pwexg 2742	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 2743	Existence of a class of subsets.
|- (A e. B -> {x | (x (_ A /\ ph)} e. V)
Theorem	dtruALT 2744	A version of dtru 2768 ("two things exist") proved directly from the axioms (no set theory definitions).
|- -. A.x x = y
Theorem	ax16b 2745	This theorem shows that axiom ax-16 1209 is redundant in the presence of theorem dtruALT 2744, 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 2746	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 2773, Replacement is not needed.
|- {A} e. V
Theorem	el 2747	Every set is an element of some other set.
|- E.y x e. y
Theorem	snelpw 2748	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 2749	Substitution expressed in terms of quantification over a singleton.
|- (A e. B -> ([A / x]ph <-> A.x e. {A}ph))
Theorem	rext 2750	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 2751	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 2752	A class equals the union of its power class. Exercise 6(a) of [Enderton] p. 38.
|- U.P~A = A
Theorem	pwuni 2753	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 2754	Subclass relationship for power class and union.
|- (A (_ P~B <-> U.A (_ B)
Theorem	pwel 2755	Membership of a power class. Exercise 10 of [Enderton] p. 26.
|- (A e. B -> P~A e. P~P~U.B)
Theorem	pwssb 2756	Two ways to express a collection of subclasses.
|- (A (_ P~B <-> A.x e. A x (_ B)
Theorem	elpwuni 2757	Relationship for power class and union.
|- (B e. A -> (A (_ P~B <-> U.A = B))
Theorem	ssextss 2758	An extensionality-like principle defining subclass in terms of subsets.
|- (A (_ B <-> A.x(x (_ A -> x (_ B))
Theorem	ssext 2759	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 2760	Negation of subclass relationship. Compare nss 2110.
|- (-. A (_ B <-> E.x(x (_ A /\ -. x (_ B))
Theorem	pweqb 2761	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 2762	"At most one" existence implies a class abstraction exists.
|- (E*xph -> {x | ph} e. V)
Theorem	euabex 2763	The abstraction of a wff with existential uniqueness exists.
|- (E!xph -> {x | ph} e. V)
Theorem	nnullss 2764	A non-empty class (even if proper) has a non-empty subset.
|- (A =/= (/) -> E.x(x (_ A /\ x =/= (/)))
Theorem	exss 2765	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 2766	The power set of the empty set is a set.
|- {(/)} e. V
Theorem	pp0ex 2767	The power set of the power set of the empty set is a set.
|- {(/), {(/)}} e. V
Theorem	dtru 2768	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 1126. Assuming that ZF set theory is consistent, we cannot prove this theorem unless we specify that x and y be distinct. Specifically, theorem cla4ev 1866 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 2744 for a version proved without using ax-16 1209, ax-ext 1458, or ax-sep 2699.
|- -. A.x x = y
Theorem	dtrucor 2769	Corollary of dtru 2768. 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 2770.
|- x = y   =>   |- x =/= y
Theorem	dtrucor2 2770	The theorem form of the deduction dtrucor 2769 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 2771	Demonstration of a theorem that requires x and y to be distinct, but no others. Compare dvdemo2 2772.
|- E.x(x = y -> z e. x)
Theorem	dvdemo2 2772	Demonstration of a theorem that requires x and z to be distinct, but no others. Compare dvdemo1 2771.
|- E.x(x = y -> z e. x)
Derive the Axiom of Pairing
Theorem	zfpair 2773	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 2774. Instead, use zfpair2 2776 below so that the uses of the Axiom of Pairing can be more easily identified.
|- {x, y} e. V
Theorem	axpr 2774	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 2775 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 2775	The Axiom of Pairing of ZF set theory. It was derived as theorem axpr 2774 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 2776	Derive the abbreviated version of the Axiom of Pairing from ax-pr 2775. See zfpair 2773 for its derivation from the other axioms.
|- {x, y} e. V
Theorem	prex 2777	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 2451), so we can dispense with hypotheses requiring them to be sets.
|- {A, B} e. V
Theorem	opex 2778	An ordered pair of classes is a set. Exercise 7 of [TakeutiZaring] p. 16.
|- <.A, B>. e. V
Theorem	elop 2779	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 2780	One of the two elements in an ordered pair.
|-