Metamath Proof Explorer - mmtheorems32

Jump to page: 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-5787

Statement List for Metamath Proof Explorer - 3101-3200 - Page 32 of 58

Type	Label	Description
Statement
Syntax	coa 3101	Extend the definition of a class to include the ordinal addition operation.
class +o
Syntax	comu 3102	Extend the definition of a class to include the ordinal multiplication operation.
class ·o
Syntax	coe 3103	Extend the definition of a class to include the ordinal exponentiation operation.
class ↑o
Definition	df-1o 3104	Define the ordinal number 1.
⊢ 1o = suc ∅
Definition	df-2o 3105	Define the ordinal number 2.
⊢ 2o = suc 1o
Definition	df-oadd 3106	Define the ordinal addition operation.
⊢ +o = {⟨⟨x, y⟩, z⟩∣((x ∈ On ∧ y ∈ On) ∧ z = (rec({⟨w, v⟩∣v = suc w}, x) ‘y))}
Definition	df-omul 3107	Define the ordinal multiplication operation.
⊢ ·o = {⟨⟨x, y⟩, z⟩∣((x ∈ On ∧ y ∈ On) ∧ z = (rec({⟨w, v⟩∣v = (w +o x)}, ∅) ‘y))}
Definition	df-oexp 3108	Define the ordinal exponentiation operation.
⊢ ↑o = {⟨⟨x, y⟩, z⟩∣((x ∈ On ∧ y ∈ On) ∧ z = if(x = ∅, (1o ∖ y), (rec({⟨w, v⟩∣v = (w ·o x)}, 1o) ‘y)))}
Theorem	1o 3109	Ordinal 1 is an ordinal number.
⊢ 1o ∈ On
Theorem	2o 3110	Ordinal 2 is an ordinal number.
⊢ 2o ∈ On
Theorem	df1o2 3111	Expanded value of the ordinal number 1.
⊢ 1o = {∅}
Theorem	df2o2 3112	Expanded value of the ordinal number 2.
⊢ 2o = {∅, {∅}}
Theorem	0ne1oOLD 3113	Ordinal zero is not equal to ordinal one.
⊢ ¬ ∅ = 1o
Theorem	ordgt0ge1 3114	Two ways of expressing that an ordinal class is positive.
⊢ (Ord A → (∅ ∈ A ↔ 1o ⊆ A))
Theorem	el1o 3115	Membership in ordinal one.
⊢ (A ∈ 1o ↔ A = ∅)
Theorem	0lt1o 3116	Ordinal zero is less than ordinal one.
⊢ ∅ ∈ 1o
Theorem	fnoa 3117	Functionality and domain of ordinal addition.
⊢ +o Fn (On × On)
Theorem	fnom 3118	Functionality and domain of ordinal multiplication.
⊢ ·o Fn (On × On)
Theorem	oav 3119	Value of ordinal addition.
⊢ ((A ∈ On ∧ B ∈ On) → (A +o B) = (rec({⟨x, y⟩∣y = suc x}, A) ‘B))
Theorem	omv 3120	Value of ordinal multiplication.
⊢ ((A ∈ On ∧ B ∈ On) → (A ·o B) = (rec({⟨x, y⟩∣y = (x +o A)}, ∅) ‘B))
Theorem	oe0lem 3121	A helper lemma for oe0 3130 and others.
⊢ ((φ ∧ A = ∅) → ψ)    &   ⊢ (((A ∈ On ∧ φ) ∧ ∅ ∈ A) → ψ)    ⇒   ⊢ ((A ∈ On ∧ φ) → ψ)
Theorem	oev 3122	Value of ordinal exponentiation.
⊢ ((A ∈ On ∧ B ∈ On) → (A ↑o B) = if(A = ∅, (1o ∖ B), (rec({⟨x, y⟩∣y = (x ·o A)}, 1o) ‘B)))
Theorem	oevn0 3123	Value of ordinal exponentiation at a nonzero mantissa.
⊢ (((A ∈ On ∧ B ∈ On) ∧ ∅ ∈ A) → (A ↑o B) = (rec({⟨x, y⟩∣y = (x ·o A)}, 1o) ‘B))
Theorem	oa0 3124	Addition with zero. Proposition 8.3 of [TakeutiZaring] p. 57.
⊢ (A ∈ On → (A +o ∅) = A)
Theorem	om0 3125	Ordinal multiplication with zero. Definition 8.15 of [TakeutiZaring] p. 62.
⊢ (A ∈ On → (A ·o ∅) = ∅)
Theorem	om0x 3126	Ordinal multiplication with zero. Definition 8.15 of [TakeutiZaring] p. 62. Unlike om0 3125, this version works whether or not A is an ordinal. However it since it is an artifact of our particular function value definition outside the domain, we will not use it in order to be conventional and present it only as a curiosity.
⊢ (A ·o ∅) = ∅
Theorem	oe0m 3127	Ordinal exponentiation with zero mantissa.
⊢ (A ∈ On → (∅ ↑o A) = (1o ∖ A))
Theorem	oe0m0 3128	Ordinal exponentiation with zero mantissa and zero exponent. Proposition 8.31 of [TakeutiZaring] p. 67.
⊢ (∅ ↑o ∅) = 1o
Theorem	oe0m1 3129	Ordinal exponentiation with zero mantissa and nonzero exponent. Proposition 8.31(2) of [TakeutiZaring] p. 67.
⊢ ((A ∈ On ∧ ∅ ∈ A) → (∅ ↑o A) = ∅)
Theorem	oe0 3130	Ordinal exponentiation with zero exponent. Definition 8.30 of [TakeutiZaring] p. 67.
⊢ (A ∈ On → (A ↑o ∅) = 1o)
Theorem	oasuc 3131	Addition with successor. Definition 8.1 of [TakeutiZaring] p. 56.
⊢ ((A ∈ On ∧ B ∈ On) → (A +o suc B) = suc (A +o B))
Theorem	oa1suc 3132	Addition with 1 is same as successor. Proposition 4.34(a) of [Mendelson] p. 266.
⊢ (A ∈ On → (A +o 1o) = suc A)
Theorem	omsuc 3133	Multiplication with successor. Definition 8.15 of [TakeutiZaring] p. 62.
⊢ ((A ∈ On ∧ B ∈ On) → (A ·o suc B) = ((A ·o B) +o A))
Theorem	oesuc 3134	Ordinal exponentiation with a successor exponent. Definition 8.30 of [TakeutiZaring] p. 67.
⊢ ((A ∈ On ∧ B ∈ On) → (A ↑o suc B) = ((A ↑o B) ·o A))
Theorem	oalim 3135	Ordinal addition with a limit ordinal. Definition 8.1 of [TakeutiZaring] p. 56.
⊢ ((A ∈ On ∧ (B ∈ C ∧ Lim B)) → (A +o B) = ∪x ∈ B (A +o x))
Theorem	omlim 3136	Ordinal multiplication with a limit ordinal. Definition 8.15 of [TakeutiZaring] p. 62.
⊢ ((A ∈ On ∧ (B ∈ C ∧ Lim B)) → (A ·o B) = ∪x ∈ B (A ·o x))
Theorem	oelim 3137	Ordinal exponentiation with a limit exponent and nonzero mantissa. Definition 8.30 of [TakeutiZaring] p. 67.
⊢ (((A ∈ On ∧ (B ∈ C ∧ Lim B)) ∧ ∅ ∈ A) → (A ↑o B) = ∪x ∈ B (A ↑o x))
Theorem	oacl 3138	Closure law for ordinal addition. Proposition 8.2 of [TakeutiZaring] p. 57.
⊢ ((A ∈ On ∧ B ∈ On) → (A +o B) ∈ On)
Theorem	omcl 3139	Closure law for ordinal multiplication. Proposition 8.16 of [TakeutiZaring] p. 57.
⊢ ((A ∈ On ∧ B ∈ On) → (A ·o B) ∈ On)
Theorem	oecl 3140	Closure law for ordinal exponentiation.
⊢ ((A ∈ On ∧ B ∈ On) → (A ↑o B) ∈ On)
Theorem	oa0r 3141	Ordinal addition with zero. Proposition 8.3 of [TakeutiZaring] p. 57.
⊢ (A ∈ On → (∅ +o A) = A)
Theorem	om0r 3142	Ordinal multiplication with zero. Proposition 8.18(1) of [TakeutiZaring] p. 63.
⊢ (A ∈ On → (∅ ·o A) = ∅)
Theorem	o1p1e2 3143	1 + 1 = 2 for ordinal numbers.
⊢ (1o +o 1o) = 2o
Theorem	om1 3144	Ordinal multiplication with 1. Proposition 8.18(2) of [TakeutiZaring] p. 63.
⊢ (A ∈ On → (A ·o 1o) = A)
Theorem	om1r 3145	Ordinal multiplication with 1. Proposition 8.18(2) of [TakeutiZaring] p. 63.
⊢ (A ∈ On → (1o ·o A) = A)
Theorem	oe1 3146	Ordinal exponentiation with an exponent of 1.
⊢ (A ∈ On → (A ↑o 1o) = A)
Theorem	oe1m 3147	Ordinal exponentiation with a mantissa of 1. Proposition 8.31(3) of [TakeutiZaring] p. 67.
⊢ (A ∈ On → (1o ↑o A) = 1o)
Theorem	oaordi 3148	Ordering property of ordinal addition. Proposition 8.4 of [TakeutiZaring] p. 58.
⊢ ((B ∈ On ∧ C ∈ On) → (A ∈ B → (C +o A) ∈ (C +o B)))
Theorem	oaord 3149	Ordering property of ordinal addition. Proposition 8.4 of [TakeutiZaring] p. 58 and its converse.
⊢ ((A ∈ On ∧ B ∈ On ∧ C ∈ On) → (A ∈ B ↔ (C +o A) ∈ (C +o B)))
Theorem	oacan 3150	Left cancellation law for ordinal addition. Corollary 8.5 of [TakeutiZaring] p. 58.
⊢ ((A ∈ On ∧ B ∈ On ∧ C ∈ On) → ((A +o B) = (A +o C) ↔ B = C))
Theorem	oaword 3151	Weak ordering property of ordinal addition.
⊢ ((A ∈ On ∧ B ∈ On ∧ C ∈ On) → (A ⊆ B ↔ (C +o A) ⊆ (C +o B)))
Theorem	oawordri 3152	Weak ordering property of ordinal addition. Proposition 8.7 of [TakeutiZaring] p. 59.
⊢ ((A ∈ On ∧ B ∈ On ∧ C ∈ On) → (A ⊆ B → (A +o C) ⊆ (B +o C)))
Theorem	oaord1 3153	An ordinal is less than its sum with a non-zero ordinal. Theorem 18 of [Suppes] p. 209 and its converse.
⊢ ((A ∈ On ∧ B ∈ On) → (∅ ∈ B ↔ A ∈ (A +o B)))
Theorem	oaword1 3154	An ordinal is less than or equal to its sum with another. Part of Exercise 5 of [TakeutiZaring] p. 62. (For the other part see oaord1 3153.)
⊢ ((A ∈ On ∧ B ∈ On) → A ⊆ (A +o B))
Theorem	oaword2 3155	An ordinal is less than or equal to its sum with another. Theorem 21 of [Suppes] p. 209.
⊢ ((A ∈ On ∧ B ∈ On) → A ⊆ (B +o A))
Theorem	oawordeulem 3156	Lemma for oawordex 3159.
⊢ A ∈ On    &   ⊢ B ∈ On    &   ⊢ S = {y ∈ On∣B ⊆ (A +o y)}    ⇒   ⊢ (A ⊆ B → ∃!x ∈ On (A +o x) = B)
Theorem	oawordeu 3157	Existence theorem for weak ordering of ordinal sum. Proposition 8.8 of [TakeutiZaring] p. 59.
⊢ (((A ∈ On ∧ B ∈ On) ∧ A ⊆ B) → ∃!x ∈ On (A +o x) = B)
Theorem	oawordexr 3158	Existence theorem for weak ordering of ordinal sum.
⊢ ((A ∈ On ∧ ∃x ∈ On (A +o x) = B) → A ⊆ B)
Theorem	oawordex 3159	Existence theorem for weak ordering of ordinal sum. Proposition 8.8 of [TakeutiZaring] p. 59 and its converse. See oawordeu 3157 for uniqueness.
⊢ ((A ∈ On ∧ B ∈ On) → (A ⊆ B ↔ ∃x ∈ On (A +o x) = B))
Theorem	oaordex 3160	Existence theorem for ordering of ordinal sum. Similar to Proposition 4.34(f) of [Mendelson] p. 266 and its converse.
⊢ ((A ∈ On ∧ B ∈ On) → (A ∈ B ↔ ∃x ∈ On (∅ ∈ x ∧ (A +o x) = B)))
Theorem	oa00 3161	An ordinal sum is zero iff both of its arguments are zero.
⊢ ((A ∈ On ∧ B ∈ On) → ((A +o B) = ∅ ↔ (A = ∅ ∧ B = ∅)))
Theorem	oalimcl 3162	The ordinal sum with a limit ordinal is a limit ordinal. Proposition 8.11 of [TakeutiZaring] p. 60.
⊢ ((A ∈ On ∧ (B ∈ C ∧ Lim B)) → Lim (A +o B))
Theorem	oaass 3163	Ordinal addition is associative. Theorem 25 of [Suppes] p. 211.
⊢ ((A ∈ On ∧ B ∈ On ∧ C ∈ On) → ((A +o B) +o C) = (A +o (B +o C)))
Theorem	omordi 3164	Ordering property of ordinal multiplication. Half of Proposition 8.19 of [TakeutiZaring] p. 63.
⊢ (((B ∈ On ∧ C ∈ On) ∧ ∅ ∈ C) → (A ∈ B → (C ·o A) ∈ (C ·o B)))
Theorem	oen0 3165	Ordinal exponentiation with a nonzero mantissa is nonzero. Proposition 8.32 of [TakeutiZaring] p. 67.
⊢ (((A ∈ On ∧ B ∈ On) ∧ ∅ ∈ A) → ∅ ∈ (A ↑o B))
Theorem	nna0 3166	Addition with zero. Theorem 4I(A1) of [Enderton] p. 79.
⊢ (A ∈ ω → (A +o ∅) = A)
Theorem	nnm0 3167	Multiplication with zero. Theorem 4J(A1) of [Enderton] p. 80.
⊢ (A ∈ ω → (A ·o ∅) = ∅)
Theorem	nnasuc 3168	Addition with successor. Theorem 4I(A2) of [Enderton] p. 79.
⊢ ((A ∈ ω ∧ B ∈ ω) → (A +o suc B) = suc (A +o B))
Theorem	nnmsuc 3169	Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80.
⊢ ((A ∈ ω ∧ B ∈ ω) → (A ·o suc B) = ((A ·o B) +o A))
Theorem	nna0r 3170	Addition to zero. Remark in proof of Theorem 4K(2) of [Enderton] p. 81.
⊢ (A ∈ ω → (∅ +o A) = A)
Theorem	nnm0r 3171	Multiplication with zero. Exercise 16 of [Enderton] p. 82.
⊢ (A ∈ ω → (∅ ·o A) = ∅)
Theorem	nnacl 3172	Closure of addition of natural numbers. Proposition 8.9 of [TakeutiZaring] p. 59.
⊢ ((A ∈ ω ∧ B ∈ ω) → (A +o B) ∈ ω)
Theorem	nnmcl 3173	Closure of multiplication of natural numbers. Proposition 8.17 of [TakeutiZaring] p. 63.
⊢ ((A ∈ ω ∧ B ∈ ω) → (A ·o B) ∈ ω)
Theorem	nnarcl 3174	Reverse closure law for addition of natural numbers. Exercise 1 of [TakeutiZaring] p. 62 and its converse.
⊢ ((A ∈ On ∧ B ∈ On) → ((A +o B) ∈ ω ↔ (A ∈ ω ∧ B ∈ ω)))
Theorem	nnacom 3175	Addition of natural numbers is commutative. Theorem 4K(2) of [Enderton] p. 81.
⊢ ((A ∈ ω ∧ B ∈ ω) → (A +o B) = (B +o A))
Theorem	nnaordi 3176	Ordering property of addition. Proposition 8.4 of [TakeutiZaring] p. 58, limited to natural numbers.
⊢ ((B ∈ ω ∧ C ∈ ω) → (A ∈ B → (C +o A) ∈ (C +o B)))
Theorem	nnaord 3177	Ordering property of addition. Proposition 8.4 of [TakeutiZaring] p. 58, limited to natural numbers, and its converse.
⊢ ((A ∈ ω ∧ B ∈ ω ∧ C ∈ ω) → (A ∈ B ↔ (C +o A) ∈ (C +o B)))
Theorem	nnaordr 3178	Ordering property of addition of natural numbers.
⊢ ((A ∈ ω ∧ B ∈ ω ∧ C ∈ ω) → (A ∈ B ↔ (A +o C) ∈ (B +o C)))
Theorem	nnaass 3179	Addition of natural numbers is associative. (This can be extended to all ordinals with a longer proof.) Theorem 4K(1) of [Enderton] p. 81.
⊢ ((A ∈ ω ∧ B ∈ ω ∧ C ∈ ω) → ((A +o B) +o C) = (A +o (B +o C)))
Theorem	nndi 3180	Distributive law for natural numbers. (This can be extended to all ordinals with a longer proof.) Theorem 4K(3) of [Enderton] p. 81.
⊢ ((A ∈ ω ∧ B ∈ ω ∧ C ∈ ω) → (A ·o (B +o C)) = ((A ·o B) +o (A ·o C)))
Theorem	nnmass 3181	Multiplication of natural numbers is associative. (This can be extended to all ordinals with a longer proof.) Theorem 4K(4) of [Enderton] p. 81.
⊢ ((A ∈ ω ∧ B ∈ ω ∧ C ∈ ω) → ((A ·o B) ·o C) = (A ·o (B ·o C)))
Theorem	nnmsucr 3182	Multiplication with successor. Exercise 16 of [Enderton] p. 82.
⊢ ((A ∈ ω ∧ B ∈ ω) → (suc A ·o B) = ((A ·o B) +o B))
Theorem	nnmcom 3183	Multiplication of natural numbers is commutative. Theorem 4K(5) of [Enderton] p. 81.
⊢ ((A ∈ ω ∧ B ∈ ω) → (A ·o B) = (B ·o A))
Theorem	nnacan 3184	Cancellation law for addition of natural numbers.
⊢ ((A ∈ ω ∧ B ∈ ω ∧ C ∈ ω) → ((A +o B) = (A +o C) ↔ B = C))
Theorem	nnaword 3185	Weak ordering property of addition.
⊢ ((A ∈ ω ∧ B ∈ ω ∧ C ∈ ω) → (A ⊆ B ↔ (C +o A) ⊆ (C +o B)))
Theorem	nnaword1 3186	Weak ordering property of addition.
⊢ ((A ∈ ω ∧ B ∈ ω) → A ⊆ (A +o B))
Theorem	nnaword2 3187	Weak ordering property of addition.
⊢ ((A ∈ ω ∧ B ∈ ω) → A ⊆ (B +o A))
Theorem	nnmordi 3188	Ordering property of multiplication. Half of Proposition 8.19 of [TakeutiZaring] p. 63, limited to natural numbers.
⊢ ((A ∈ ω ∧ B ∈ ω ∧ C ∈ ω) → ((A ∈ B ∧ ∅ ∈ C) → (C ·o A) ∈ (C ·o B)))
Theorem	nnmord 3189	Ordering property of multiplication. Proposition 8.19 of [TakeutiZaring] p. 63, limited to natural numbers.
⊢ ((A ∈ ω ∧ B ∈ ω ∧ C ∈ ω) → ((A ∈ B ∧ ∅ ∈ C) ↔ (C ·o A) ∈ (C ·o B)))
Theorem	nnmcan 3190	Cancellation law for multiplication of natural numbers.
⊢ (((A ∈ ω ∧ B ∈ ω ∧ C ∈ ω) ∧ ∅ ∈ A) → ((A ·o B) = (A ·o C) ↔ B = C))
Theorem	nnaordex 3191	Equivalence for ordering. Compare Exercise 23 of [Enderton] p. 88.
⊢ ((A ∈ ω ∧ B ∈ ω) → (A ∈ B ↔ ∃x ∈ ω (∅ ∈ x ∧ (A +o x) = B)))
Theorem	nnawordex 3192	Equivalence for weak ordering of natural numbers.
⊢ ((A ∈ ω ∧ B ∈ ω) → (A ⊆ B ↔ ∃x ∈ ω (A +o x) = B))
Theorem	1onn 3193	One is a natural number.
⊢ 1o ∈ ω
Theorem	2onn 3194	The ordinal 2 is a natural number.
⊢ 2o ∈ ω
Theorem	omsmolem 3195	Lemma for omsmo 3196.
⊢ (y ∈ ω → (((A ⊆ On ∧ F:ω–→A) ∧ ∀x ∈ ω (F ‘x) ∈ (F ‘suc x)) → (z ∈ y → (F ‘z) ∈ (F ‘y))))
Theorem	omsmo 3196	A strictly monotonic ordinal function on the set of natural numbers is one-to-one.
⊢ (((A ⊆ On ∧ F:ω–→A) ∧ ∀x ∈ ω (F ‘x) ∈ (F ‘suc x)) → F:ω–1-1→A)
Syntax	wer 3197	Extend the definition of a wff to include the equivalence predicate.
wff Er R
Syntax	cec 3198	Extend the definition of a class to include equivalence class.
class [A]R
Syntax	cqs 3199	Extend the definition of a class to include quotient set.
class (A / R)
Definition	df-er 3200	Define the equivalence predicate. R need not be a relation but ordinarily will be, in which case we call it an equivalence relation. Our notation is not standard. A formal notation doesn't seem to exist in the literature; instead only informal English tends to be used. Some definitions in the literature may also require that R be a relation. The present definition, although somewhat cryptic, nicely avoids dummy variables. In er2 3201 we derive a more typical definition. We show that an equivalence relation is reflexive, symmetric, and transitive in erref 3212, ersymb 3210, and ertr 3211.
⊢ (Er R ↔ (◡R ∪ (R ∘ R)) ⊆ R)