Metamath Proof Explorer

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

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

Color key:

Metamath Proof Explorer (1-4957)

Hilbert Space Explorer (4958-5787)

**Statement List for Metamath Proof Explorer -** 3301-3400 - Page 34 of 58
Type	Label	Description
Statement

Theorem	f1oen 3301	The domain and range of a one-to-one, onto function are equinumerous.


Theorem	f1dom 3302	The domain of a one-to-one function is dominated by its range.


Theorem	en2d 3303	Equinumerosity inference from an implicit one-to-one onto function.
$/\$ $/\$

Theorem	en3d 3304	Equinumerosity inference from an implicit one-to-one onto function.
$/\$

Theorem	en2 3305	Equinumerosity inference from an implicit one-to-one onto function.
$/\$ $/\$

Theorem	en3 3306	Equinumerosity inference from an implicit one-to-one onto function.
$/\$

Theorem	dom2d 3307	A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its range.
$/\$

Theorem	dom2 3308	A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its range.
$/\$

Theorem	idssen 3309	Equality implies equinumerosity.


Theorem	dmen 3310	The domain of equinumerosity.


Theorem	ssdomg 3311	A set dominates its subsets. Theorem 16 of [Suppes] p. 94.


Theorem	ssdom2g 3312	A set dominates its subsets. Theorem 16 of [Suppes] p. 94.


Theorem	ener 3313	Equinumerosity is an equivalence relation.


Theorem	sdomirr 3314	Strict dominance is irreflexive. Theorem 21(i) of [Suppes] p. 97.


Theorem	sdomex 3315	Technical lemma for simplifying proofs involving strict dominance.
$/\$

Theorem	ensymg 3316	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92.


Theorem	ensym 3317	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92.


Theorem	ensymi 3318	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92.


Theorem	entrt 3319	Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92.
$/\$

Theorem	domtr 3320	Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94.
$/\$

Theorem	entr 3321	A chained equinumerosity inference.


Theorem	entr2 3322	A chained equinumerosity inference.


Theorem	entr3 3323	A chained equinumerosity inference.


Theorem	entr4 3324	A chained equinumerosity inference.


Theorem	endomtr 3325	Transitivity of equinumerosity and dominance.
$/\$

Theorem	domentr 3326	Transitivity of dominance and equinumerosity.
$/\$

Theorem	f1imaen 3327	A one-to-one function's image under a subset of its domain is equinumerous to the subset.
$/\$

Theorem	en0 3328	The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88.


Theorem	ensn1 3329	A singleton is equinumerous to ordinal one.


Theorem	ensn1g 3330	A singleton is equinumerous to ordinal one.


Theorem	en1 3331	A set is equinumerous to ordinal one iff it is a singleton.


Theorem	2dom 3332	A set that dominates ordinal 2 has at least 2 different members.


Theorem	fundmen 3333	A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98.


Theorem	mapsnen 3334	Set exponentiation to a singleton exponent is equinumerous to its base. Exercise 4.43 of [Mendelson] p. 255.


Theorem	map1 3335	Set exponentiation: ordinal 1 to any set is equinumerous to ordinal 1. Exercise 4.42(b) of [Mendelson] p. 255.


Theorem	en2sn 3336	Two singletons are equinumerous.
$/\$

Theorem	snfi 3337	A singleton is finite.


Theorem	unen 3338	Equinumerosity of union of disjoint sets. Theorem 4 of [Suppes] p. 92.
$/\$ $/\$ $/\$

Theorem	xpsnen 3339	A set is equinumerous to its cross-product with a singleton. Proposition 4.22(c) of [Mendelson] p. 254.


Theorem	xpsneng 3340	A set is equinumerous to its cross-product with a singleton. Proposition 4.22(c) of [Mendelson] p. 254.
$/\$

Theorem	endisj 3341	Any two sets are equinumerous to disjoint sets. Exercise 4.39 of [Mendelson] p. 255.
$/\$ $/\$

Theorem	undom 3342	Dominance law for union. Proposition 4.24(a) of [Mendelson] p. 257.
$/\$ $/\$

Theorem	xpcomen 3343	Commutative law for equinumerosity of cross product. Proposition 4.22(d) of [Mendelson] p. 254.


Theorem	xpassen 3344	Associative law for equinumerosity of cross product. Proposition 4.22(e) of [Mendelson] p. 254.


Theorem	xpdom2 3345	Dominance law for cross product. Proposition 10.33(2) of [TakeutiZaring] p. 92.


Theorem	xpdom1 3346	Dominance law for cross product. Theorem 6L(c) of [Enderton] p. 149.


Theorem	xpdom3 3347	A set is dominated by its cross product with a non-empty set. Exercise 6 of [Suppes] p. 98.


Theorem	pw2en 3348	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.)


Theorem	sbthlem1 3349	Lemma for Schroeder-Bernstein Theorem.
$/\$

Theorem	sbthlem2 3350	Lemma for Schroeder-Bernstein Theorem.
$/\$

Theorem	sbthlem3 3351	Lemma for Schroeder-Bernstein Theorem.
$/\$

Theorem	sbthlem4 3352	Lemma for Schroeder-Bernstein Theorem.
$/\$ $/\$ $/\$

Theorem	sbthlem5 3353	Lemma for Schroeder-Bernstein Theorem.
$/\$ $/\$

Theorem	sbthlem6 3354	Lemma for Schroeder-Bernstein Theorem.
$/\$ $/\$ $/\$ $/\$

Theorem	sbthlem7 3355	Lemma for Schroeder-Bernstein Theorem.
$/\$ $/\$ <