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

Statement List for Metamath Proof Explorer - 2901-3000 - Page 30 of 107

Type	Label	Description
Statement
Theorem	reuxfr2 2901	Transfer existential uniqueness from a variable x to another variable y contained in expression A.
|- (y e. B -> A e. B)   &   |- (x e. B -> E*y(y e. B /\ x = A))   =>   |- (E!x e. B E.y e. B (x = A /\ ph) <-> E!y e. B ph)
Theorem	reuxfr 2902	Transfer existential uniqueness from a variable x to another variable y contained in expression A. Use reuhyp 2903 to eliminate the second hypothesis.
|- (y e. B -> A e. B)   &   |- (x e. B -> E!y e. B x = A)   &   |- (x = A -> (ph <-> ps))   =>   |- (E!x e. B ph <-> E!y e. B ps)
Theorem	reuhyp 2903	A theorem useful for eliminating the restricted existential uniqueness hypotheses in reuxfr 2902.
|- (x e. C -> B e. C)   &   |- ((x e. C /\ y e. C) -> (x = A <-> y = B))   =>   |- (x e. C -> E!y e. C x = A)
Theorem	reuunixfr 2904	Change the variable x in the expression for "the unique A such that ph" to another variable y contained in expression B. Use reuhyp 2903 to eliminate the last hypothesis.
|- (z e. C -> A.y z e. C)   &   |- (y e. A -> B e. A)   &   |- (U.{y e. A | ps} e. A -> C e. A)   &   |- (x = B -> (ph <-> ps))   &   |- (y = U.{y e. A | ps} -> B = C)   &   |- (x e. A -> E!y e. A x = B)   =>   |- (E!x e. A ph -> U.{x e. A | ph} = C)
Theorem	uniexb 2905	The Axiom of Union and its converse. A class is a set iff its union is a set.
|- (A e. V <-> U.A e. V)
Theorem	pwexb 2906	The Axiom of Power Sets and its converse. A class is a set iff its power class is a set.
|- (A e. V <-> P~A e. V)
Theorem	univ 2907	The union of the universe is the universe. Exercise 4.12(c) of [Mendelson] p. 235.
|- U.V = V
Theorem	eldifpw 2908	Membership in a power class difference.
|- C e. V   =>   |- ((A e. P~B /\ -. C (_ B) -> (A u. C) e. (P~(B u. C) \ P~B))
Theorem	elpwun 2909	Membership in the power class of a union.
|- C e. V   =>   |- (A e. P~(B u. C) <-> (A \ C) e. P~B)
Theorem	elpwunsn 2910	Membership in an extension of a power class.
|- (A e. (P~(B u. {C}) \ P~B) -> C e. A)
Theorem	op1stb 2911	Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (See op2ndb 3449 to extract the second member, op1sta 3446 for an alternate version, and op1st 4084 for the preferred version.)
|- A e. V   =>   |- |^||^|<.A, B>. = A
Theorem	iunpw 2912	The power class of an intersection in terms of indexed intersection. Part of Exercise 24(b) of [Enderton] p. 33.
|- A e. V   =>   |- (E.x e. A x = U.A <-> P~U.A = U_x e. A P~x)
Founded and well-ordering relations
Syntax	wfr 2913	Extend wff notation to include the founded predicate. Read: 'R is a founded relation on A.'
wff R Fr A
Syntax	wwe 2914	Extend wff notation to include the well-ordering predicate. Read: 'R well-orders A.'
wff R We A
Definition	df-fr 2915	Define a founded relation. For alternate definitions, see dffr2 2917 and dffr3 3427.
|- (R Fr A <-> A.x((x (_ A /\ x =/= (/)) -> E.y e. x A.z e. x -. zRy))
Theorem	fri 2916	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 2917	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 2918	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 2919	Subset theorem for the founded predicate. Exercise 1 of [TakeutiZaring] p. 31.
|- (A (_ B -> (R Fr B -> R Fr A))
Theorem	freq1 2920	Equality theorem for the founded predicate.
|- (R = S -> (R Fr A <-> S Fr A))
Theorem	freq2 2921	Equality theorem for the founded predicate.
|- (A = B -> (R Fr A <-> R Fr B))
Theorem	frirr 2922	A founded relation is irreflexive. Special case of Proposition 6.23 of [TakeutiZaring] p. 30.
|- ((R Fr A /\ x e. A) -> -. xRx)
Theorem	fr2nr 2923	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	fr3nr 2924	A founded relation has no 3-cycle loops. Special case of Proposition 6.23 of [TakeutiZaring] p. 30.
|- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. (xRy /\ yRz /\ zRx))
Theorem	fr0 2925	Any relation is founded on the empty set.
|- R Fr (/)
Theorem	efrirr 2926	Irreflexivitiy of the epsilon relation: a class founded by epsilon is not a member of itself.
|- (E Fr A -> -. A e. A)
Theorem	efrn2lp 2927	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	epne3 2928	A set founded by epsilon contains no 3-cycle loops.
|- ((E Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. (x e. y /\ y e. z /\ z e. x))
Theorem	tz7.2 2929	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 2930	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 2931	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 2932	Define a well-ordering. For an alternate definition see dfwe2 2933.
|- (R We A <-> (R Fr A /\ R Or A))
Theorem	dfwe2 2933	Alternate definition of well-ordering. Definition 6.24(2) of [TakeutiZaring] p. 30.
|- (R We A <-> (R Fr A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))
Theorem	wess 2934	Subset theorem for the well-ordering predicate. Exercise 4 of [TakeutiZaring] p. 31.
|- (A (_ B -> (R We B -> R We A))
Theorem	weeq1 2935	Equality theorem for the well-ordering predicate.
|- (R = S -> (R We A <-> S We A))
Theorem	weeq2 2936	Equality theorem for the well-ordering predicate.
|- (A = B -> (R We A <-> R We B))
Theorem	wefr 2937	A well-ordering is founded.
|- (R We A -> R Fr A)
Theorem	weso 2938	A well-ordering is a strict ordering.
|- (R We A -> R Or A)
Theorem	wecmpep 2939	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 2940	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 2941	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 2942	Any relation is a well-ordering of the empty set.
|- R We (/)
Theorem	wereu 2943	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 2944	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 2945	Extend the definition of a wff to include the ordinal predicate.
wff Ord A
Syntax	con0 2946	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 2947	Extend the definition of a wff to include the limit ordinal predicate.
wff Lim A
Syntax	csuc 2948	Extend class notation to include the successor function.
class suc A
Definition	df-ord 2949	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 2950	Define the class of all ordinal numbers. Definition 7.11 of [TakeutiZaring] p. 38.
|- On = {x | Ord x}
Definition	df-lim 2951	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 3024, dflim3 3117, and dflim4 for alternate definitions.
|- (Lim A <-> (Ord A /\ A =/= (/) /\ A = U.A))
Definition	df-suc 2952	Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 4163). 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 3043), so that the successor of any ordinal class is still an ordinal class (ordsuc 3064), 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 2953	Equality theorem for the ordinal predicate.
|- (A = B -> (Ord A <-> Ord B))
Theorem	elong 2954	An ordinal number is an ordinal set.
|- (A e. B -> (A e. On <-> Ord A))
Theorem	elon 2955	An ordinal number is an ordinal set.
|- A e. V   =>   |- (A e. On <-> Ord A)
Theorem	eloni 2956	An ordinal number has the ordinal property.
|- (A e. On -> Ord A)
Theorem	elon2 2957	An ordinal number is an ordinal set.
|- (A e. On <-> (Ord A /\ A e. V))
Theorem	limeq 2958	Equality theorem for the limit predicate.
|- (A = B -> (Lim A <-> Lim B))
Theorem	ordwe 2959	Epsilon well orders every ordinal. Proposition 7.4 of [TakeutiZaring] p. 36.
|- (Ord A -> E We A)
Theorem	ordtr 2960	An ordinal class is transitive.
|- (Ord A -> Tr A)
Theorem	ordfr 2961	Epsilon is well-founded on an ordinal class.
|- (Ord A -> E Fr A)
Theorem	ordelss 2962	An element of an ordinal class is a subset of it.
|- ((Ord A /\ B e. A) -> B (_ A)
Theorem	trssord 2963	A transitive subclass of an ordinal class is ordinal.
|- ((Tr A /\ A (_ B /\ Ord B) -> Ord A)
Theorem	ordirr 2964	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 2965	A member of an ordinal class is not equal to it.
|- ((Ord A /\ B e. A) -> A =/= B)
Theorem	ordn2lp 2966	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 2967	A subclass (possibly proper) of an ordinal class has a minimal element. Proposition 7.5 of [TakeutiZaring] p. 36.
|- ((Ord A /\ B (_ A /\ B =/= (/)) ->