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

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

Type	Label	Description
Statement
Theorem	ordtr1 3001	Transitive law for ordinal classes.
⊢ (Ord C → ((A ∈ B ⋀ B ∈ C) → A ∈ C))
Theorem	ordtr2 3002	Transitive law for ordinal classes.
⊢ ((Ord A ⋀ Ord C) → ((A ⊆ B ⋀ B ∈ C) → A ∈ C))
Theorem	ontr1 3003	Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192.
⊢ (C ∈ On → ((A ∈ B ⋀ B ∈ C) → A ∈ C))
Theorem	ontr2 3004	Transitive law for ordinal numbers. Exercise 3 of [TakeutiZaring] p. 40.
⊢ ((A ∈ On ⋀ C ∈ On) → ((A ⊆ B ⋀ B ∈ C) → A ∈ C))
Theorem	ordunidif 3005	The union of an ordinal stays the same if a subset equal to one of its elements is removed.
⊢ ((Ord A ⋀ B ∈ A) → ∪(A ∖ B) = ∪A)
Theorem	onint 3006	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 ∈ A)
Theorem	onint0 3007	The intersection of a class of ordinal numbers is zero iff the class contains zero.
⊢ (A ⊆ On → (∩A = ∅ ↔ ∅ ∈ A))
Theorem	onssmin 3008	A non-empty class of ordinal numbers has a smallest member. Exercise 9 of [TakeutiZaring] p. 40.
⊢ ((A ⊆ On ⋀ A ≠ ∅) → ∃x ∈ A ∀y ∈ A x ⊆ y)
Theorem	onminsb 3009	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.
⊢ (ψ → ∀xψ)    &   ⊢ (x = ∩{x ∈ On∣φ} → (φ ↔ ψ))    ⇒   ⊢ (∃x ∈ On φ → ψ)
Theorem	onminesb 3010	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.
⊢ (∃x ∈ On φ → [∩{x ∈ On∣φ} / x]φ)
Theorem	onintss 3011	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 → (φ ↔ ψ))    ⇒   ⊢ (A ∈ On → (ψ → ∩{x ∈ On∣φ} ⊆ A))
Theorem	oninton 3012	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 ∈ On)
Theorem	onintrab 3013	The intersection of a class of ordinal numbers exists iff it is an ordinal number.
⊢ (∩{x ∈ On∣φ} ∈ V ↔ ∩{x ∈ On∣φ} ∈ On)
Theorem	onintrab2 3014	An existence condition equivalent to an intersection's being an ordinal number.
⊢ (∃x ∈ On φ ↔ ∩{x ∈ On∣φ} ∈ On)
Theorem	onnmin 3015	No member of a set of ordinal numbers belongs to its minimum.
⊢ ((A ⊆ On ⋀ B ∈ A) → ¬ B ∈ ∩A)
Theorem	onnminsb 3016	An ordinal number smaller than the minimum of a set of ordinal numbers does not have the property determining that set. ψ is the wff resulting from the substitution of A for x in wff φ.
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ On → (A ∈ ∩{x ∈ On∣φ} → ¬ ψ))
Theorem	oneqmini 3017	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 ∈ B ⋀ ∀x ∈ A ¬ x ∈ B) → A = ∩B))
Theorem	oneqmin 3018	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 ∈ B ⋀ ∀x ∈ A ¬ x ∈ B)))
Theorem	bm2.5ii 3019	Problem 2.5(ii) of [BellMachover] p. 471.
⊢ A ∈ V    ⇒   ⊢ (A ⊆ On → ∪A = ∩{x ∈ On∣∀y ∈ A y ⊆ x})
Theorem	onminex 3020	If a wff is true for an ordinal number, there is a smallest ordinal number for which it is true.
⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∃x ∈ On φ → ∃x ∈ On (φ ⋀ ∀y ∈ x ¬ ψ))
Theorem	ord0 3021	The empty set is an ordinal class.
⊢ Ord ∅
Theorem	0elon 3022	The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193.
⊢ ∅ ∈ On
Theorem	ord0eln0 3023	A non-empty ordinal contains the empty set.
⊢ (Ord A → (∅ ∈ A ↔ A ≠ ∅))
Theorem	on0eln0 3024	An ordinal number contains zero iff it is nonzero.
⊢ (A ∈ On → (∅ ∈ A ↔ A ≠ ∅))
Theorem	dflim2 3025	An alternate definition of a limit ordinal.
⊢ (Lim A ↔ (Ord A ⋀ ∅ ∈ A ⋀ A = ∪A))
Theorem	inton 3026	The intersection of the class of ordinal numbers is the empty set.
⊢ ∩On = ∅
Theorem	nlim0 3027	The empty set is not a limit ordinal.
⊢ ¬ Lim ∅
Theorem	limord 3028	A limit ordinal is ordinal.
⊢ (Lim A → Ord A)
Theorem	limuni 3029	A limit ordinal is its own supremum (union).
⊢ (Lim A → A = ∪A)
Theorem	limuni2 3030	The union of a limit ordinal is a limit ordinal.
⊢ (Lim A → Lim ∪A)
Theorem	0ellim 3031	A limit ordinal contains the empty set.
⊢ (Lim A → ∅ ∈ A)
Theorem	limelon 3032	A limit ordinal class that is also a set is an ordinal number.
⊢ ((A ∈ B ⋀ Lim A) → A ∈ On)
Theorem	onne0 3033	The class of all ordinal numbers in not empty.
⊢ On ≠ ∅
Theorem	suceq 3034	Equality of successors.
⊢ (A = B → suc A = suc B)
Theorem	elsuci 3035	Membership in a successor. This one-way implication does not require that either A or B be sets.
⊢ (A ∈ suc B → (A ∈ B ⋁ A = B))
Theorem	elsucg 3036	Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17.
⊢ (A ∈ C → (A ∈ suc B ↔ (A ∈ B ⋁ A = B)))
Theorem	elsuc2g 3037	Variant of membership in a successor, requiring that B rather than A be a set.
⊢ (B ∈ C → (A ∈ suc B ↔ (A ∈ B ⋁ A = B)))
Theorem	elsuc 3038	Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17.
⊢ A ∈ V    ⇒   ⊢ (A ∈ suc B ↔ (A ∈ B ⋁ A = B))
Theorem	elsuc2 3039	Membership in a successor.
⊢ A ∈ V    ⇒   ⊢ (B ∈ suc A ↔ (B ∈ A ⋁ B = A))
Theorem	hbsuc 3040	Bound-variable hypothesis builder for successor.
⊢ (y ∈ A → ∀x y ∈ A)    ⇒   ⊢ (y ∈ suc A → ∀x y ∈ suc A)
Theorem	elelsuc 3041	Membership in a successor.
⊢ (A ∈ B → A ∈ suc B)
Theorem	sucel 3042	Membership of a successor in another class.
⊢ (suc A ∈ B ↔ ∃x ∈ B ∀y(y ∈ x ↔ (y ∈ A ⋁ y = A)))
Theorem	suc0 3043	The successor of the empty set.
⊢ suc ∅ = {∅}
Theorem	sucprc 3044	A proper class is its own successor.
⊢ (¬ A ∈ V → suc A = A)
Theorem	sucon 3045	The class of all ordinal numbers is its own successor.
⊢ suc On = On
Theorem	unisuc 3046	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 ∈ V    ⇒   ⊢ (Tr A ↔ ∪suc A = A)
Theorem	sssucid 3047	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 3048	A successor exists iff its class argument exists.
⊢ (A ∈ V ↔ suc A ∈ V)
Theorem	sucexg 3049	The successor of a set is a set (generalization).
⊢ (A ∈ B → suc A ∈ V)
Theorem	sucex 3050	The successor of a set is a set.
⊢ A ∈ V    ⇒   ⊢ suc A ∈ V
Theorem	sucid 3051	A set belongs to its successor.
⊢ A ∈ V    ⇒   ⊢ A ∈ suc A
Theorem	sucidg 3052	Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized).
⊢ (A ∈ B → A ∈ suc A)
Theorem	nsuceq0 3053	No successor is empty.
⊢ suc A ≠ ∅
Theorem	eqelsuc 3054	A set belongs to the successor of an equal set.
⊢ A ∈ V    ⇒   ⊢ (A = B → A ∈ suc B)
Theorem	trsuc 3055	A set whose successor belongs to a transitive class also belongs.
⊢ ((Tr A ⋀ suc B ∈ A) → B ∈ A)
Theorem	trsucss 3056	A member of the successor of a transitive class is a subclass of it.
⊢ (Tr A → (B ∈ suc A → B ⊆ A))
Theorem	ordsssuc 3057	A subset of an ordinal belongs to its successor.
⊢ ((A ∈ On ⋀ Ord B) → (A ⊆ B ↔ A ∈ suc B))
Theorem	onsssuc 3058	A subset of an ordinal number belongs to its successor.
⊢ ((A ∈ On ⋀ B ∈ On) → (A ⊆ B ↔ A ∈ suc B))
Theorem	ordsssuc2 3059	An ordinal subset of an ordinal number belongs to its successor.
⊢ ((Ord A ⋀ B ∈ On) → (A ⊆ B ↔ A ∈ suc B))
Theorem	onmindif 3060	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 ∈ On) → B ∈ ∩(A ∖ suc B))
Theorem	onmindif2 3061	The minimum of a class of ordinal numbers is less than the minimum of that class with its minimum removed.
⊢ ((A ⊆ On ⋀ A ≠ ∅) → ∩A ∈ ∩(A ∖ {∩A}))
Theorem	suceloni 3062	The successor of an ordinal number is an ordinal number. Proposition 7.24 of [TakeutiZaring] p. 41.
⊢ (A ∈ On → suc A ∈ On)
Theorem	ordnbtwn 3063	There is no set between an ordinal class and its successor. Generalized Proposition 7.25 of [TakeutiZaring] p. 41.
⊢ (Ord A → ¬ (A ∈ B ⋀ B ∈ suc A))
Theorem	onnbtwn 3064	There is no set between an ordinal number and its successor. Proposition 7.25 of [TakeutiZaring] p. 41.
⊢ (A ∈ On → ¬ (A ∈ B ⋀ B ∈ suc A))
Theorem	ordsuc 3065	The successor of an ordinal class is ordinal.
⊢ (Ord A ↔ Ord suc A)
Theorem	ordpwsuc 3066	The collection of ordinals in the power class of an ordinal is its successor.
⊢ (Ord A → (℘A ∩ On) = suc A)
Theorem	onpwsuc 3067	The collection of ordinal numbers in the power set of an ordinal number is its successor.
⊢ (A ∈ On → (℘A ∩ On) = suc A)
Theorem	sucelon 3068	The successor of an ordinal number is an ordinal number.
⊢ (A ∈ On ↔ suc A ∈ On)
Theorem	ordsucss 3069	The successor of an element of an ordinal class is a subset of it.
⊢ (Ord B → (A ∈ B → suc A ⊆ B))
Theorem	sucssel 3070	A set whose successor is a subset of another class is a member of that class.
⊢ (A ∈ C → (suc A ⊆ B → A ∈ B))
Theorem	ordelsuc 3071	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 ∈ C ⋀ Ord B) → (A ∈ B ↔ suc A ⊆ B))
Theorem	onsucmin 3072	The successor of an ordinal number is the smallest larger ordinal number.
⊢ (A ∈ On → suc A = ∩{x ∈ On∣A ∈ x})
Theorem	ordsucelsuc 3073	Membership is inherited by successors. Generalization of Exercise 9 of [TakeutiZaring] p. 42.
⊢ (Ord B → (A ∈ B ↔ suc A ∈ suc B))
Theorem	ordsucsssuc 3074	The subclass relationship between two ordinal classes is inherited by their successors.
⊢ ((Ord A ⋀ Ord B) → (A ⊆ B ↔ suc A ⊆ suc B))
Theorem	orddif 3075	Ordinal derived from its successor.
⊢ (Ord A → A = (suc A ∖ {A}))
Theorem	orduniss 3076	An ordinal class includes its union.
⊢ (Ord A → ∪A ⊆ A)
Theorem	ordtri2or 3077	A trichotomy law for ordinal classes.
⊢ ((Ord A ⋀ Ord B) → (A ∈ B ⋁ B ⊆ A))
Theorem	ordtri2or2 3078	A trichotomy law for ordinal classes.
⊢ ((Ord A ⋀ Ord B) → (A ⊆ B ⋁ B ⊆ A))
Theorem	ordssun 3079	Property of a subclass of the maximum (i.e. union) of two ordinals.
⊢ ((Ord B ⋀ Ord C) → (A ⊆ (B ∪ C) ↔ (A ⊆ B ⋁ A ⊆ C)))
Theorem	ordequn 3080	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 ∪ C) → (A = B ⋁ A = C)))
Theorem	ordun 3081	The maximum (i.e. union) of two ordinals is ordinal. Exercise 12 of [TakeutiZaring] p. 40.
⊢ ((Ord A ⋀ Ord B) → Ord (A ∪ B))
Theorem	ordsucun 3082	The successor of the maximum (i.e. union) of two ordinals is the maximum of their successors.
⊢ ((Ord A ⋀ Ord B) → suc (A ∪ B) = (suc A ∪ suc B))
Theorem	ordunisssuc 3083	A subclass relationship for union and successor of ordinal classes.
⊢ ((A ⊆ On ⋀ Ord B) → (∪A ⊆ B ↔ A ⊆ suc B))
Theorem	ordunel 3084	The maximum of two ordinals belongs to a third if each of them do.
⊢ ((Ord A ⋀ B ∈ A ⋀ C ∈ A) → (B ∪ C) ∈ A)
Theorem	onsucuni 3085	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 ∪A)
Theorem	ordsucuni 3086	An ordinal class is a subclass of the successor of its union.
⊢ (Ord A → A ⊆ suc ∪A)
Theorem	orduniorsuc 3087	An ordinal class is either its union or the successor of its union.
⊢ (Ord A → (A = ∪A ⋁ A = suc ∪A))
Theorem	unon 3088	The class of all ordinal numbers is its own union. Exercise 11 of [TakeutiZaring] p. 40.
⊢ ∪On = On
Theorem	ordunisuc 3089	An ordinal class is equal to the union of its successor.
⊢ (Ord A → ∪suc A = A)
Theorem	orduniss2 3090	The union of the ordinal subsets of an ordinal number is that number.
⊢ (Ord A → ∪{x ∈ On∣x ⊆ A} = A)
Theorem	onsucuni2 3091	A successor ordinal is the successor of its union.
⊢ ((A ∈ On ⋀ A = suc B) → suc ∪A = A)
Theorem	0elsuc 3092	The successor of an ordinal class contains the empty set.
⊢ (Ord A → ∅ ∈ suc A)
Theorem	suc11 3093	The successor operation behaves like a one-to-one function. Compare Exercise 16 of [Enderton] p. 194.
⊢ ((A ∈ On ⋀ B ∈ On) → (suc A = suc B ↔ A = B))
Theorem	limon 3094	The class of ordinal numbers is a limit ordinal.
⊢ Lim On
Theorem	onord 3095	An ordinal number is an ordinal class.
⊢ A ∈ On    ⇒   ⊢ Ord A
Theorem	ontrc 3096	An ordinal number is a transitive class.
⊢ A ∈ On    ⇒   ⊢ Tr A
Theorem	onirr 3097	An ordinal number is not a member of itself. Theorem 7M(c) of [Enderton] p. 192.
⊢ A ∈ On    ⇒   ⊢ ¬ A ∈ A
Theorem	onel 3098	A member of an ordinal number is an ordinal number. Theorem 7M(a) of [Enderton] p. 192.
⊢ A ∈ On    ⇒   ⊢ (B ∈ A → B ∈ On)
Theorem	onss 3099	An ordinal number is a subset of On.
⊢ A ∈ On    ⇒   ⊢ A ⊆ On
Theorem	onelss 3100	A member of an ordinal number is a subset of it.
⊢ A ∈ On    ⇒   ⊢ (B ∈ A → B ⊆ A)