mmtheorems30 - 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 - 2901-3000 - Page 30 of 123

Type	Label	Description
Statement
Theorem	ssopab2i 2901	Inference of ordered pair abstraction subclass from implication.
|- (ph -> ps)   =>   |- {<.x, y>. | ph} (_ {<.x, y>. | ps}
Theorem	opabn0 2902	Non-empty ordered pair class abstraction.
|- ({<.x, y>. | ph} =/= (/) <-> E.xE.yph)
Power class of union and intersection
Theorem	pwin 2903	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 2904	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 2905	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 2906	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 2907	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 2908	Extend class notation to include the epsilon relation.
class E
Syntax	cid 2909	Extend the definition of a class to include identity relation.
class I
Definition	df-eprel 2910	Define the epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30.
|- E = {<.x, y>. | x e. y}
Theorem	epelc 2911	The epsilon relation and the membership relation are the same.
|- A e. V   &   |- B e. V   =>   |- (AEB <-> A e. B)
Theorem	epel 2912	The epsilon relation and the membership relation are the same.
|- (xEy <-> x e. y)
Definition	df-id 2913	Define the identity relation. Definition 9.15 of [Quine] p. 64.
|- I = {<.x, y>. | x = y}
Theorem	dfid3 2914	A stronger version of df-id 2913 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 2915	Alternate definition of the identity relation.
|- I = {<.x, x>. | x = x}
Partial and complete ordering
Syntax	wpo 2916	Extend wff notation to include the strict partial ordering predicate. Read: 'R is a partial order on A.'
wff R Po A
Syntax	wor 2917	Extend wff notation to include the strict complete ordering predicate. Read: 'R orders A.'
wff R Or A
Definition	df-po 2918	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 2919	Subset theorem for the partial ordering predicate.
|- (A (_ B -> (R Po B -> R Po A))
Theorem	poeq1 2920	Equality theorem for partial ordering predicate.
|- (R = S -> (R Po A <-> S Po A))
Theorem	poeq2 2921	Equality theorem for partial ordering predicate.
|- (A = B -> (R Po A <-> R Po B))
Theorem	pocl 2922	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 2923	A partial order relation is irreflexive.
|- ((R Po A /\ B e. A) -> -. BRB)
Theorem	potr 2924	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 2925	A partial order relation has no 2-cycle loops.
|- ((R Po A /\ (B e. A /\ C e. A)) -> -. (BRC /\ CRB))
Theorem	po3nr 2926	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 2927	Any relation is a partial ordering of the empty set.
|- R Po (/)
Theorem	posn 2928	Partial ordering of a singleton.
|- (R Po {x} <-> -. <.x, x>. e. R)
Definition	df-so 2929	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 2930	A strict linear order is a strict partial order.
|- (R Or A -> R Po A)
Theorem	soss 2931	Subset theorem for the strict ordering predicate.
|- (A (_ B -> (R Or B -> R Or A))
Theorem	soeq1 2932	Equality theorem for the strict ordering predicate.
|- (R = S -> (R Or A <-> S Or A))
Theorem	soeq2 2933	Equality theorem for the strict ordering predicate.
|- (A = B -> (R Or A <-> R Or B))
Theorem	sonr 2934	A strict order relation is irreflexive.
|- ((R Or A /\ B e. A) -> -. BRB)
Theorem	sotr 2935	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 2936	A strict order relation is linear (satisfies trichotomy).
|- ((R Or A /\ (B e. A /\ C e. A)) -> (BRC \/ B = C \/ CRB))
Theorem	so2nr 2937	A strict order relation has no 2-cycle loops.
|- ((R Or A /\ (B e. A /\ C e. A)) -> -. (BRC /\ CRB))
Theorem	so3nr 2938	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 2939	A strict order relation satisfies strict trichotomy.
|- ((R Or A /\ (B e. A /\ C e. A)) -> (BRC <-> -. (B = C \/ CRB)))
Theorem	sotrieq 2940	Trichotomy law for strict order relation.
|- ((R Or A /\ (B e. A /\ C e. A)) -> (B = C <-> -. (BRC \/ CRB)))
Theorem	sotrieq2 2941	Trichotomy law for strict order relation.
|- ((R Or A /\ (B e. A /\ C e. A)) -> (B = C <-> (-. BRC /\ -. CRB)))
Theorem	itlso 2942	A irreflexive, transitive, linear relation is a strict ordering.
|- (x e. A -> -. xRx)   &   |- ((x e. A /\ y e. A /\ z e. A) -> ((xRy /\ yRz) -> xRz))   &   |- ((x e. A /\ y e. A) -> (xRy \/ x = y \/ yRx))   =>   |- R Or A
Theorem	so 2943	Deduce strict ordering from its properties.
|- ((x e. A /\ y e. A /\ z e. A) -> ((xRy <-> -. (x = y \/ yRx)) /\ ((xRy /\ yRz) -> xRz)))   =>   |- R Or A
Theorem	so0 2944	Any relation is a strict ordering of the empty set.
|- R Or (/)
Founded and well-ordering relations
Syntax	wfr 2945	Extend wff notation to include the founded predicate. Read: 'R is a founded relation on A.'
wff R Fr A
Syntax	wwe 2946	Extend wff notation to include the well-ordering predicate. Read: 'R well-orders A.'
wff R We A
Definition	df-fr 2947	Define a founded relation. For alternate definitions, see dffr2 2949 and dffr3 3523.
|- (R Fr A <-> A.x((x (_ A /\ x =/= (/)) -> E.y e. x A.z e. x -. zRy))
Theorem	fri 2948	Property of founded relation (one direction of definition).
|- (((B e. C /\ R Fr A) /\ (B (_ A /\ B =/= (/))) -> E.x e. B A.y e. B -. yRx)
Theorem	dffr2 2949	Alternate definition of founded relation. Similar to Definition 6.21 of [TakeutiZaring] p. 30.
|- (R Fr A <-> A.x((x (_ A /\ x =/= (/)) -> E.y e. x (x i^i {z | zRy}) = (/)))
Theorem	frc 2950	Property of founded relation (one direction of definition using class variables).
|- B e. V   =>   |- ((R Fr A /\ B (_ A /\ B =/= (/)) -> E.x e. B (B i^i {y | yRx}) = (/))
Theorem	frss 2951	Subset theorem for the founded predicate. Exercise 1 of [TakeutiZaring] p. 31.
|- (A (_ B -> (R Fr B -> R Fr A))
Theorem	freq1 2952	Equality theorem for the founded predicate.
|- (R = S -> (R Fr A <-> S Fr A))
Theorem	freq2 2953	Equality theorem for the founded predicate.
|- (A = B -> (R Fr A <-> R Fr B))
Theorem	frirr 2954	A founded relation is irreflexive. Special case of Proposition 6.23 of [TakeutiZaring] p. 30.
|- ((R Fr A /\ x e. A) -> -. xRx)
Theorem	fr2nr 2955	A founded relation has no 2-cycle loops. Special case of Proposition 6.23 of [TakeutiZaring] p. 30.
|- ((R Fr A /\ (x e. A /\ y e. A)) -> -. (xRy /\ yRx))
Theorem	fr0 2956	Any relation is founded on the empty set.
|- R Fr (/)
Theorem	efrirr 2957	Irreflexivitiy of the epsilon relation: a class founded by epsilon is not a member of itself.
|- (E Fr A -> -. A e. A)
Theorem	efrn2lp 2958	A set founded by epsilon contains no 2-cycle loops.
|- ((E Fr A /\ (x e. A /\ y e. A)) -> -. (x e. y /\ y e. x))
Theorem	tz7.2 2959	Similar to Theorem 7.2 of [TakeutiZaring] p. 35, of except that the Axiom of Regularity is not required due to antecedent E Fr A.
|- ((Tr A /\ E Fr A /\ B e. A) -> (B (_ A /\ B =/= A))
Theorem	dfepfr 2960	An alternate way of saying that the epsilon relation is founded.
|- (E Fr A <-> A.x((x (_ A /\ x =/= (/)) -> E.y e. x (x i^i y) = (/)))
Theorem	epfrc 2961	A subset of an epsilon-founded class has a minimal element.
|- B e. V   =>   |- ((E Fr A /\ B (_ A /\ B =/= (/)) -> E.x e. B (B i^i x) = (/))
Definition	df-we 2962	Define a well-ordering. For an alternate definition, see dfwe2 3140.
|- (R We A <-> (R Fr A /\ R Or A))
Theorem	wess 2963	Subset theorem for the well-ordering predicate. Exercise 4 of [TakeutiZaring] p. 31.
|- (A (_ B -> (R We B -> R We A))
Theorem	weeq1 2964	Equality theorem for the well-ordering predicate.
|- (R = S -> (R We A <-> S We A))
Theorem	weeq2 2965	Equality theorem for the well-ordering predicate.
|- (A = B -> (R We A <-> R We B))
Theorem	wefr 2966	A well-ordering is founded.
|- (R We A -> R Fr A)
Theorem	weso 2967	A well-ordering is a strict ordering.
|- (R We A -> R Or A)
Theorem	wecmpep 2968	The elements of an epsilon well-ordering are comparable.
|- ((E We A /\ (x e. A /\ y e. A)) -> (x e. y \/ x = y \/ y e. x))
Theorem	wetrep 2969	An epsilon well-ordering is a transitive relation.
|- ((E We A /\ (x e. A /\ y e. A /\ z e. A)) -> ((x e. y /\ y e. z) -> x e. z))
Theorem	wefrc 2970	A non-empty (possibly proper) subclass of a class well-ordered by E has a minimal element. Special case of Proposition 6.26 of [TakeutiZaring] p. 31.
|- ((E We A /\ B (_ A /\ B =/= (/)) -> E.x e. B (B i^i x) = (/))
Theorem	we0 2971	Any relation is a well-ordering of the empty set.
|- R We (/)
Theorem	wereu 2972	A subset of a well-ordered set has a unique minimal element.
|- B e. V   =>   |- ((R We A /\ B (_ A /\ B =/= (/)) -> E!x e. B A.y e. B -. yRx)
Theorem	wereucl 2973	The unique minimal element of a subset of a well-ordered set.
|- B e. V   =>   |- ((R We A /\ B (_ A /\ B =/= (/)) -> U.{x e. B | A.y e. B -. yRx} e. B)
Ordinals
Syntax	word 2974	Extend the definition of a wff to include the ordinal predicate.
wff Ord A
Syntax	con0 2975	Extend the definition of a class to include the class of all ordinal numbers. (The 0 in the name prevents creating a file called con.html, which causes problems in Windows.)
class On
Syntax	wlim 2976	Extend the definition of a wff to include the limit ordinal predicate.
wff Lim A
Syntax	csuc 2977	Extend class notation to include the successor function.
class suc A
Definition	df-ord 2978	Define the ordinal predicate, which is true for a class that is transitive and is well-ordered by the epsilon relation. Variant of definition of [BellMachover] p. 468.
|- (Ord A <-> (Tr A /\ E We A))
Definition	df-on 2979	Define the class of all ordinal numbers. Definition 7.11 of [TakeutiZaring] p. 38.
|- On = {x | Ord x}
Definition	df-lim 2980	Define the limit ordinal predicate, which is true for a non-empty ordinal that is not a successor (i.e. that is the union of itself). Our definition combines the definition of Lim of [BellMachover] p. 471 and Exercise 1 of [TakeutiZaring] p. 42. See dflim2 3029, dflim3 3201, and dflim4 for alternate definitions.
|- (Lim A <-> (Ord A /\ A =/= (/) /\ A = U.A))
Definition	df-suc 2981	Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 4300). Definition 7.22 of [TakeutiZaring] p. 41, who use "+ 1" to denote this function. Our definition is a generalization to classes. Although it is not conventional to use it with proper classes, it has no affect on a proper class (sucprc 3048), so that the successor of any ordinal class is still an ordinal class (ordsuc 3171), simplifying certain proofs. Some authors denote the successor operation with a prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] p. 134 and the definition of successor in [Mendelson] p. 246 (who uses the symbol "Suc" as a predicate to mean "is a successor ordinal"). The definition of successor of [Enderton] p. 68 denotes the operation with a plus-sign superscript.
|- suc A = (A u. {A})
Theorem	ordeq 2982	Equality theorem for the ordinal predicate.
|- (A = B -> (Ord A <-> Ord B))
Theorem	elong 2983	An ordinal number is an ordinal set.
|- (A e. B -> (A e. On <-> Ord A))
Theorem	elon 2984	An ordinal number is an ordinal set.
|- A e. V   =>   |- (A e. On <-> Ord A)
Theorem	eloni 2985	An ordinal number has the ordinal property.
|- (A e. On -> Ord A)
Theorem	elon2 2986	An ordinal number is an ordinal set.
|- (A e. On <-> (Ord A /\ A e. V))
Theorem	limeq 2987	Equality theorem for the limit predicate.
|- (A = B -> (Lim A <-> Lim B))
Theorem	ordwe 2988	Epsilon well orders every ordinal. Proposition 7.4 of [TakeutiZaring] p. 36.
|- (Ord A -> E We A)
Theorem	ordtr 2989	An ordinal class is transitive.
|- (Ord A -> Tr A)
Theorem	ordfr 2990	Epsilon is well-founded on an ordinal class.
|- (Ord A -> E Fr A)
Theorem	ordelss 2991	An element of an ordinal class is a subset of it.
|- ((Ord A /\ B e. A) -> B (_ A)
Theorem	trssord 2992	A transitive subclass of an ordinal class is ordinal.
|- ((Tr A /\ A (_ B /\ Ord B) -> Ord A)
Theorem	ordirr 2993	Epsilon irreflexivity of ordinals: no ordinal class is a member of itself. Theorem 2.2(i) of [BellMachover] p. 469, generalized to classes. We prove this without invoking the Axiom of Regularity.
|- (Ord A -> -. A e. A)
Theorem	nordeq 2994	A member of an ordinal class is not equal to it.
|- ((Ord A /\ B e. A) -> A =/= B)
Theorem	ordn2lp 2995	An ordinal class cannot an element of one of its members. Variant of first part of Theorem 2.2(vii) of [BellMachover] p. 469.
|- (Ord A -> -. (A e. B /\ B e. A))
Theorem	tz7.5 2996	A subclass (possibly proper) of an ordinal class has a minimal element. Proposition 7.5 of [TakeutiZaring] p. 36.
|- ((Ord A /\ B (_ A /\ B =/= (/)) -> E.x e. B (B i^i x) = (/))
Theorem	ordelord 2997	An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36.
|- ((Ord A /\ B e. A) -> Ord B)
Theorem	tron 2998	The class of all ordinal numbers is transitive.
|- Tr On
Theorem	ordelon 2999	An element of an ordinal class is an ordinal number.
|- ((Ord A /\ B e. A) -> B e. On)
Theorem	onelon 3000	An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469.
|- ((A e. On /\ B e. A) -> B e. On)