mmtheorems32 - 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-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

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

Type	Label	Description
Statement
Theorem	difex2 3101	If the subtrahend of a class difference exists, then the minuend exists iff the difference exists.
|- (B e. C -> (A e. V <-> (A \ B) e. V))
Theorem	tpex 3102	A triple of classes exists.
|- {A, B, C} e. V
Theorem	opeluu 3103	Each member of an ordered pair belongs to the union of the union of a class to which the ordered pair belongs. Lemma 3D of [Enderton] p. 41.
|- (<.x, y>. e. A -> (x e. U.U.A /\ y e. U.U.A))
Theorem	uniuni 3104	Expression for double union that moves union into a class builder. (Contributed by FL, 28-May-2007.)
|- U.U.A = U.{x | E.y(x = U.y /\ y e. A)}
Theorem	euuni 3105	If ph is true for exactly one x, then U.{x | ph} is a way to express "the unique element such that ph is true." Some books use a special symbol such as iota to denote "the unique element such that."
|- (E!xph -> (ph <-> U.{x | ph} = x))
Theorem	reuuni1 3106	A way to express "the unique element such that" (restricted quantifier version).
|- ((x e. A /\ E!x e. A ph) -> (ph <-> U.{x e. A | ph} = x))
Theorem	reuuni2f 3107	U.{x e. A | ph} is an explicit representation of "the unique element in A such that ph." This theorem shows a condition that allows us to represent this element with a class expression B. The second hypothesis is a weakened bound variable condition that allows hbsbc1g 1993 to be used.
|- (y e. B -> A.x y e. B)   &   |- (B e. A -> (ps -> A.xps))   &   |- (x = B -> (ph <-> ps))   =>   |- ((B e. A /\ E!x e. A ph) -> (ps <-> U.{x e. A | ph} = B))
Theorem	reuuni2 3108	U.{x e. A | ph} is an explicit representation of "the unique element in A such that ph."
|- (x = B -> (ph <-> ps))   =>   |- ((B e. A /\ E!x e. A ph) -> (ps <-> U.{x e. A | ph} = B))
Theorem	reuuni3 3109	Derive the property ch of "the unique element in A such that ph" when expressed explicitly as U.{y e. A | ps}.
|- (x = y -> (ph <-> ps))   &   |- (x = U.{y e. A | ps} -> (ph <-> ch))   =>   |- (E!x e. A ph -> ch)
Theorem	reuuni4 3110	Derive the property of "the unique element in A such that ph" when expressed explicitly as U.{x e. A | ph}.
|- (E!x e. A ph -> [U.{x e. A | ph} / x]ph)
Theorem	reucl2 3111	Membership law for "the unique element in A such that ph."
|- (E!x e. A ph -> U.{x e. A | ph} e. {x e. A | ph})
Theorem	reuuniss 3112	Restriction of a unique element to a smaller class.
|- ((A (_ B /\ E.x e. A ph /\ E!x e. B ph) -> U.{x e. A | ph} = U.{x e. B | ph})
Theorem	mouniss 3113	Restriction of a unique element to a smaller class.
|- ((A (_ B /\ E.x e. A ph /\ E*x(x e. B /\ ph)) -> U.{x e. A | ph} = U.{x e. B | ph})
Theorem	reuuniss2 3114	Restriction of a unique element to a smaller class.
|- (((A (_ B /\ A.x e. A (ph -> ps)) /\ (E.x e. A ph /\ E!x e. B ps)) -> U.{x e. A | ph} = U.{x e. B | ps})
Theorem	reusn 3115	A way to express restricted existential uniqueness of a wff: its restricted class abstraction is a singleton.
|- (E!x e. A ph <-> E.y{x e. A | ph} = {y})
Theorem	reusni 3116	Restricted existential uniqueness determined by a singleton.
|- B e. V   =>   |- ({x e. A | ph} = {B} -> E!x e. A ph)
Theorem	rabsnt 3117	Truth implied by equality of a restricted class abstraction and a singleton.
|- B e. V   &   |- (x = B -> (ph <-> ps))   =>   |- ({x e. A | ph} = {B} -> ps)
Theorem	reuunisn 3118	A restricted class abstraction with a unique member can be expressed as a singleton.
|- (E!x e. A ph -> {x e. A | ph} = {U.{x e. A | ph}})
Theorem	alxfr 3119	Transfer universal quantification from a variable x to another variable y contained in expression A.
|- (x = A -> (ph <-> ps))   =>   |- ((A.y A e. B /\ A.xE.y x = A) -> (A.xph <-> A.yps))
Theorem	ralxfrd 3120	Transfer universal quantification from a variable x to another variable y contained in expression A.
|- ((ph /\ y e. B) -> A e. B)   &   |- ((ph /\ x e. B) -> E.y e. B x = A)   &   |- ((ph /\ x = A) -> (ps <-> ch))   =>   |- (ph -> (A.x e. B ps <-> A.y e. B ch))
Theorem	rexxfrd 3121	Transfer universal quantification from a variable x to another variable y contained in expression A. (Contributed by FL, 10-Apr-2007.)
|- ((ph /\ y e. B) -> A e. B)   &   |- ((ph /\ x e. B) -> E.y e. B x = A)   &   |- ((ph /\ x = A) -> (ps <-> ch))   =>   |- (ph -> (E.x e. B ps <-> E.y e. B ch))
Theorem	ralxfr 3122	Transfer universal quantification from a variable x to another variable y contained in expression A.
|- (y e. B -> A e. B)   &   |- (x e. B -> E.y e. B x = A)   &   |- (x = A -> (ph <-> ps))   =>   |- (A.x e. B ph <-> A.y e. B ps)
Theorem	ralxfrALT 3123	Transfer universal quantification from a variable x to another variable y contained in expression A.
|- (y e. B -> A e. B)   &   |- (x e. B -> E.y e. B x = A)   &   |- (x = A -> (ph <-> ps))   =>   |- (A.x e. B ph <-> A.y e. B ps)
Theorem	rexxfr 3124	Transfer existence from a variable x to another variable y contained in expression A.
|- (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	rabxfr 3125	Abstraction class membership after substituting an expression A (containing y) for x in the class expression ph.
|- (z e. B -> A.y z e. B)   &   |- (z e. C -> A.y z e. C)   &   |- (y e. D -> A e. D)   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> A = C)   =>   |- (B e. D -> (C e. {x e. D | ph} <-> B e. {y e. D | ps}))
Theorem	reuxfr2 3126	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 3127	Transfer existential uniqueness from a variable x to another variable y contained in expression A. Use reuhyp 3128 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 3128	A theorem useful for eliminating the restricted existential uniqueness hypotheses in reuxfr 3127.
|- (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 3129	Change the variable x in the expression for "the unique A such that ph" to another variable y contained in expression B. Use reuhyp 3128 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 3130	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 3131	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 3132	The union of the universe is the universe. Exercise 4.12(c) of [Mendelson] p. 235.
|- U.V = V
Theorem	eldifpw 3133	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 3134	Membership in the power class of a union.
|- C e. V   =>   |- (A e. P~(B u. C) <-> (A \ C) e. P~B)
Theorem	elpwunsn 3135	Membership in an extension of a power class.
|- (A e. (P~(B u. {C}) \ P~B) -> C e. A)
Theorem	op1stb 3136	Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (See op2ndb 3583 to extract the second member, op1sta 3579 for an alternate version, and op1st 4146 for the preferred version.)
|- A e. V   =>   |- |^||^|<.A, B>. = A
Theorem	iunpw 3137	An indexed union of a power class in terms of the power class of the union of its index. 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)
Theorem	fr3nr 3138	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	epne3 3139	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	dfwe2 3140	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)))
Ordinals (continued)
Theorem	ordon 3141	The class of all ordinal numbers is ordinal. Proposition 7.12 of [TakeutiZaring] p. 38, but without using the Axiom of Regularity.
|- Ord On
Theorem	epweon 3142	The epsilon relation well-orders the class of ordinal numbers. Proposition 4.8(g) of [Mendelson] p. 244.
|- E We On
Theorem	onprc 3143	No set contains all ordinal numbers. Proposition 7.13 of [TakeutiZaring] p. 38, but without using the Axiom of Regularity. This is also known as the Burali-Forti paradox (remark in [Enderton] p. 194). In 1897, Cesare Burali-Forti noticed that since the "set" of all ordinal numbers is an ordinal class (ordon 3141), it must be both an element of the set of all ordinal numbers yet greater than every such element. ZF set theory resolves this paradox by not allowing the class of all ordinal numbers to be a set (so instead it is a proper class). Here we prove the denial of its existence.
|- -. On e. V
Theorem	ordeleqon 3144	A way to express the ordinal property of a class in terms of the class of ordinal numbers. Corollary 7.14 of [TakeutiZaring] p. 38 and its converse.
|- (Ord A <-> (A e. On \/ A = On))
Theorem	ordsson 3145	Any ordinal class is a subclass of the class of ordinal numbers. Corollary 7.15 of [TakeutiZaring] p. 38.
|- (Ord A -> A (_ On)
Theorem	onss 3146	An ordinal number is a subset of the class of ordinal numbers.
|- (A e. On -> A (_ On)
Theorem	ssorduni 3147	The union of a class of ordinal numbers is ordinal. Proposition 7.19 of [TakeutiZaring] p. 40.
|- (A (_ On -> Ord U.A)
Theorem	ssonuni 3148	The union of a set of ordinal numbers is an ordinal number. Theorem 9 of [Suppes] p. 132.
|- (A e. B -> (A (_ On -> U.A e. On))
Theorem	ssonunii 3149	The union of a set of ordinal numbers is an ordinal number. Corollary 7N(d) of [Enderton] p. 193.
|- A e. V   =>   |- (A (_ On -> U.A e. On)
Theorem	onuni 3150	The union of an ordinal number is an ordinal number.
|- (A e. On -> U.A e. On)
Theorem	orduni 3151	The union of an ordinal class is ordinal.
|- (Ord A -> Ord U.A)
Theorem	onint 3152	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 3153	The intersection of a class of ordinal numbers is zero iff the class contains zero.
|- (A (_ On -> (|^|A = (/) <-> (/) e. A))
Theorem	onssmin 3154	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 3155	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 3156	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	oninton 3157	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 3158	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 3159	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 3160	No member of a set of ordinal numbers belongs to its minimum.
|- ((A (_ On /\ B e. A) -> -. B e. |^|A)
Theorem	onnminsb 3161	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	oneqmin 3162	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 3163	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 3164	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	sucon 3165	The class of all ordinal numbers is its own successor.
|- suc On = On
Theorem	sucexb 3166	A successor exists iff its class argument exists.
|- (A e. V <-> suc A e. V)
Theorem	sucexg 3167	The successor of a set is a set (generalization).
|- (A e. B -> suc A e. V)
Theorem	sucex 3168	The successor of a set is a set.
|- A e. V   =>   |- suc A e. V
Theorem	onmindif2 3169	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 3170	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	ordsuc 3171	The successor of an ordinal class is ordinal.
|- (Ord A <-> Ord suc A)
Theorem	ordpwsuc 3172	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 3173	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 3174	The successor of an ordinal number is an ordinal number.
|- (A e. On <-> suc A e. On)
Theorem	ordsucss 3175	The successor of an element of an ordinal class is a subset of it.
|- (Ord B -> (A e. B -> suc A (_ B))
Theorem	ordelsuc 3176	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 3177	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 3178	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 3179	The subclass relationship between two ordinal classes is inherited by their successors.
|- ((Ord A /\ Ord B) -> (A (_ B <-> suc A (_ suc B))
Theorem	ordsucun 3180	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	ordunel 3181	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 3182	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 3183	An ordinal class is a subclass of the successor of its union.
|- (Ord A -> A (_ suc U.A)
Theorem	orduniorsuc 3184	An ordinal class is either its union or the successor of its union.
|- (Ord A -> (A = U.A \/ A = suc U.A))
Theorem	unon 3185	The class of all ordinal numbers is its own union. Exercise 11 of [TakeutiZaring] p. 40.
|- U.On = On
Theorem	ordunisuc 3186	An ordinal class is equal to the union of its successor.
|- (Ord A -> U.suc A = A)
Theorem	orduniss2 3187	The union of the ordinal subsets of an ordinal number is that number.
|- (Ord A -> U.{x e. On | x (_ A} = A)
Theorem	onsucuni2 3188	A successor ordinal is the successor of its union.
|- ((A e. On /\ A = suc B) -> suc U.A = A)
Theorem	0elsuc 3189	The successor of an ordinal class contains the empty set.
|- (Ord A -> (/) e. suc A)
Theorem	limon 3190	The class of ordinal numbers is a limit ordinal.
|- Lim On
Theorem	onssi 3191	An ordinal number is a subset of On.
|- A e. On   =>   |- A (_ On
Theorem	onsuci 3192	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	onuniorsuci 3193	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	onuninsuci 3194	A limit ordinal is not a successor ordinal.
|- A e. On   =>   |- (A = U.A <-> -. E.x e. On A = suc x)
Theorem	onsucssi 3195	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 3196	A successor is not a limit ordinal.
|- (A e. B -> -. Lim suc A)
Theorem	orduninsuc 3197	An ordinal equal to its union is not a successor.
|- (Ord A -> (A = U.A <-> -. E.x e. On A = suc x))
Theorem	ordunisuc2 3198	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 3199	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 3200	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)))