mmtheorems29 - 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-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Statement List for Metamath Proof Explorer - 2801-2900 - Page 29 of 123

Type	Label	Description
Statement
Theorem	elpw2g 2801	Membership in a power class. Theorem 86 of [Suppes] p. 47.
|- (B e. C -> (A e. P~B <-> A (_ B))
Theorem	elpw2 2802	Membership in a power class. Theorem 86 of [Suppes] p. 47.
|- B e. V   =>   |- (A e. P~B <-> A (_ B)
Theorem	intex 2803	The intersection of a non-empty class exists. Exercise 5 of [TakeutiZaring] p. 44 and its converse.
|- (A =/= (/) <-> |^|A e. V)
Theorem	intnex 2804	If a class intersection is not a set, it must be the universe.
|- (-. |^|A e. V <-> |^|A = V)
Theorem	intexab 2805	The intersection of a non-empty class abstraction exists.
|- (E.xph <-> |^|{x | ph} e. V)
Theorem	intexrab 2806	The intersection of a non-empty restricted class abstraction exists.
|- (E.x e. A ph <-> |^|{x e. A | ph} e. V)
Theorem	intabs 2807	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 2808	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 2809	Equality theorem based on class2set 2808. (The proof was shortened by Raph Levien, 30-Jun-2006.)
|- (A e. B -> {x e. A | A e. V} = A)
Theorem	0elpw 2810	Every power class contains the empty set.
|- (/) e. P~A
Theorem	0nep0 2811	The empty set and its power set are not equal.
|- (/) =/= {(/)}
Theorem	0inp0 2812	Something cannot be equal to both the null set and the power set of the null set.
|- (A = (/) -> -. A = {(/)})
Theorem	unidif0 2813	The removal of the empty set from a class does not affect its union.
|- U.(A \ {(/)}) = U.A
Theorem	iin0 2814	An indexed intersection of the empty set, with a non-empty index set, is empty.
|- (A =/= (/) <-> |^|_x e. A (/) = (/))
Theorem	notzfaus 2815	In the Separation Scheme zfauscl 2779, 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))
Theorem	intv 2816	The intersection of the universal class is empty.
|- |^|V = (/)
Theorem	axpweq 2817	Two equivalent ways to express the Power Set Axiom. Note that ax-pow 2818 is not used by the proof.
|- A e. V   =>   |- (P~A e. V <-> E.xA.y(A.z(z e. y -> z e. A) -> y e. x))
ZF Set Theory - add the Axiom of Power Sets
Introduce the Axiom of Power Sets
Axiom	ax-pow 2818	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 2820 states that the power set itself exists. A version using class notation is pwex 2823.
|- E.yA.z(A.w(w e. z -> w e. x) -> z e. y)
Theorem	zfpow 2819	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 2820	A variant of the Axiom of Power Sets ax-pow 2818 using subset notation. Problem in {BellMachover] p. 466.
|- E.yA.z(z (_ x -> z e. y)
Theorem	axpow3 2821	A variant of the Axiom of Power Sets ax-pow 2818. 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 (_ x <-> z e. y)
Theorem	el 2822	Every set is an element of some other set. See elALT 2827 for a shorter proof using more axioms.
|- E.y x e. y
Theorem	pwex 2823	Power set axiom expressed in class notation. Axiom 4 of [TakeutiZaring] p. 17.
|- A e. V   =>   |- P~A e. V
Theorem	pwexg 2824	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 2825	Existence of a class of subsets.
|- (A e. B -> {x | (x (_ A /\ ph)} e. V)
Theorem	snex 2826	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 2853, Replacement is not needed.
|- {A} e. V
Theorem	elALT 2827	Every set is an element of some other set. This has a shorter proof than el 2822 but uses more axioms.
|- E.y x e. y
Theorem	p0ex 2828	The power set of the empty set (the ordinal 1) is a set.
|- {(/)} e. V
Theorem	pp0ex 2829	The power set of the power set of the empty set (the ordinal 2) is a set.
|- {(/), {(/)}} e. V
Theorem	ord3ex 2830	The ordinal number 3 is a set, proved without the Axiom of Union ax-un 3089.
|- {(/), {(/)}, {(/), {(/)}}} e. V
Theorem	dtru 2831	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 1164. Assuming that ZF set theory is consistent, we cannot prove this theorem unless we specify that x and y be distinct. Specifically, theorem cla4ev 1915 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. This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-16 1247, ax-ext 1500, or ax-sep 2777. See dtruALT 2848 for a shorter proof using these axioms.
|- -. A.x x = y
Theorem	ax16b 2832	This theorem shows that axiom ax-16 1247 is redundant in the presence of theorem dtru 2831, 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	snelpw 2833	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	rext 2834	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 2835	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 2836	A class equals the union of its power class. Exercise 6(a) of [Enderton] p. 38. (The proof was shortened by Alan Sare, 28-Dec-2008.)
|- U.P~A = A
Theorem	pwuni 2837	A class is a subclass of the power class of its union. Exercise 6(b) of [Enderton] p. 38.
|- A (_ P~U.A
Theorem	pwel 2838	Membership of a power class. Exercise 10 of [Enderton] p. 26.
|- (A e. B -> P~A e. P~P~U.B)
Theorem	ssextss 2839	An extensionality-like principle defining subclass in terms of subsets.
|- (A (_ B <-> A.x(x (_ A -> x (_ B))
Theorem	ssext 2840	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 2841	Negation of subclass relationship. Compare nss 2165.
|- (-. A (_ B <-> E.x(x (_ A /\ -. x (_ B))
Theorem	pweqb 2842	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	intid 2843	The intersection of all sets to which a set belongs is the singleton of that set.
|- A e. V   =>   |- |^|{x | A e. x} = {A}
Theorem	moabex 2844	"At most one" existence implies a class abstraction exists.
|- (E*xph -> {x | ph} e. V)
Theorem	euabex 2845	The abstraction of a wff with existential uniqueness exists.
|- (E!xph -> {x | ph} e. V)
Theorem	nnullss 2846	A non-empty class (even if proper) has a non-empty subset.
|- (A =/= (/) -> E.x(x (_ A /\ x =/= (/)))
Theorem	exss 2847	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	dtruALT 2848	A version of dtru 2831 ("two things exist") with a shorter proof using more axioms.
|- -. A.x x = y
Theorem	dtrucor 2849	Corollary of dtru 2831. 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 2850.
|- x = y   =>   |- x =/= y
Theorem	dtrucor2 2850	The theorem form of the deduction dtrucor 2849 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 2851	Demonstration of a theorem that requires x and y to be distinct, but no others. Compare dvdemo2 2852.
|- E.x(x = y -> z e. x)
Theorem	dvdemo2 2852	Demonstration of a theorem that requires x and z to be distinct, but no others. Compare dvdemo1 2851.
|- E.x(x = y -> z e. x)
Derive the Axiom of Pairing
Theorem	zfpair 2853	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 2854. Instead, use zfpair2 2856 below so that the uses of the Axiom of Pairing can be more easily identified.
|- {x, y} e. V
Theorem	axpr 2854	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 2855 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 2855	The Axiom of Pairing of ZF set theory. It was derived as theorem axpr 2854 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 2856	Derive the abbreviated version of the Axiom of Pairing from ax-pr 2855. See zfpair 2853 for its derivation from the other axioms.
|- {x, y} e. V
Theorem	prex 2857	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 2517), so we can dispense with hypotheses requiring them to be sets.
|- {A, B} e. V
Theorem	opex 2858	An ordered pair of classes is a set. Exercise 7 of [TakeutiZaring] p. 16.
|- <.A, B>. e. V
Theorem	elop 2859	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 2860	One of the two elements in an ordered pair.
|- {A} e. <.A, B>.
Theorem	opi2 2861	One of the two elements of an ordered pair.
|- {A, B} e. <.A, B>.
Ordered pair theorem
Theorem	opth1 2862	Equality of the first members of equal ordered pairs, which holds whether or not the second members are sets.
|- A e. V   =>   |- (<.A, B>. = <.C, D>. -> A = C)
Theorem	opth 2863	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 2864	Ordered pair theorem.
|- A e. V   &   |- B e. V   =>   |- (D e. R -> (<.A, B>. = <.C, D>. <-> (A = C /\ B = D)))
Theorem	opthgg 2865	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 2866	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 2867	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 2868	Substitution of class A for ordered pair <.x, y>..
|- (A = <.x, y>. -> (ph <-> E.xE.y(A = <.x, y>. /\ ph)))
Theorem	copsex2g 2869	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 2870	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 2871	An ordered pair is not empty.
|- -. <.A, B>. = (/)
Theorem	opprc1b 2872	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 2873	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	opeqex 2874	Equivalence of existence implied by equality of ordered pairs.
|- (<.A, B>. = <.C, D>. -> (A e. V <-> C e. V))
Theorem	oteqex 2875	Equivalence of existence implied by equality of ordered triples.
|- (<.<.A, B>., C>. = <.<.R, S>., T>. -> (A e. V <-> R e. V))
Theorem	opth2 2876	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	opcom 2877	An ordered pair commutes iff its members are equal.
|- A e. V   =>   |- (<.A, B>. = <.B, A>. <-> A = B)
Theorem	moop2 2878	"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	opeqsn 2879	Equivalence for an ordered pair equal to a singleton.
|- A e. V   &   |- B e. V   &   |- C e. V   =>   |- (<.A, B>. = {C} <-> (A = B /\ C = {A}))
Theorem	opeqpr 2880	Equivalence for an ordered pair equal to an unordered pair.
|- C e. V   &   |- D e. V   =>   |- (<.A, B>. = {C, D} <-> ((C = {A} /\ D = {A, B}) \/ (C = {A, B} /\ D = {A})))
Theorem	mosubopt 2881	"At most one" remains true inside ordered pair quantification.
|- (A.yA.zE*xph -> E*xE.yE.z(A = <.y, z>. /\ ph))
Theorem	mosubop 2882	"At most one" remains true inside ordered pair quantification.
|- E*xph   =>   |- E*xE.yE.z(A = <.y, z>. /\ ph)
Theorem	euop2 2883	Transfer existential uniqueness to second member of an ordered pair.
|- (E!xE.y(x = <.A, y>. /\ ph) <-> E!yph)
Theorem	opthwiener 2884	Justification theorem for the ordered pair definition in Norbert Wiener, "A simplification of the logic of relations," Proc. of the Cambridge Philos. Soc., 1914, vol. 17, pp.387-390. It is also shown as a definition in [Enderton] p. 36 and as Exercise 4.8(b) of [Mendelson] p. 230. It is meaningful only for classes that exist as sets (i.e. are not proper classes). See df-op 2474 for other ordered pair definitions.
|- A e. V   &   |- B e. V   =>   |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} <-> (A = C /\ B = D))
Theorem	uniop 2885	The union of an ordered pair. Theorem 65 of [Suppes] p. 39.
|- U.<.A, B>. = {A, B}
Theorem	uniopel 2886	Ordered pair membership is inherited by class union.
|- (<.A, B>. e. C -> U.<.A, B>. e. U.C)
Ordered-pair class abstractions (cont.)
Theorem	opabid 2887	The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61.
|- (<.x, y>. e. {<.x, y>. | ph} <-> ph)
Theorem	elopab 2888	Membership in a class abstraction of pairs.
|- (A e. {<.x, y>. | ph} <-> E.xE.y(A = <.x, y>. /\ ph))
Theorem	hbopab 2889	Bound-variable hypothesis builder for class abstraction.
|- (ph -> A.zph)   =>   |- (w e. {<.x, y>. | ph} -> A.z w e. {<.x, y>. | ph})
Theorem	hbopab1 2890	The first abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free.
|- (z e. {<.x, y>. | ph} -> A.x z e. {<.x, y>. | ph})
Theorem	hbopab2 2891	The second abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free.
|- (z e. {<.x, y>. | ph} -> A.y z e. {<.x, y>. | ph})
Theorem	opelopabsb 2892	The law of concretion in terms of substitutions.
|- (<.z, w>. e. {<.x, y>. | ph} <-> [w / y][z / x]ph)
Theorem	brabsb 2893	The law of concretion in terms of substitutions.
|- R = {<.x, y>. | ph}   =>   |- (zRw <-> [w / y][z / x]ph)
Theorem	opelopabg 2894	The law of concretion. Theorem 9.5 of [Quine] p. 61.
|- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   =>   |- ((A e. C /\ B e. D) -> (<.A, B>. e. {<.x, y>. | ph} <-> ch))
Theorem	brabg 2895	The law of concretion for a binary relation.
|- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- R = {<.x, y>. | ph}   =>   |- ((A e. C /\ B e. D) -> (ARB <-> ch))
Theorem	opelopab2 2896	Ordered pair membership in an ordered pair class abstraction.
|- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   =>   |- ((A e. C /\ B e. D) -> (<.A, B>. e. {<.x, y>. | ((x e. C /\ y e. D) /\ ph)} <-> ch))
Theorem	opelopab 2897	The law of concretion. Theorem 9.5 of [Quine] p. 61.
|- A e. V   &   |- B e. V   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   =>   |- (<.A, B>. e. {<.x, y>. | ph} <-> ch)
Theorem	brab 2898	The law of concretion for a binary relation.
|- A e. V   &   |- B e. V   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- R = {<.x, y>. | ph}   =>   |- (ARB <-> ch)
Theorem	opelopabf 2899	The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 2897 uses bound-variable hypotheses in place of distinct variable conditions."
|- (ps -> A.xps)   &   |- (ch -> A.ych)   &   |- A e. V   &   |- B e. V   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   =>   |- (<.A, B>. e. {<.x, y>. | ph} <-> ch)
Theorem	ssopab2 2900	Equivalence of ordered pair abstraction subclass and implication.
|- ({<.x, y>. | ph} (_ {<.x, y>. | ps} <-> A.xA.y(ph -> ps))