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

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

Type	Label	Description
Statement
Theorem	euop2 2801	Transfer existential uniqueness to second member of an ordered pair.
|- (E!xE.y(x = <.A, y>. /\ ph) <-> E!yph)
Theorem	opthwiener 2802	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 2803	The union of an ordered pair. Theorem 65 of [Suppes] p. 39.
|- U.<.A, B>. = {A, B}
Theorem	uniopel 2804	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 2805	The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61.
|- (<.x, y>. e. {<.x, y>. | ph} <-> ph)
Theorem	elopab 2806	Membership in a class abstraction of pairs.
|- (A e. {<.x, y>. | ph} <-> E.xE.y(A = <.x, y>. /\ ph))
Theorem	hbopab 2807	Bound-variable hypothesis builder for class abstraction.
|- (ph -> A.zph)   =>   |- (w e. {<.x, y>. | ph} -> A.z w e. {<.x, y>. | ph})
Theorem	hbopab1 2808	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 2809	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 2810	The law of concretion in terms of substitutions.
|- (<.z, w>. e. {<.x, y>. | ph} <-> [w / y][z / x]ph)
Theorem	brabsb 2811	The law of concretion in terms of substitutions.
|- R = {<.x, y>. | ph}   =>   |- (zRw <-> [w / y][z / x]ph)
Theorem	opelopabg 2812	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 2813	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 2814	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 2815	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 2816	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 2817	Equivalence of ordered pair abstraction subclass and implication.
|- ({<.x, y>. | ph} (_ {<.x, y>. | ps} <-> A.xA.y(ph -> ps))
Theorem	ssopab2i 2818	Inference of ordered pair abstraction subclass from implication.
|- (ph -> ps)   =>   |- {<.x, y>. | ph} (_ {<.x, y>. | ps}
Theorem	opabn0 2819	Non-empty ordered pair class abstraction.
|- ({<.x, y>. | ph} =/= (/) <-> E.xE.yph)
Power class of union and intersection
Theorem	pwin 2820	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 2821	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 2822	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 2823	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 2824	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 2825	Extend class notation to include the epsilon relation.
class E
Syntax	cid 2826	Extend the definition of a class to include identity relation.
class I
Definition	df-eprel 2827	Define the epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30.
|- E = {<.x, y>. | x e. y}
Theorem	epelc 2828	The epsilon relation and the membership relation are the same.
|- A e. V   &   |- B e. V   =>   |- (AEB <-> A e. B)
Theorem	epel 2829	The epsilon relation and the membership relation are the same.
|- (xEy <-> x e. y)
Definition	df-id 2830	Define the identity relation. Definition 9.15 of [Quine] p. 64.
|- I = {<.x, y>. | x = y}
Theorem	dfid3 2831	A stronger version of df-id 2830 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 2832	Alternate definition of the identity relation.
|- I = {<.x, x>. | x = x}
Partial and complete ordering
Syntax	wpo 2833	Extend wff notation to include the strict partial ordering predicate. Read: 'R is a partial order on A.'
wff R Po A
Syntax	wor 2834	Extend wff notation to include the strict complete ordering predicate. Read: 'R orders A.'
wff R Or A
Definition	df-po 2835	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 2836	Subset theorem for the partial ordering predicate.
|- (A (_ B -> (R Po B -> R Po A))
Theorem	poeq1 2837	Equality theorem for partial ordering predicate.
|- (R = S -> (R Po A <-> S Po A))
Theorem	poeq2 2838	Equality theorem for partial ordering predicate.
|- (A = B -> (R Po A <-> R Po B))
Theorem	pocl 2839	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 2840	A partial order relation is irreflexive.
|- ((R Po A /\ B e. A) -> -. BRB)
Theorem	potr 2841	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 2842	A partial order relation has no 2-cycle loops.
|- ((R Po A /\ (B e. A /\ C e. A)) -> -. (BRC /\ CRB))
Theorem	po3nr 2843	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 2844	Any relation is a partial ordering of the empty set.
|- R Po (/)
Definition	df-so 2845	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 2846	A strict linear order is a strict partial order.
|- (R Or A -> R Po A)
Theorem	soss 2847	Subset theorem for the strict ordering predicate.
|- (A (_ B -> (R Or B -> R Or A))
Theorem	soeq1 2848	Equality theorem for the strict ordering predicate.
|- (R = S -> (R Or A <-> S Or A))
Theorem	soeq2 2849	Equality theorem for the strict ordering predicate.
|- (A = B -> (R Or A <-> R Or B))
Theorem	sonr 2850	A strict order relation is irreflexive.
|- ((R Or A /\ B e. A) -> -. BRB)
Theorem	sotr 2851	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 2852	A strict order relation is linear (satisfies trichotomy).
|- ((R Or A /\ (B e. A /\ C e. A)) -> (BRC \/ B = C \/ CRB))
Theorem	so2nr 2853	A strict order relation has no 2-cycle loops.
|- ((R Or A /\ (B e. A /\ C e. A)) -> -. (BRC /\ CRB))
Theorem	so3nr 2854	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 2855	A strict order relation satisfies strict trichotomy.
|- ((R Or A /\ (B e. A /\ C e. A)) -> (BRC <-> -. (B = C \/ CRB)))
Theorem	sotrieq 2856	Trichotomy law for strict order relation.
|- ((R Or A /\ (B e. A /\ C e. A)) -> (B = C <-> -. (BRC \/ CRB)))
Theorem	sotrieq2 2857	Trichotomy law for strict order relation.
|- ((R Or A /\ (B e. A /\ C e. A)) -> (B = C <-> (-. BRC /\ -. CRB)))
Theorem	itlso 2858	A irreflexive, transitive, linear relation is a strict ordering.
|- (x e. A -> -. xRx)   &   |- ((x e. A /\ y e.