Home	Metamath Proof Explorer	< Previous   Next >
		Browser slow? Try the Unicode version.

---

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

Color key:

Metamath Proof Explorer (1-8757)

Hilbert Space Explorer (8758-10682)

Statement List for Metamath Proof Explorer - 4401-4500 - Page 45 of 107

Type	Label	Description
Statement
Theorem	dom2 4401	A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its range. and can be read and , as can be shown from their distinct variable conditions.
Theorem	idssen 4402	Equality implies equinumerosity.
Theorem	dmen 4403	The domain of equinumerosity.
Theorem	ssdomg 4404	A set dominates its subsets. Theorem 16 of [Suppes] p. 94.
Theorem	ssdom2g 4405	A set dominates its subsets. Theorem 16 of [Suppes] p. 94.
Theorem	ener 4406	Equinumerosity is an equivalence relation.
Theorem	ensymg 4407	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92.
Theorem	ensym 4408	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92.
Theorem	ensymi 4409	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92.
Theorem	entrt 4410	Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92.
Theorem	domtr 4411	Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94.
Theorem	entr 4412	A chained equinumerosity inference.
Theorem	entr2 4413	A chained equinumerosity inference.
Theorem	entr3 4414	A chained equinumerosity inference.
Theorem	entr4 4415	A chained equinumerosity inference.
Theorem	endomtr 4416	Transitivity of equinumerosity and dominance.
Theorem	domentr 4417	Transitivity of dominance and equinumerosity.
Theorem	f1imaen 4418	A one-to-one function's image under a subset of its domain is equinumerous to the subset.
Theorem	en0 4419	The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88.
Theorem	ensn1 4420	A singleton is equinumerous to ordinal one.
Theorem	ensn1g 4421	A singleton is equinumerous to ordinal one.
Theorem	en1 4422	A set is equinumerous to ordinal one iff it is a singleton.
Theorem	2dom 4423	A set that dominates ordinal 2 has at least 2 different members.
Theorem	fundmen 4424	A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98.
Theorem	mapsnen 4425	Set exponentiation to a singleton exponent is equinumerous to its base. Exercise 4.43 of [Mendelson] p. 255.
Theorem	map1 4426	Set exponentiation: ordinal 1 to any set is equinumerous to ordinal 1. Exercise 4.42(b) of [Mendelson] p. 255.
Theorem	en2sn 4427	Two singletons are equinumerous.
Theorem	snfi 4428	A singleton is finite.
Theorem	unen 4429	Equinumerosity of union of disjoint sets. Theorem 4 of [Suppes] p. 92.
Theorem	xpsnen 4430	A set is equinumerous to its cross-product with a singleton. Proposition 4.22(c) of [Mendelson] p. 254.
Theorem	xpsneng 4431	A set is equinumerous to its cross-product with a singleton. Proposition 4.22(c) of [Mendelson] p. 254.
Theorem	endisj 4432	Any two sets are equinumerous to disjoint sets. Exercise 4.39 of [Mendelson] p. 255.
Theorem	undom 4433	Dominance law for union. Proposition 4.24(a) of [Mendelson] p. 257.
Theorem	xpcomen 4434	Commutative law for equinumerosity of cross product. Proposition 4.22(d) of [Mendelson] p. 254.
Theorem	xpcomeng 4435	Commutative law for equinumerosity of cross product. Proposition 4.22(d) of [Mendelson] p. 254.
Theorem	xpassen 4436	Associative law for equinumerosity of cross product. Proposition 4.22(e) of [Mendelson] p. 254.
Theorem	xpdom2 4437	Dominance law for cross product. Proposition 10.33(2) of [TakeutiZaring] p. 92.
Theorem	xpdom1 4438	Dominance law for cross product. Theorem 6L(c) of [Enderton] p. 149.
Theorem	xpdom1g 4439	Dominance law for cross product. Theorem 6L(c) of [Enderton] p. 149.
Theorem	xpdom3 4440	A set is dominated by its cross product with a non-empty set. Exercise 6 of [Suppes] p. 98.
Theorem	pw2en 4441	The power set of a set is equinumerous to set exponentiation with a base of ordinal 2. Proposition 10.44 of [TakeutiZaring] p. 96. (This proof seems excessively long. An attempt to find a shorter one is on my to-do list.)
Schroeder-Bernstein Theorem
Theorem	sbthlem1 4442	Lemma for sbth 4452.
Theorem	sbthlem2 4443	Lemma for sbth 4452.
Theorem	sbthlem3 4444	Lemma for sbth 4452.
Theorem	sbthlem4 4445	Lemma for sbth 4452.
Theorem	sbthlem5 4446	Lemma for sbth 4452.
Theorem	sbthlem6 4447	Lemma for sbth 4452.
Theorem	sbthlem7 4448	Lemma for sbth 4452.
Theorem	sbthlem8 4449	Lemma for sbth 4452.
Theorem	sbthlem9 4450	Lemma for sbth 4452.
Theorem	sbthlem10 4451	Lemma for sbth 4452.
Theorem	sbth 4452	Schroeder-Bernstein Theorem. Theorem 18 of [Suppes] p. 95. This theorem states that if set is smaller (has lower cardinality) than and vice-versa, then and are equinumerous (have the same cardinality). The interesting thing is that this can be proved without invoking the Axiom of Choice, as we do here, but the proof as you can see is quite difficult. (The theorem can be proved more easily if we allow AC.) The main proof consists of lemmas sbthlem1 4442 through sbthlem10 4451; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlem10 4451. We follow closely the proof in Suppes, which you should consult to understand our proof at a higher level.
Theorem	sbthbg 4453	Schroeder-Bernstein Theorem and its converse.
Theorem	sbthcl 4454	Schroeder-Bernstein Theorem in class form.
Theorem	dfsdom2 4455	Alternate definition of strict dominance. Compare Definition 3 of [Suppes] p. 97.
Theorem	brsdom2 4456	Alternate definition of strict dominance. Definition 3 of [Suppes] p. 97.
Theorem	sdomnsym 4457	Strict dominance is not symmetric. Theorem 21(ii) of [Suppes] p. 97.
Theorem	domnsym 4458	Theorem 22(i) of [Suppes] p. 97.
Theorem	0dom 4459	Any set dominates the empty set.
Theorem	dom0 4460	A set dominated by the empty set is empty.
Theorem	0sdomg 4461	A set strictly dominates the empty set iff it is not empty.
Theorem	0sdom 4462	A set strictly dominates the empty set iff it is not empty.
Theorem	sdom0 4463	The empty set does not strictly dominate any set.
Theorem	sdomdomtr 4464	Transitivity of strict dominance and dominance. Theorem 22(iii) of [Suppes] p. 97.
Theorem	sdomentr 4465	Transitivity of strict dominance and equinumerosity. Exercise 11 of [Suppes] p. 98.
Theorem	ensdomtr 4466	Transitivity of equinumerosity and strict dominance.
Theorem	sdomirr 4467	Strict dominance is irreflexive. Theorem 21(i) of [Suppes] p. 97.
Theorem	sdomex 4468	Technical lemma for simplifying proofs involving strict dominance.
Theorem	sdomtr 4469	Strict dominance is transitive. Theorem 21(iii) of [Suppes] p. 97.
Theorem	sdomn2lp 4470	Strict dominance has no 2-cycle loops.
Theorem	domsdomtr 4471	Transitivity of dominance and strict dominance. Theorem 22(ii) of [Suppes] p. 97.
Theorem	enen1 4472	Equality-like theorem for equinumerosity.
Theorem	enen2 4473	Equality-like theorem for equinumerosity.
Theorem	domen1 4474	Equality-like theorem for equinumerosity and dominance.
Theorem	domen2 4475	Equality-like theorem for equinumerosity and dominance.
Theorem	sdomen1 4476	Equality-like theorem for equinumerosity and strict dominance.
Theorem	sdomen2 4477	Equality-like theorem for equinumerosity and strict dominance.
Theorem	fodomr 4478	There exists a mapping from a set onto any (non-empty) set that it dominates.
Theorem	canth2 4479	Cantor's Theorem. No set is equinumerous to its power set. Specifically, any set has a cardinality (size) strictly less than the cardinality of its power set. For example, the cardinality of real numbers is the same as the cardinality of the power set of integers, so real numbers cannot be put into a one-to-one correspondence with integers. Theorem 23 of [Suppes] p. 97. For the function version, see canth 3907.
Theorem	2pwuninel 4480	The power set of the power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set.
Theorem	canth2g 4481	Cantor's theorem with the sethood requirement expressed as an antecedent. Theorem 23 of [Suppes] p. 97.
Theorem	pwuninel 4482	The power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set.
Theorem	pwuninelgOLD 4483	The power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set.
Theorem	xpen 4484	Equinumerosity law for cross product. Proposition 4.22(b) of [Mendelson] p. 254.