mmtheorems55 - 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-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17411

Statement List for Metamath Proof Explorer - 5401-5500 - Page 55 of 175

Type	Label	Description
Statement
Theorem	map0e 5401	Set exponentiation with an empty exponent (ordinal number 0) is ordinal number 1. Exercise 4.42(a) of [Mendelson] p. 255.
|- A e. _V   =>   |- (A ^m (/)) = 1o
Theorem	map0b 5402	Set exponentiation with an empty base is the empty set, provided the exponent is non-empty. Theorem 96 of [Suppes] p. 89.
|- A e. _V   =>   |- (A =/= (/) -> ((/) ^m A) = (/))
Theorem	map0 5403	Set exponentiation is empty iff the base is empty and the exponent is not empty. Theorem 97 of [Suppes] p. 89.
|- A e. _V   &   |- B e. _V   =>   |- ((A ^m B) = (/) <-> (A = (/) /\ B =/= (/)))
Theorem	mapsn 5404	The value of set exponentiation with a singleton exponent. Theorem 98 of [Suppes] p. 89.
|- A e. _V   &   |- B e. _V   =>   |- (A ^m {B}) = {f | E.y e. A f = {<.B, y>.}}
Theorem	mapss 5405	Subset inheritance for set exponentiation. Theorem 99 of [Suppes] p. 89.
|- B e. _V   &   |- C e. _V   =>   |- (A C_ B -> (A ^m C) C_ (B ^m C))
Infinite Cartesian products
Syntax	cixp 5406	Extend class notation to include infinite Cartesian products.
class X_x e. A B
Definition	df-ixp 5407	Definition of infinite Cartesian product of [Enderton] p. 54. Enderton uses a bold "X" with x e. A written underneath or as a subscript, as does Stoll p. 47. Some books use a capital pi, but we will reserve that notation for products of numbers. Usually B represents a class expression containing x free and thus can be thought of as B(x). Normally, x is not free in A, although this is not a requirement of the definition.
|- X_x e. A B = {f | (f Fn A /\ A.x e. A (f` x) e. B)}
Theorem	elixp2 5408	Membership in an infinite Cartesian product. See df-ixp 5407 for discussion of the notation.
|- (F e. X_x e. A B <-> (F e. _V /\ F Fn A /\ A.x e. A (F` x) e. B))
Theorem	elixp 5409	Membership in an infinite Cartesian product.
|- F e. _V   =>   |- (F e. X_x e. A B <-> (F Fn A /\ A.x e. A (F` x) e. B))
Theorem	elixpconst 5410	Membership in an infinite Cartesian product of a constant B.
|- F e. _V   =>   |- (F e. X_x e. A B <-> F:A-->B)
Theorem	ixpconst 5411	Infinite Cartesian product of a constant B.
|- A e. _V   &   |- B e. _V   =>   |- X_x e. A B = (B ^m A)
Theorem	ixpeq1 5412	Equality theorem for infinite Cartesian product.
|- (A = B -> X_x e. A C = X_x e. B C)
Theorem	ss2ixp 5413	Subclass theorem for infinite Cartesian product.
|- (A.x e. A B C_ C -> X_x e. A B C_ X_x e. A C)
Theorem	ixpeq2 5414	Equality theorem for infinite Cartesian product.
|- (A.x e. A B = C -> X_x e. A B = X_x e. A C)
Theorem	ixpf 5415	A member of an infinite Cartesian product maps to the indexed union of the product argument. Remark in [Enderton] p. 54.
|- (F e. X_x e. A B -> F:A-->U_x e. A B)
Theorem	uniixp 5416	The union of an infinite Cartesian product is included in a cross product.
|- U.X_x e. A B C_ (A X. U_x e. A B)
Theorem	ixpexg 5417	The existence of an infinite Cartesian product. x is normally a free-variable parameter in B. Remark in Enderton p. 54.
|- ((A e. C /\ A.x e. A B e. D) -> X_x e. A B e. _V)
Theorem	ixp0x 5418	An infinite Cartesian product with an empty index set.
|- X_x e. (/) A = {(/)}
Theorem	0elixp 5419	Membership of the empty set in an infinite Cartesian product. (Contributed by Steve Rodriguez, 29-Sep-2006.)
|- (/) e. X_x e. (/) A
Theorem	ixp0 5420	The infinite Cartesian product of a family B(x) with an empty member is empty.
|- (E.x e. A B = (/) -> X_x e. A B = (/))
Theorem	mapixp 5421	Express set exponentiation in terms of an infinite Cartesian product. Remark in [Stoll] p. 47. Note that B is constant, i.e. x does not occur in B.
|- A e. _V   &   |- B e. _V   =>   |- (B ^m A) = X_x e. A B
Theorem	ixpssmap 5422	An infinite Cartesian product is a subset of set exponentation. Remark in [Enderton] p. 54.
|- A e. _V   &   |- B e. _V   =>   |- X_x e. A B C_ (U_x e. A B ^m A)
Equinumerosity
Syntax	cen 5423	Extend class definition to include the equinumerosity relation ("approximately equals" symbol)
class ~~
Syntax	cdom 5424	Extend class definition to include the dominance relation (curly less-than-or-equal)
class ~<_
Syntax	csdm 5425	Extend class definition to include the strict dominance relation (curly less-than)
class ~<
Syntax	cfn 5426	Extend class definition to include the class of all finite sets.
class Fin
Definition	df-en 5427	Define the equinumerosity relation. Definition of [Enderton] p. 129. We define ~~ to be a binary relation rather than a connective, so its arguments must be sets to be meaningful. This is acceptable because we do not consider equinumerosity for proper classes. We derive the usual definition as bren 5436.
|- ~~ = {<.x, y>. | E.f f:x-1-1-onto->y}
Definition	df-dom 5428	Define the dominance relation. For an alternate definition see dfdom2 5443. Compare Definition of [Enderton] p. 145. Typical textbook definitions are derived as brdom 5437 and domen 5438.
|- ~<_ = {<.x, y>. | E.f f:x-1-1->y}
Definition	df-sdom 5429	Define the strict dominance relation. Alternate possible definitions are derived as brsdom 5440 and brsdom2 5524. Definition 3 of [Suppes] p. 97.
|- ~< = ( ~<_ \ ~~ )
Definition	df-fin 5430	Define the (proper) class of all finite sets. Similar to Definition 10.29 of [TakeutiZaring] p. 91, whose "Fin(a)" corresponds to our "a e. Fin". This definition is meaningful whether or not we accept the Axiom of Infinity ax-inf2 5731. If we accept Infinity, we can also express A e. Fin by A ~< om (theorem isfinite 5741.)
|- Fin = {x | E.y e. om x ~~ y}
Theorem	relen 5431	Equinumerosity is a relation.
|- Rel ~~
Theorem	reldom 5432	Dominance is a relation.
|- Rel ~<_
Theorem	relsdom 5433	Strict dominance is a relation.
|- Rel ~<
Theorem	breng 5434	Equinumerosity relation.
|- (B e. C -> (A ~~ B <-> E.f f:A-1-1-onto->B))
Theorem	brdomg 5435	Dominance relation.
|- (B e. C -> (A ~<_ B <-> E.f f:A-1-1->B))
Theorem	bren 5436	Equinumerosity relation. Compare Definition of [Enderton] p. 129.
|- B e. _V   =>   |- (A ~~ B <-> E.f f:A-1-1-onto->B)
Theorem	brdom 5437	Dominance relation.
|- B e. _V   =>   |- (A ~<_ B <-> E.f f:A-1-1->B)
Theorem	domen 5438	Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146.
|- B e. _V   =>   |- (A ~<_ B <-> E.x(A ~~ x /\ x C_ B))
Theorem	domeng 5439	Dominance in terms of equinumerosity, with the sethood requirement expressed as an antecedent. Example 1 of [Enderton] p. 146.
|- (B e. C -> (A ~<_ B <-> E.x(A ~~ x /\ x C_ B)))
Theorem	brsdom 5440	Strict dominance relation, meaning "B is strictly greater in size than A." Definition of [Mendelson] p. 255.
|- (A ~< B <-> (A ~<_ B /\ -. A ~~ B))
Theorem	isfi 5441	Express "A is finite." Definition 10.29 of [TakeutiZaring] p. 91 (whose "Fin " is a predicate instead of a class).
|- (A e. Fin <-> E.x e. om A ~~ x)
Theorem	enssdom 5442	Equinumerosity implies dominance.
|- ~~ C_ ~<_
Theorem	dfdom2 5443	Alternate definition of dominance.
|- ~<_ = ( ~< u. ~~ )
Theorem	endom 5444	Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94.
|- (A ~~ B -> A ~<_ B)
Theorem	sdomdom 5445	Strict dominance implies dominance.
|- (A ~< B -> A ~<_ B)
Theorem	sdomnen 5446	Strict dominance implies non-equinumerosity.
|- (A ~< B -> -. A ~~ B)
Theorem	brdom2 5447	Dominance in terms of strict dominance and equinumerosity. Theorem 22(iv) of [Suppes] p. 97.
|- (A ~<_ B <-> (A ~< B \/ A ~~ B))
Theorem	bren2 5448	Equinumerosity expressed in terms of dominance and strict dominance.
|- (A ~~ B <-> (A ~<_ B /\ -. A ~< B))
Theorem	enrefg 5449	Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92.
|- (A e. B -> A ~~ A)
Theorem	enref 5450	Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92.
|- A e. _V   =>   |- A ~~ A
Theorem	eqeng 5451	Equality implies equinumerosity.
|- (A e. C -> (A = B -> A ~~ B))
Theorem	domrefg 5452	Dominance is reflexive.
|- (A e. B -> A ~<_ A)
Theorem	f1oen2g 5453	The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 5454 does not require the Axiom of Replacement.
|- ((F e. C /\ F:A-1-1-onto->B) -> A ~~ B)
Theorem	f1oeng 5454	The domain and range of a one-to-one, onto function are equinumerous.
|- ((A e. C /\ F:A-1-1-onto->B) -> A ~~ B)
Theorem	f1domg 5455	The domain of a one-to-one function is dominated by its codomain.
|- (A e. C -> (F:A-1-1->B -> A ~<_ B))
Theorem	f1dom2g 5456	The domain of a one-to-one function is dominated by its codomain.
|- (B e. C -> (F:A-1-1->B -> A ~<_ B))
Theorem	f1oen 5457	The domain and range of a one-to-one, onto function are equinumerous.
|- A e. _V   =>   |- (F:A-1-1-onto->B -> A ~~ B)
Theorem	f1dom 5458	The domain of a one-to-one function is dominated by its codomain.
|- A e. _V   =>   |- (F:A-1-1->B -> A ~<_ B)
Theorem	en2d 5459	Equinumerosity inference from an implicit one-to-one onto function.
|- (ph -> A e. _V)   &   |- (ph -> (x e. A -> C e. _V))   &   |- (ph -> (y e. B -> D e. _V))   &   |- (ph -> ((x e. A /\ y = C) <-> (y e. B /\ x = D)))   =>   |- (ph -> A ~~ B)
Theorem	en3d 5460	Equinumerosity inference from an implicit one-to-one onto function.
|- (ph -> A e. _V)   &   |- (ph -> (x e. A -> C e. B))   &   |- (ph -> (y e. B -> D e. A))   &   |- (ph -> ((x e. A /\ y e. B) -> (x = D <-> y = C)))   =>   |- (ph -> A ~~ B)
Theorem	en2 5461	Equinumerosity inference from an implicit one-to-one onto function.
|- A e. _V   &   |- (x e. A -> C e. _V)   &   |- (y e. B -> D e. _V)   &   |- ((x e. A /\ y = C) <-> (y e. B /\ x = D))   =>   |- A ~~ B
Theorem	en3 5462	Equinumerosity inference from an implicit one-to-one onto function.
|- A e. _V   &   |- (x e. A -> C e. B)   &   |- (y e. B -> D e. A)   &   |- ((x e. A /\ y e. B) -> (x = D <-> y = C))   =>   |- A ~~ B
Theorem	dom2d 5463	A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain.
|- (ph -> (x e. A -> C e. B))   &   |- (ph -> ((x e. A /\ y e. A) -> (C = D <-> x = y)))   =>   |- (ph -> (A e. R -> A ~<_ B))
Theorem	dom2 5464	A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. C and D can be read C(x) and D(y), as can be shown from their distinct variable conditions.
|- (x e. A -> C e. B)   &   |- ((x e. A /\ y e. A) -> (C = D <-> x = y))   =>   |- (A e. R -> A ~<_ B)
Theorem	idssen 5465	Equality implies equinumerosity.
|- _I C_ ~~
Theorem	dmen 5466	The domain of equinumerosity.
|- dom ~~ = _V
Theorem	ssdomg 5467	A set dominates its subsets. Theorem 16 of [Suppes] p. 94.
|- (A e. C -> (A C_ B -> A ~<_ B))
Theorem	ssdom2g 5468	A set dominates its subsets. Theorem 16 of [Suppes] p. 94.
|- (B e. C -> (A C_ B -> A ~<_ B))
Theorem	ener 5469	Equinumerosity is an equivalence relation.
|- Er ~~
Theorem	ensymg 5470	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92.
|- (B e. C -> (A ~~ B -> B ~~ A))
Theorem	ensym 5471	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92.
|- B e. _V   =>   |- (A ~~ B -> B ~~ A)
Theorem	ensymi 5472	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92.
|- B e. _V   &   |- A ~~ B   =>   |- B ~~ A
Theorem	entr 5473	Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92.
|- ((A ~~ B /\ B ~~ C) -> A ~~ C)
Theorem	domtr 5474	Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94.
|- ((A ~<_ B /\ B ~<_ C) -> A ~<_ C)
Theorem	entri 5475	A chained equinumerosity inference.
|- A ~~ B   &   |- B ~~ C   =>   |- A ~~ C
Theorem	entr2i 5476	A chained equinumerosity inference.
|- C e. _V   &   |- A ~~ B   &   |- B ~~ C   =>   |- C ~~ A
Theorem	entr3i 5477	A chained equinumerosity inference.
|- B e. _V   &   |- A ~~ B   &   |- A ~~ C   =>   |- B ~~ C
Theorem	entr4i 5478	A chained equinumerosity inference.
|- B e. _V   &   |- A ~~ B   &   |- C ~~ B   =>   |- A ~~ C
Theorem	endomtr 5479	Transitivity of equinumerosity and dominance.
|- ((A ~~ B /\ B ~<_ C) -> A ~<_ C)
Theorem	domentr 5480	Transitivity of dominance and equinumerosity.
|- ((A ~<_ B /\ B ~~ C) -> A ~<_ C)
Theorem	f1imaen 5481	A one-to-one function's image under a subset of its domain is equinumerous to the subset.
|- C e. _V   =>   |- ((F:A-1-1->B /\ C C_ A) -> (F"C) ~~ C)
Theorem	en0 5482	The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88.
|- (A ~~ (/) <-> A = (/))
Theorem	ensn1 5483	A singleton is equinumerous to ordinal one.
|- A e. _V   =>   |- {A} ~~ 1o
Theorem	ensn1g 5484	A singleton is equinumerous to ordinal one.
|- (A e. B -> {A} ~~ 1o)
Theorem	en1 5485	A set is equinumerous to ordinal one iff it is a singleton.
|- (A ~~ 1o <-> E.x A = {x})
Theorem	2dom 5486	A set that dominates ordinal 2 has at least 2 different members.
|- A e. _V   =>   |- (2o ~<_ A -> E.x e. A E.y e. A -. x = y)
Theorem	fundmen 5487	A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98.
|- F e. _V   =>   |- (Fun F -> dom F ~~ F)
Theorem	mapsnen 5488	Set exponentiation to a singleton exponent is equinumerous to its base. Exercise 4.43 of [Mendelson] p. 255.
|- A e. _V   &   |- B e. _V   =>   |- (A ^m {B}) ~~ A
Theorem	map1 5489	Set exponentiation: ordinal 1 to any set is equinumerous to ordinal 1. Exercise 4.42(b) of [Mendelson] p. 255.
|- A e. _V   =>   |- (1o ^m A) ~~ 1o
Theorem	en2sn 5490	Two singletons are equinumerous.
|- ((A e. C /\ B e. D) -> {A} ~~ {B})
Theorem	snfi 5491	A singleton is finite.
|- {A} e. Fin
Theorem	fiprc 5492	The class of finite sets is a proper class. (Contributed by Jeffrey Hankins, 10-Oct-2008.)
|- Fin e/ _V
Theorem	unen 5493	Equinumerosity of union of disjoint sets. Theorem 4 of [Suppes] p. 92.
|- (((A ~~ B /\ C ~~ D) /\ ((A i^i C) = (/) /\ (B i^i D) = (/))) -> (A u. C) ~~ (B u. D))
Theorem	xpsnen 5494	A set is equinumerous to its cross-product with a singleton. Proposition 4.22(c) of [Mendelson] p. 254.
|- A e. _V   &   |- B e. _V   =>   |- (A X. {B}) ~~ A
Theorem	xpsneng 5495	A set is equinumerous to its cross-product with a singleton. Proposition 4.22(c) of [Mendelson] p. 254.
|- ((A e. C /\ B e. D) -> (A X. {B}) ~~ A)
Theorem	endisj 5496	Any two sets are equinumerous to disjoint sets. Exercise 4.39 of [Mendelson] p. 255.
|- A e. _V   &   |- B e. _V   =>   |- E.xE.y((x ~~ A /\ y ~~ B) /\ (x i^i y) = (/))
Theorem	undom 5497	Dominance law for union. Proposition 4.24(a) of [Mendelson] p. 257.
|- B e. _V   &   |- C e. _V   &   |- D e. _V   =>   |- (((A ~<_ B /\ C ~<_ D) /\ (B i^i D) = (/)) -> (A u. C) ~<_ (B u. D))
Theorem	xpcomen 5498	Commutative law for equinumerosity of cross product. Proposition 4.22(d) of [Mendelson] p. 254.
|- A e. _V   &   |- B e. _V   =>   |- (A X. B) ~~ (B X. A)
Theorem	xpcomeng 5499	Commutative law for equinumerosity of cross product. Proposition 4.22(d) of [Mendelson] p. 254.
|- ((A e. C /\ B e. D) -> (A X. B) ~~ (B X. A))
Theorem	xpassen 5500	Associative law for equinumerosity of cross product. Proposition 4.22(e) of [Mendelson] p. 254.
|- A e. _V   &   |- B e. _V   &   |- C e. _V   =>   |- ((A X. B) X. C) ~~ (A X. (B X. C))