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

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

Type	Label	Description
Statement
Theorem	elsuc 3001	Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17.
|- A e. V   =>   |- (A e. suc B <-> (A e. B \/ A = B))
Theorem	elsuc2 3002	Membership in a successor.
|- A e. V   =>   |- (B e. suc A <-> (B e. A \/ B = A))
Theorem	hbsuc 3003	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 3004	Membership in a successor.
|- (A e. B -> A e. suc B)
Theorem	sucel 3005	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 3006	The successor of the empty set.
|- suc (/) = {(/)}
Theorem	sucprc 3007	A proper class is its own successor.
|- (-. A e. V -> suc A = A)
Theorem	sucon 3008	The class of all ordinals is its own successor.
|- suc On = On
Theorem	unisuc 3009	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 3010	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 3011	A successor exists iff its class argument exists.
|- (A e. V <-> suc A e. V)
Theorem	sucexg 3012	The successor of a set is a set (generalization).
|- (A e. B -> suc A e. V)
Theorem	sucex 3013	The successor of a set is a set.
|- A e. V   =>   |- suc A e. V
Theorem	sucid 3014	A set belongs to its successor.
|- A e. V   =>   |- A e. suc A
Theorem	sucidg 3015	Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized).
|- (A e. B -> A e. suc A)
Theorem	nsuceq0 3016	No successor is empty.
|- suc A =/= (/)
Theorem	eqelsuc 3017	A set belongs to the successor of an equal set.
|- A e. V   =>   |- (A = B -> A e. suc B)
Theorem	trsuc 3018	A set whose successor belongs to a transitive class also belongs.
|- ((Tr A /\ suc B e. A) -> B e. A)
Theorem	trsucss 3019	A member of the successor of a transitive class is a subclass of it.
|- (Tr A -> (B e. suc A -> B (_ A))
Theorem	ordsssuc 3020	A subset of an ordinal belongs to its successor.
|- ((A e. On /\ Ord B) -> (A (_ B <-> A e. suc B))
Theorem	onsssuc 3021	A subset of an ordinal number belongs to its successor.
|- ((A e. On /\ B e. On) -> (A (_ B <-> A e. suc B))
Theorem	ordsssuc2 3022	An ordinal subset of an ordinal number belongs to its successor.
|- ((Ord A /\ B e. On) -> (A (_ B <-> A e. suc B))
Theorem	onmindif 3023	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 3024	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 3025	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 3026	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 3027	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 3028	The successor of an ordinal class is ordinal.
|- (Ord A <-> Ord suc A)
Theorem	ordpwsuc 3029	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 3030	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 3031	The successor of an ordinal number is an ordinal number.
|- (A e. On <-> suc A e. On)
Theorem	ordsucss 3032	The successor of an element of an ordinal class is a subset of it.
|- (Ord B -> (A e. B -> suc A (_ B))
Theorem	sucssel 3033	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 3034	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 3035	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 3036	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 3037	The subclass relationship between two ordinal classes is inherited by their successors.
|- ((Ord A /\ Ord B) -> (A (_ B <-> suc A (_ suc B))
Theorem	orddif 3038	Ordinal derived from its successor.
|- (Ord A -> A = (suc A \ {A}))
Theorem	orduniss 3039	An ordinal class includes its union.
|- (Ord A -> U.A (_ A)
Theorem	ordtri2or 3040	A trichotomy law for ordinal classes.
|- ((Ord A /\ Ord B) -> (A e. B \/ B (_ A))
Theorem	ordtri2or2 3041	A trichotomy law for ordinal classes.
|- ((Ord A /\ Ord B) -> (A (_ B \/ B (_ A))
Theorem	ordssun 3042	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 3043	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 3044	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 3045	The successor of the maximum (i.e. union) of two ordinals is the maximum of their successors.
|- ((Ord A /\ Ord B) -> suc (A u. B) = (suc A u. suc B))
Theorem	ordunisssuc 3046	A subclass relationship for union and successor of ordinal classes.
|- ((A (_ On /\ Ord B) -> (U.A (_ B <-> A (_ suc B))
Theorem	ordunel 3047	The maximum of two ordinals belongs to a third if each of them do.
|- ((Ord A /\ B e. A /\ C e. A) -> (B u. C) e. A)
Theorem	onsucuni 3048	A class of ordinal numbers is a subclass of the successor of its union. Similar to Proposition 7.26 of [TakeutiZaring] p. 41.
|- (A (_ On -> A (_ suc U.A)
Theorem	ordsucuni 3049	An ordinal class is a subclass of the successor of its union.
|- (Ord A -> A (_ suc U.A)
Theorem	orduniorsuc 3050	An ordinal class is either its union or the successor of its union.
|- (Ord A -> (A = U.A \/ A = suc U.A))
Theorem	unon 3051	The class of all ordinals is its own union. Exercise 11 of [TakeutiZaring] p. 40.
|- U.On = On
Theorem	ordunisuc 3052	An ordinal class is equal to the union of its successor.
|- (Ord A -> U.suc A = A)
Theorem	orduniss2 3053	The union of the ordinal subsets of an ordinal number is that number.
|- (Ord A -> U.{x e. On | x (_ A} = A)
Theorem	onsucuni2 3054	A successor ordinal is the successor of its union.
|- ((A e. On /\ A = suc B) -> suc U.A = A)
Theorem	0elsuc 3055	The successor of an ordinal class contains the empty set.
|- (Ord A -> (/) e. suc A)
Theorem	suc11 3056	The successor operation behaves like a one-to-one function. Compare Exercise 16 of [Enderton] p. 194.
|- ((A e. On /\ B e. On) -> (suc A = suc B <-> A = B))
Theorem	limon 3057	The class of ordinal numbers is a limit ordinal.
|- Lim On
Theorem	onord 3058	An ordinal number is an ordinal class.
|- A e. On   =>   |- Ord A
Theorem	ontrc 3059	An ordinal number is a transitive class.
|- A e. On   =>   |- Tr A
Theorem	onirr 3060	An ordinal number is not a member of itself. Theorem 7M(c) of [Enderton] p. 192.
|- A e. On   =>   |- -. A e. A
Theorem	onel 3061	A member of an ordinal number is an ordinal number. Theorem 7M(a) of [Enderton] p. 192.
|- A e. On   =>   |- (B e. A -> B e. On)
Theorem	onss 3062	An ordinal number is a subset of On.
|- A e. On   =>   |- A (_ On
Theorem	onelss 3063	A member of an ordinal number is a subset of it.
|- A e. On   =>   |- (B e. A -> B (_ A)
Theorem	onssneli 3064	An ordering law for ordinals.
|- A e. On   =>   |- (A (_ B -> -. B e. A)
Theorem	onssneli2 3065	An ordering law for ordinals.
|- A e. On   =>   |- (B (_ A -> -. A e. B)
Theorem	onelin 3066	An element of an ordinal number equals the intersection with it.
|- A e. On   =>   |- (B e. A -> B = (B i^i A))
Theorem	onelun 3067	An ordinal number equals its union with any element.
|- A e. On   =>   |- (B e. A -> (A u. B) = A)
Theorem	onsuc 3068	The successor of an ordinal number is an ordinal number. Corollary 7N(c) of [Enderton] p. 193.
|- A e. On   =>   |- suc A e. On
Theorem	onunisuc 3069	An ordinal number is equal to the union of its successor.
|- A e. On   =>   |- U.suc A = A
Theorem	onuniorsuc 3070	An ordinal number is either its own union (if zero or a limit ordinal) or the successor of its union.
|- A e. On   =>   |- (A = U.A \/ A = suc U.A)
Theorem	onuninsuc 3071	A limit ordinal is not a successor ordinal.
|- A e. On   =>   |- (A = U.A <-> -. E.x e. On A = suc x)
Theorem	onssel 3072	Subset is equivalent to membership or equality for ordinal numbers.
|- A e. On   &   |- B e. On   =>   |- (A (_ B <-> (A e. B \/ A = B))
Theorem	onun 3073	The union of two ordinal numbers is an ordinal number.
|- A e. On   &   |- B e. On   =>   |- (A u. B) e. On
Theorem	onsucss 3074	A set belongs to an ordinal number iff its successor is a subset of the ordinal number. Exercise 8 of [TakeutiZaring] p. 42 and its converse.
|- A e. On   &   |- B e. On   =>   |- (A e. B <-> suc A (_ B)
Theorem	nlimsucg 3075	A successor is not a limit ordinal.
|- (A e. B -> -. Lim suc A)
Theorem	unizlim 3076	An ordinal equal to its own union is either zero or a limit ordinal.
|- (Ord A -> (A = U.A <-> (A = (/) \/ Lim A)))
Theorem	orduninsuc 3077	An ordinal equal to its union is not a successor.
|- (Ord A -> (A = U.A <-> -. E.x e. On A = suc x))
Theorem	ordunisuc2 3078	An ordinal equal to its union contains the successor of each of its members.
|- (Ord A -> (A = U.A <-> A.x e. A suc x e. A))
Theorem	ordzsl 3079	An ordinal is zero, a successor ordinal, or a limit ordinal.
|- (Ord A <-> (A = (/) \/ E.x e. On A = suc x \/ Lim A))
Theorem	onzsl 3080	An ordinal number is zero, a successor ordinal, or a limit ordinal number.
|- (A e. On <-> (A = (/) \/ E.x e. On A = suc x \/ (A e. V /\ Lim A)))
Theorem	dflim3 3081	An alternate definition of a limit ordinal, which is any ordinal that is neither zero nor a successor.
|- (Lim A <-> (Ord A /\ -. (A = (/) \/ E.x e. On A = suc x)))
Theorem	dflim4 3082	An alternate definition of a limit ordinal.
|- (Lim A <-> (Ord A /\ (/) e. A /\ A.x e. A suc x e. A))
Theorem	limsuc 3083	The successor of a member of a limit ordinal is also a member.
|- (Lim A -> (B e. A <-> suc B e. A))
Theorem	limsssuc 3084	A class includes a limit ordinal iff the successor of the class includes it.