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-10700 108 10701-10782

<

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

Type	Label	Description
Statement
Theorem	zfrep4 2701	A version of Replacement using class abstractions.
|- {x | ph} e. V   &   |- (ph -> E.zA.y(ps -> y = z))   =>   |- {y | E.x(ph /\ ps)} e. V
Derive the Axiom of Separation
Theorem	axsep 2702	Separation Scheme, which is an axiom scheme of Zermelo's original theory. Scheme Sep of [BellMachover] p. 463. As we show here, it is redundant if we assume Replacement in the form of ax-rep 2693. Some textbooks present Separation as a separate axiom scheme in order to show that much of set theory can be derived without the stronger Replacement. The Separation Scheme is a weak form of Frege's Axiom of Comprehension, conditioning it (with x e. z) so that it asserts the existence of a collection only if it is smaller than some other collection z that already exists. This prevents Russell's paradox ru 1938. In some texts, this scheme is called "Aussonderung" or the Subset Axiom. The variable x can appear free in the wff ph, which in textbooks is often written ph(x). To specify this in the Metamath language, we omit the distinct variable requirement ($d) that x not appear in ph. For a version using a class variable, see zfauscl 2705, which requires the Axiom of Extensionality as well as Replacement for its derivation. If we omit the requirement that y not occur in ph, we can derive a contradiction, as notzfaus 2741 shows (contradicting zfauscl 2705). However, as axsep2 2704 shows, we can eliminate the restriction that z not occur in ph. Note: the distinct variable restriction that z not occur in ph is actually redundant in this particular proof, but we keep it since its purpose is to demonstrate the derivation of the exact ax-sep 2703 from ax-rep 2693. This theorem should not be referenced by any proof. Instead, use ax-sep 2703 below so that the uses of the Axiom of Separation can be more easily identified.
|- E.yA.x(x e. y <-> (x e. z /\ ph))
Axiom	ax-sep 2703	The Axiom of Separation of ZF set theory. It was derived as axsep 2702 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily.
|- E.yA.x(x e. y <-> (x e. z /\ ph))
Theorem	axsep2 2704	A less restrictive version of the Separation Scheme axsep 2702, where variables x and z can both appear free in the wff ph, which can therefore be thought of as ph(x, z). This version was derived from the more restrictive ax-sep 2703 with no additional set theory axioms.
|- E.yA.x(x e. y <-> (x e. z /\ ph))
Theorem	zfauscl 2705	Separation Scheme using a class variable. To derive this from ax-sep 2703, we invoke the Axiom of Extensionality (indirectly via vtocl 1842), 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 2741 shows.
|- A e. V   =>   |- E.yA.x(x e. y <-> (x e. A /\ ph))
Theorem	bm1.3ii 2706	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 2707	Show the uniqueness of the empty set (using the Axiom of Extensionality via bm1.1 1462 to strengthen axnul 2709).
|- E.xA.y -. y e. x   =>   |- E!xA.y -. y e. x
Theorem	axnul2 2708	Prove axnul 2709 directly from ax-rep 2693 without using any equality axioms (ax-9 965 thru ax-16 1210). The wff x = x substituted for ph in the ax-rep 2693 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 2709	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 2703. 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 2707). This proof, suggested by Jeff Hoffman (3-Feb-2008), does not require the set existence axiom ax-9 965, unlike some empty set existence proofs (such as the remark in [Kunen] p. 11). However, it uses ax-4 973, 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 972, which shows the redundancy of ax-4 973, depends on ax-9 965 for its proof. See axnul2 2708 for a similar proof directly from ax-rep 2693. This theorem should not be referenced by any proof. Instead, use ax-nul 2710 below so that the uses of the Null Set Axiom can be more easily identified.
|- E.xA.y -. y e. x
Axiom	ax-nul 2710	The Null Set Axiom of ZF set theory. It was derived as axnul 2709 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 2711	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 2710.
|- (/) e. V
Theorems requiring subset and intersection existence
Theorem	nalset 2712	No set contains all sets. Theorem 41 of [Suppes] p. 30.
|- -. E.xA.y y e. x
Theorem	nvelv 2713	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 2714	The universal class doesn't belong to any class. (Contributed by FL, 31-Dec-2006.)
|- -. V e. A
Theorem	vnex 2715	The universal class does not exist.
|- -. E.x x = V
Theorem	inex1 2716	Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22.
|- A e. V   =>   |- (A i^i B) e. V
Theorem	inex2 2717	Separation Scheme (Aussonderung) using class notation.
|- A e. V   =>   |- (B i^i A) e. V
Theorem	inex1g 2718	Closed-form, generalized Separation Scheme.
|- (A e. C -> (A i^i B) e. V)
Theorem	ssex 2719	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 2703 (a.k.a. Subset Axiom).
|- B e. V   =>   |- (A (_ B -> A e. V)
Theorem	ssexi 2720	The subset of a set is also a set.
|- B e. V   &   |- A (_ B   =>   |- A e. V
Theorem	ssexg 2721	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 2722	Existence of a difference.
|- (A e. C -> (A \ B) e. V)
Theorem	zfausab 2723	Separation Scheme in terms of a class abstraction.
|- A e. V   =>   |- {x | (x e. A /\ ph)} e. V
Theorem	rabexg 2724	Separation Scheme in terms of a restricted class abstraction.
|- (A e. B -> {x e. A | ph} e. V)
Theorem	rabex 2725	Separation Scheme in terms of a restricted class abstraction.
|- A e. V   =>   |- {x e. A | ph} e. V
Theorem	elssabg 2726	Membership in a class abstraction involving a subset. Unlike elabg 1899, 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 2727	Membership in a power class. Theorem 86 of [Suppes] p. 47.
|- (B e. C -> (A e. P~B <-> A (_ B))
Theorem	elpw2 2728	Membership in a power class. Theorem 86 of [Suppes] p. 47.
|- B e. V   =>   |- (A e. P~B <-> A (_ B)
Theorem	intex 2729	The intersection of a non-empty class exists. Exercise 5 of [TakeutiZaring] p. 44 and its converse.
|- (A =/= (/) <-> |^|A e. V)
Theorem	intnex 2730	If a class intersection is not a set, it must be the universe.
|- (-. |^|A e. V <-> |^|A = V)
Theorem	intexab 2731	The intersection of a non-empty class abstraction exists.
|- (E.xph <-> |^|{x | ph} e. V)
Theorem	intexrab 2732	The intersection of a non-empty restricted class abstraction exists.
|- (E.x e. A ph <-> |^|{x e. A | ph} e. V)
Theorem	intabs 2733	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 2734	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 2735	Equality theorem based on class2set 2734. (The proof was shortened by Raph Levien, 30-Jun-2006.)
|- (A e. B -> {x e. A | A e. V} = A)
Theorem	0elpw 2736	Every power class contains the empty set.
|- (/) e. P~A
Theorem	0nep0 2737	The empty set and its power set are not equal.
|- (/) =/= {(/)}
Theorem	0inp0 2738	Something cannot be equal to both the null set and the power set of the null set.
|- (A = (/) -> -. A = {(/)})
Theorem	unidif0 2739	The removal of the empty set from a class does not affect its union.
|- U.(A \ {(/)}) = U.A
Theorem	iin0 2740	An indexed intersection of the empty set, with a non-empty index set, is empty.
|- (A =/= (/) <-> |^|_x e. A (/) = (/))
Theorem	notzfaus 2741	In the Separation Scheme zfauscl 2705, 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 2742	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 2744 states that the power set itself exists. A version using class notation is pwex 2745.
|- E.yA.z(A.w(w e. z -> w e. x) -> z e. y)
Theorem	axpow 2743	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 2744	A variant of the Axiom of Power Sets ax-pow 2742. 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 2745	Power set axiom expressed in class notation. Axiom 4 of [TakeutiZaring] p. 17.
|- A e. V   =>   |- P~A e. V
Theorem	pwexg 2746	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 2747	Existence of a class of subsets.
|- (A e. B -> {x | (x (_ A /\ ph)} e. V)
Theorem	dtruALT 2748	A version of dtru 2772 ("two things exist") proved directly from the axioms (no set theory definitions).
|- -. A.x x = y
Theorem	ax16b 2749	This theorem shows that axiom ax-16 1210 is redundant in the presence of theorem dtruALT 2748, 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 2750	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 2777, Replacement is not needed.
|- {A} e. V
Theorem	el 2751	Every set is an element of some other set.
|- E.y x e. y
Theorem	snelpw 2752	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 2753	Substitution expressed in terms of quantification over a singleton.
|- (A e. B -> ([A / x]ph <-> A.x e. {A}ph))
Theorem	rext 2754	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 2755	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 2756	A class equals the union of its power class. Exercise 6(a) of [Enderton] p. 38.
|- U.P~A = A
Theorem	pwuni 2757	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 2758	Subclass relationship for power class and union.
|- (A (_ P~B <-> U.A (_ B)
Theorem	pwel 2759	Membership of a power class. Exercise 10 of [Enderton] p. 26.
|- (A e. B -> P~A e. P~P~U.B)
Theorem	pwssb 2760	Two ways to express a collection of subclasses.
|- (A (_ P~B <-> A.x e. A x (_ B)
Theorem	elpwuni 2761	Relationship for power class and union.
|- (B e. A -> (A (_ P~B <-> U.A = B))
Theorem	ssextss 2762	An extensionality-like principle defining subclass in terms of subsets.
|- (A (_ B <-> A.x(x (_ A -> x (_ B))
Theorem	ssext 2763	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 2764	Negation of subclass relationship. Compare nss 2113.
|- (-. A (_ B <-> E.x(x (_ A /\ -. x (_ B))
Theorem	pweqb 2765	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 2766	"At most one" existence implies a class abstraction exists.
|- (E*xph -> {x | ph} e. V)
Theorem	euabex 2767	The abstraction of a wff with existential uniqueness exists.
|- (E!xph -> {x | ph} e. V)
Theorem	nnullss 2768	A non-empty class (even if proper) has a non-empty subset.
|- (A =/= (/) -> E.x(x (_ A /\ x =/= (/)))
Theorem	exss 2769	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 2770	The power set of the empty set is a set.
|- {(/)} e. V
Theorem	pp0ex 2771	The power set of the power set of the empty set is a set.
|- {(/), {(/)}} e. V
Theorem	dtru 2772	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 1127. Assuming that ZF set theory is consistent, we cannot prove this theorem unless we specify that x and y be distinct. Specifically, theorem cla4ev 1869 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 2748 for a version proved without using ax-16 1210, ax-ext 1459, or ax-sep 2703.
|- -. A.x x = y
Theorem	dtrucor 2773	Corollary of dtru 2772. 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 2774.
|- x = y   =>   |- x =/= y
Theorem	dtrucor2 2774	The theorem form of the deduction dtrucor 2773 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 2775	Demonstration of a theorem that requires x and y to be distinct, but no others. Compare dvdemo2 2776.
|- E.x(x = y -> z e. x)
Theorem	dvdemo2 2776