mmtheorems31 - 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-10697

Statement List for Metamath Proof Explorer - 3001-3100 - Page 31 of 107

Type	Label	Description
Statement
Theorem	ontr1 3001	Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192.
|- (C e. On -> ((A e. B /\ B e. C) -> A e. C))
Theorem	ontr2 3002	Transitive law for ordinal numbers. Exercise 3 of [TakeutiZaring] p. 40.
|- ((A e. On /\ C e. On) -> ((A (_ B /\ B e. C) -> A e. C))
Theorem	ordunidif 3003	The union of an ordinal stays the same if a subset equal to one of its elements is removed.
|- ((Ord A /\ B e. A) -> U.(A \ B) = U.A)
Theorem	onint 3004	The intersection (infimum) of a non-empty class of ordinal numbers belongs to the class. Compare Exercise 4 of [TakeutiZaring] p. 45.
|- ((A (_ On /\ A =/= (/)) -> |^|A e. A)
Theorem	onint0 3005	The intersection of a class of ordinal numbers is zero iff the class contains zero.
|- (A (_ On -> (|^|A = (/) <-> (/) e. A))
Theorem	onssmin 3006	A non-empty class of ordinal numbers has a smallest member. Exercise 9 of [TakeutiZaring] p. 40.
|- ((A (_ On /\ A =/= (/)) -> E.x e. A A.y e. A x (_ y)
Theorem	onminsb 3007	If a property is true for some ordinal number, it is true for a minimal ordinal number. This version uses implicit substitution. Theorem Schema 62 of [Suppes] p. 228.
|- (ps -> A.xps)   &   |- (x = |^|{x e. On | ph} -> (ph <-> ps))   =>   |- (E.x e. On ph -> ps)
Theorem	onminesb 3008	If a property is true for some ordinal number, it is true for a minimal ordinal number. This version uses explicit substitution. Theorem Schema 62 of [Suppes] p. 228.
|- (E.x e. On ph -> [|^|{x e. On | ph} / x]ph)
Theorem	onintss 3009	If a property is true for an ordinal number, then the minimum ordinal number for which it is true is smaller or equal. Theorem Schema 61 of [Suppes] p. 228.
|- (x = A -> (ph <-> ps))   =>   |- (A e. On -> (ps -> |^|{x e. On | ph} (_ A))
Theorem	oninton 3010	The intersection of a non-empty collection of ordinal numbers is an ordinal number. Compare Exercise 6 of [TakeutiZaring] p. 44.
|- ((A (_ On /\ A =/= (/)) -> |^|A e. On)
Theorem	onintrab 3011	The intersection of a class of ordinal numbers exists iff it is an ordinal number.
|- (|^|{x e. On | ph} e. V <-> |^|{x e. On | ph} e. On)
Theorem	onintrab2 3012	An existence condition equivalent to an intersection's being an ordinal number.
|- (E.x e. On ph <-> |^|{x e. On | ph} e. On)
Theorem	onnmin 3013	No member of a set of ordinal numbers belongs to its minimum.
|- ((A (_ On /\ B e. A) -> -. B e. |^|A)
Theorem	onnminsb 3014	An ordinal number smaller than the minimum of a set of ordinal numbers does not have the property determining that set. ps is the wff resulting from the substitution of A for x in wff ph.
|- (x = A -> (ph <-> ps))   =>   |- (A e. On -> (A e. |^|{x e. On | ph} -> -. ps))
Theorem	oneqmini 3015	A way to show that an ordinal number equals the minimum of a collection of ordinal numbers: it must be in the collection, and it must not be larger than any member of the collection.
|- (B (_ On -> ((A e. B /\ A.x e. A -. x e. B) -> A = |^|B))
Theorem	oneqmin 3016	A way to show that an ordinal number equals the minimum of a non-empty collection of ordinal numbers: it must be in the collection, and it must not be larger than any member of the collection.
|- ((B (_ On /\ B =/= (/)) -> (A = |^|B <-> (A e. B /\ A.x e. A -. x e. B)))
Theorem	bm2.5ii 3017	Problem 2.5(ii) of [BellMachover] p. 471.
|- A e. V   =>   |- (A (_ On -> U.A = |^|{x e. On | A.y e. A y (_ x})
Theorem	onminex 3018	If a wff is true for an ordinal number, there is a smallest ordinal number for which it is true.
|- (x = y -> (ph <-> ps))   =>   |- (E.x e. On ph -> E.x e. On (ph /\ A.y e. x -. ps))
Theorem	ord0 3019	The empty set is an ordinal class.
|- Ord (/)
Theorem	0elon 3020	The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193.
|- (/) e. On
Theorem	ord0eln0 3021	A non-empty ordinal contains the empty set.
|- (Ord A -> ((/) e. A <-> A =/= (/)))
Theorem	on0eln0 3022	An ordinal number contains zero iff it is nonzero.
|- (A e. On -> ((/) e. A <-> A =/= (/)))
Theorem	dflim2 3023	An alternate definition of a limit ordinal.
|- (Lim A <-> (Ord A /\ (/) e. A /\ A = U.A))
Theorem	inton 3024	The intersection of the class of ordinal numbers is the empty set.
|- |^|On = (/)
Theorem	nlim0 3025	The empty set is not a limit ordinal.
|- -. Lim (/)
Theorem	limord 3026	A limit ordinal is ordinal.
|- (Lim A -> Ord A)
Theorem	limuni 3027	A limit ordinal is its own supremum (union).
|- (Lim A -> A = U.A)
Theorem	limuni2 3028	The union of a limit ordinal is a limit ordinal.
|- (Lim A -> Lim U.A)
Theorem	0ellim 3029	A limit ordinal contains the empty set.
|- (Lim A -> (/) e. A)
Theorem	limelon 3030	A limit ordinal class that is also a set is an ordinal number.
|- ((A e. B /\ Lim A) -> A e. On)
Theorem	onne0 3031	The class of all ordinal numbers in not empty.
|- On =/= (/)
Theorem	suceq 3032	Equality of successors.
|- (A = B -> suc A = suc B)
Theorem	elsuci 3033	Membership in a successor. This one-way implication does not require that either A or B be sets.
|- (A e. suc B -> (A e. B \/ A = B))
Theorem	elsucg 3034	Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17.
|- (A e. C -> (A e. suc B <-> (A e. B \/ A = B)))
Theorem	elsuc2g 3035	Variant of membership in a successor, requiring that B rather than A be a set.
|- (B e. C -> (A e. suc B <-> (A e. B \/ A = B)))
Theorem	elsuc 3036	Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17.
|- A e. V   =>   |- (A e. suc B <-> (A e. B \/ A = B))
Theorem	elsuc2 3037	Membership in a successor.
|- A e. V   =>   |- (B e. suc A <-> (B e. A \/ B = A))
Theorem	hbsuc 3038	Bound-variable hypothesis builder for successor.
|- (y e. A -> A.x y e. A)   =>   |- (y e. suc A -> A.x y e. suc A)
Theorem	elelsuc 3039	Membership in a successor.
|- (A e. B -> A e. suc B)
Theorem	sucel 3040	Membership of a successor in another class.
|- (suc A e. B <-> E.x e. B A.y(y e. x <-> (y e. A \/ y = A)))
Theorem	suc0 3041	The successor of the empty set.
|- suc (/) = {(/)}
Theorem	sucprc 3042	A proper class is its own successor.
|- (-. A e. V -> suc A = A)
Theorem	sucon 3043	The class of all ordinal numbers is its own successor.
|- suc On = On
Theorem	unisuc 3044	A transitive class is equal to the union of its successor. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73.
|- A e. V   =>   |- (Tr A <-> U.suc A = A)
Theorem	sssucid 3045	A class is included in its own successor. Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized to arbitrary classes).
|- A (_ suc A
Theorem	sucexb 3046	A successor exists iff its class argument exists.
|- (A e. V <-> suc A e. V)
Theorem	sucexg 3047	The successor of a set is a set (generalization).
|- (A e. B -> suc A e. V)
Theorem	sucex 3048	The successor of a set is a set.
|- A e. V   =>   |- suc A e. V
Theorem	sucid 3049	A set belongs to its successor.
|- A e. V   =>   |- A e. suc A
Theorem	sucidg 3050	Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized).
|- (A e. B -> A e. suc A)
Theorem	nsuceq0 3051	No successor is empty.
|- suc A =/= (/)
Theorem	eqelsuc 3052	A set belongs to the successor of an equal set.
|- A e. V   =>   |- (A = B -> A e. suc B)
Theorem	trsuc 3053	A set whose successor belongs to a transitive class also belongs.
|- ((Tr A /\ suc B e. A) -> B e. A)
Theorem	trsucss 3054	A member of the successor of a transitive class is a subclass of it.
|- (Tr A -> (B e. suc A -> B (_ A))
Theorem	ordsssuc 3055	A subset of an ordinal belongs to its successor.
|- ((A e. On /\ Ord B) -> (A (_ B <-> A e. suc B))
Theorem	onsssuc 3056	A subset of an ordinal number belongs to its successor.
|- ((A e. On /\ B e. On) -> (A (_ B <-> A e. suc B))
Theorem	ordsssuc2 3057	An ordinal subset of an ordinal number belongs to its successor.
|- ((Ord A /\ B e. On) -> (A (_ B <-> A e. suc B))
Theorem	onmindif 3058	When its successor is subtracted from a class of ordinal numbers, an ordinal number is less than the minimum of the resulting subclass.
|- ((A (_ On /\ B e. On) -> B e. |^|(A \ suc B))
Theorem	onmindif2 3059	The minimum of a class of ordinal numbers is less than the minimum of that class with its minimum removed.
|- ((A (_ On /\ A =/= (/)) -> |^|A e. |^|(A \ {|^|A}))
Theorem	suceloni 3060	The successor of an ordinal number is an ordinal number. Proposition 7.24 of [TakeutiZaring] p. 41.
|- (A e. On -> suc A e. On)
Theorem	ordnbtwn 3061	There is no set between an ordinal class and its successor. Generalized Proposition 7.25 of [TakeutiZaring] p. 41.
|- (Ord A -> -. (A e. B /\ B e. suc A))
Theorem	onnbtwn 3062	There is no set between an ordinal number and its successor. Proposition 7.25 of [TakeutiZaring] p. 41.
|- (A e. On -> -. (A e. B /\ B e. suc A))
Theorem	ordsuc 3063	The successor of an ordinal class is ordinal.
|- (Ord A <-> Ord suc A)
Theorem	ordpwsuc 3064	The collection of ordinals in the power class of an ordinal is its successor.
|- (Ord A -> (P~A i^i On) = suc A)
Theorem	onpwsuc 3065	The collection of ordinal numbers in the power set of an ordinal number is its successor.
|- (A e. On -> (P~A i^i On) = suc A)
Theorem	sucelon 3066	The successor of an ordinal number is an ordinal number.
|- (A e. On <-> suc A e. On)
Theorem	ordsucss 3067	The successor of an element of an ordinal class is a subset of it.
|- (Ord B -> (A e. B -> suc A (_ B))
Theorem	sucssel 3068	A set whose successor is a subset of another class is a member of that class.
|- (A e. C -> (suc A (_ B -> A e. B))
Theorem	ordelsuc 3069	A set belongs to an ordinal iff its successor is a subset of the ordinal. Exercise 8 of [TakeutiZaring] p. 42 and its converse.
|- ((A e. C /\ Ord B) -> (A e. B <-> suc A (_ B))
Theorem	onsucmin 3070	The successor of an ordinal number is the smallest larger ordinal number.
|- (A e. On -> suc A = |^|{x e. On | A e. x})
Theorem	ordsucelsuc 3071	Membership is inherited by successors. Generalization of Exercise 9 of [TakeutiZaring] p. 42.
|- (Ord B -> (A e. B <-> suc A e. suc B))
Theorem	ordsucsssuc 3072	The subclass relationship between two ordinal classes is inherited by their successors.
|- ((Ord A /\ Ord B) -> (A (_ B <-> suc A (_ suc B))
Theorem	orddif 3073	Ordinal derived from its successor.
|- (Ord A -> A = (suc A \ {A}))
Theorem	orduniss 3074	An ordinal class includes its union.
|- (Ord A -> U.A (_ A)
Theorem	ordtri2or 3075	A trichotomy law for ordinal classes.
|- ((Ord A /\ Ord B) -> (A e. B \/ B (_ A))
Theorem	ordtri2or2 3076	A trichotomy law for ordinal classes.
|- ((Ord A /\ Ord B) -> (A (_ B \/ B (_ A))
Theorem	ordssun 3077	Property of a subclass of the maximum (i.e. union) of two ordinals.
|- ((Ord B /\ Ord C) -> (A (_ (B u. C) <-> (A (_ B \/ A (_ C)))
Theorem	ordequn 3078	The maximum (i.e. union) of two ordinals is either one or the other. Similar to Exercise 14 of [TakeutiZaring] p. 40.
|- ((Ord B /\ Ord C) -> (A = (B u. C) -> (A = B \/ A = C)))
Theorem	ordun 3079	The maximum (i.e. union) of two ordinals is ordinal. Exercise 12 of [TakeutiZaring] p. 40.
|- ((Ord A /\ Ord B) -> Ord (A u. B))
Theorem	ordsucun 3080	The successor of the maximum (i.e. union) of two ordinals is the maximum of their successors.
|- ((Ord