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-10684

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

Type	Label	Description
Statement
Theorem	mosubopt 2801	"At most one" remains true inside ordered pair quantification.
|- (A.yA.zE*xph -> E*xE.yE.z(A = <.y, z>. /\ ph))
Theorem	mosubop 2802	"At most one" remains true inside ordered pair quantification.
|- E*xph   =>   |- E*xE.yE.z(A = <.y, z>. /\ ph)
Theorem	euop2 2803	Transfer existential uniqueness to second member of an ordered pair.
|- (E!xE.y(x = <.A, y>. /\ ph) <-> E!yph)
Theorem	opthwiener 2804	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 2412 for other ordered pair definitions.
|- A e. V   &   |- B e. V   =>   |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} <-> (A = C /\ B = D))
Theorem	uniop 2805	The union of an ordered pair. Theorem 65 of [Suppes] p. 39.
|- U.<.A, B>. = {A, B}
Theorem	uniopel 2806	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 2807	The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61.
|- (<.x, y>. e. {<.x, y>. | ph} <-> ph)
Theorem	elopab 2808	Membership in a class abstraction of pairs.
|- (A e. {<.x, y>. | ph} <-> E.xE.y(A = <.x, y>. /\ ph))
Theorem	hbopab 2809	Bound-variable hypothesis builder for class abstraction.
|- (ph -> A.zph)   =>   |- (w e. {<.x, y>. | ph} -> A.z w e. {<.x, y>. | ph})
Theorem	hbopab1 2810	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 2811	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	opabsb 2812	The law of concretion in terms of substitutions.
|- (<.z, w>. e. {<.x, y>. | ph} <-> [w / y][z / x]ph)
Theorem	brabsb 2813	The law of concretion in terms of substitutions.
|- R = {<.x, y>. | ph}   =>   |- (zRw <-> [w / y][z / x]ph)
Theorem	opelopabg 2814	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 2815	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 2816	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 2817	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 2818	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	ssopab2 2819	Equivalence of ordered pair abstraction subclass and implication.
|- ({<.x, y>. | ph} (_ {<.x, y>. | ps} <-> A.xA.y(ph -> ps))
Theorem	ssopab2i 2820	Inference of ordered pair abstraction subclass from implication.
|- (ph -> ps)   =>   |- {<.x, y>. | ph} (_ {<.x, y>. | ps}
Theorem	opabn0 2821	Non-empty ordered pair class abstraction.
|- ({<.x, y>. | ph} =/= (/) <-> E.xE.yph)
Power class of union and intersection
Theorem	pwin 2822	The power class of the intersection of two classes is the intersection of their power classes. Exercise 4.12(j) of [Mendelson] p. 235.
|- P~(A i^i B) = (P~A i^i P~B)
Theorem	pwunss 2823	The power class of the union of two classes includes the union of their power classes. Exercise 4.12(k) of [Mendelson] p. 235.
|- (P~A u. P~B) (_ P~(A u. B)
Theorem	pwssun 2824	The power class of the union of two classes is a subset of the union of their power classes, iff one class is a subclass of the other. Exercise 4.12(l) of [Mendelson] p. 235.
|- ((A (_ B \/ B (_ A) <-> P~(A u. B) (_ (P~A u. P~B))
Theorem	pwundif 2825	Break up the power class of a union into a union of smaller classes.
|- P~(A u. B) = ((P~(A u. B) \ P~A) u. P~A)
Theorem	pwun 2826	The power class of the union of two classes equals the union of their power classes, iff one class is a subclass of the other. Part of Exercise 7(b) of [Enderton] p. 28.
|- ((A (_ B \/ B (_ A) <-> P~(A u. B) = (P~A u. P~B))
Epsilon and identity relations
Syntax	cep 2827	Extend class notation to include the epsilon relation.
class E
Syntax	cid 2828	Extend the definition of a class to include identity relation.
class I
Definition	df-eprel 2829	Define the epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30.
|- E = {<.x, y>. | x e. y}
Theorem	epelc 2830	The epsilon relation and the membership relation are the same.
|- A e. V   &   |- B e. V   =>   |- (AEB <-> A e. B)
Theorem	epel 2831	The epsilon relation and the membership relation are the same.
|- (xEy <-> x e. y)
Definition	df-id 2832	Define the identity relation. Definition 9.15 of [Quine] p. 64.
|- I = {<.x, y>. | x = y}
Theorem	ideqgOLD 2833	For sets, the identity relation is the same as equality.
|- ((A e. C /\ B e. D) -> (AIB <-> A = B))
Theorem	dfid3 2834	A stronger version of df-id 2832 that doesn't require x and y to be distinct. Ordinarily, we wouldn't use this as a definition, since non-distinct dummy variables would make soundness verification more difficult (as the proof here shows). The proof can be instructive in showing how distinct variable requirements may be eliminated, a task that is not necessarily obvious.
|- I = {<.x, y>. | x = y}
Theorem	dfid2 2835	Alternate definition of the identity relation.
|- I = {<.x, x>. | x = x}
Theorem	ideqOLD 2836	For sets, the identity relation is the same as equality.
|- A e. V   &   |- B e. V   =>   |- (AIB <-> A = B)
Partial and complete ordering
Syntax	wpo 2837	Extend wff notation to include the strict partial ordering predicate. Read: 'R is a partial order on A.'
wff R Po A
Syntax	wor 2838	Extend wff notation to include the strict complete ordering predicate. Read: 'R orders A.'
wff R Or A
Definition	df-po 2839	Define a strict partial order relation. Definition of [Enderton] p. 168.
|- (R Po A <-> A.x e. A A.y e. A A.z e. A (-. xRx /\ ((xRy /\ yRz) -> xRz)))
Theorem	poss 2840	Subset theorem for the partial ordering predicate.
|- (A (_ B -> (R Po B -> R Po A))
Theorem	poeq1 2841	Equality theorem for partial ordering predicate.
|- (R = S -> (R Po A <-> S Po A))
Theorem	poeq2 2842	Equality theorem for partial ordering predicate.
|- (A = B -> (R Po A <-> R Po B))
Theorem	pocl 2843	Properties of partial order relation in class notation.
|- (R Po A -> ((B e. A /\ C e. A /\ D e. A) -> (-. BRB /\ ((BRC /\ CRD) -> BRD))))
Theorem	poirr 2844	A partial order relation is irreflexive.
|- ((R Po A /\ B e. A) -> -. BRB)
Theorem	potr 2845	A partial order relation is a transitive relation.
|- ((R Po A /\ (B e. A /\ C e. A /\ D e. A)) -> ((BRC /\ CRD) -> BRD))
Theorem	po2nr 2846	A partial order relation has no 2-cycle loops.
|- ((R Po A /\ (B e. A /\ C e. A)) -> -. (BRC /\ CRB))
Theorem	po3nr 2847	A partial order relation has no 3-cycle loops.
|- ((R Po A /\ (B e. A /\ C e. A /\ D e. A)) -> -. (BRC /\ CRD /\ DRB))
Theorem	po0 2848	Any relation is a partial ordering of the empty set.
|- R Po (/)
Definition	df-so 2849	Define a strict complete (linear) order relation.
|- (R Or A <-> (R Po A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))
Theorem	sopo 2850	A strict linear order is a strict partial order.
|- (R Or A -> R Po A)
Theorem	soss 2851	Subset theorem for the strict ordering predicate.
|- (A (_ B -> (R Or B -> R Or A))
Theorem	soeq1 2852	Equality theorem for the strict ordering predicate.
|- (R = S -> (R Or A <-> S Or A))
Theorem	soeq2 2853	Equality theorem for the strict ordering predicate.
|- (A = B -> (R Or A <-> R Or B))
Theorem	sonr 2854	A strict order relation is irreflexive.
|- ((R Or A /\ B e. A) -> -. BRB)
Theorem	sotr 2855	A strict order relation is a transitive relation.
|- ((R Or A /\ (B e. A /\ C e. A /\ D e. A)) -> ((BRC /\ CRD) -> BRD))
Theorem	solin 2856	A strict order relation is linear (satisfies trichotomy).
|- ((R Or A /\ (B e. A /\ C e. A)) -> (BRC \/ B = C \/ CRB))
Theorem	so2nr 2857	A strict order relation has no 2-cycle loops.
|- ((R Or A /\ (B e. A /\ C e. A)) -> -. (BRC /\ CRB))
Theorem	so3nr 2858	A strict order relation has no 3-cycle loops.
|- ((R Or A /\ (B e. A /\ C e. A /\ D e. A)) -> -. (BRC /\ CRD /\ DRB))
Theorem	sotric 2859	A strict order relation satisfies strict trichotomy.
|- ((R Or A /\ (B e. A /\ C e. A)) -> (BRC <-> -.