mmtheorems45 - 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-10658

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

Type	Label	Description
Statement
Theorem	ensymi 4401	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92.
|- B e. V   &   |- A ~~ B   =>   |- B ~~ A
Theorem	entrt 4402	Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92.
|- ((A ~~ B /\ B ~~ C) -> A ~~ C)
Theorem	domtr 4403	Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94.
|- ((A ~<_ B /\ B ~<_ C) -> A ~<_ C)
Theorem	entr 4404	A chained equinumerosity inference.
|- A ~~ B   &   |- B ~~ C   =>   |- A ~~ C
Theorem	entr2 4405	A chained equinumerosity inference.
|- C e. V   &   |- A ~~ B   &   |- B ~~ C   =>   |- C ~~ A
Theorem	entr3 4406	A chained equinumerosity inference.
|- B e. V   &   |- A ~~ B   &   |- A ~~ C   =>   |- B ~~ C
Theorem	entr4 4407	A chained equinumerosity inference.
|- B e. V   &   |- A ~~ B   &   |- C ~~ B   =>   |- A ~~ C
Theorem	endomtr 4408	Transitivity of equinumerosity and dominance.
|- ((A ~~ B /\ B ~<_ C) -> A ~<_ C)
Theorem	domentr 4409	Transitivity of dominance and equinumerosity.
|- ((A ~<_ B /\ B ~~ C) -> A ~<_ C)
Theorem	f1imaen 4410	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 (_ A) -> (F"C) ~~ C)
Theorem	en0 4411	The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88.
|- (A ~~ (/) <-> A = (/))
Theorem	ensn1 4412	A singleton is equinumerous to ordinal one.
|- A e. V   =>   |- {A} ~~ 1o
Theorem	ensn1g 4413	A singleton is equinumerous to ordinal one.
|- (A e. B -> {A} ~~ 1o)
Theorem	en1 4414	A set is equinumerous to ordinal one iff it is a singleton.
|- (A ~~ 1o <-> E.x A = {x})
Theorem	2dom 4415	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 4416	A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98.
|- F e. V   =>   |- (Fun F -> dom F ~~ F)
Theorem	mapsnen 4417	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 4418	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 4419	Two singletons are equinumerous.
|- ((A e. C /\ B e. D) -> {A} ~~ {B})
Theorem	snfi 4420	A singleton is finite.
|- E.x e. om {A} ~~ x
Theorem	unen 4421	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 4422	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 4423	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 4424	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 4425	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 4426	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 4427	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 4428	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))
Theorem	xpdom2 4429	Dominance law for cross product. Proposition 10.33(2) of [TakeutiZaring] p. 92.
|- B e. V   &   |- C e. V   =>   |- (A ~<_ B -> (C X. A) ~<_ (C X. B))
Theorem	xpdom1 4430	Dominance law for cross product. Theorem 6L(c) of [Enderton] p. 149.
|- B e. V   &   |- C e. V   =>   |- (A ~<_ B -> (A X. C) ~<_ (B X. C))
Theorem	xpdom1g 4431	Dominance law for cross product. Theorem 6L(c) of [Enderton] p. 149.
|- ((B e. R /\ C e. S /\ A ~<_ B) -> (A X. C) ~<_ (B X. C))
Theorem	xpdom3 4432	A set is dominated by its cross product with a non-empty set. Exercise 6 of [Suppes] p. 98.
|- A e. V   =>   |- (B =/= (/) -> A ~<_ (A X. B))
Theorem	pw2en 4433	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.)
|- A e. V   =>   |- P~A ~~ (2o ^m A)
Schroeder-Bernstein Theorem
Theorem	sbthlem1 4434	Lemma for sbth 4444.
Theorem	sbthlem2 4435	Lemma for sbth 4444.
Theorem	sbthlem3 4436	Lemma for sbth 4444.
Theorem	sbthlem4 4437	Lemma for sbth 4444.
Theorem	sbthlem5 4438	Lemma for sbth 4444.
Theorem	sbthlem6 4439	Lemma for sbth 4444.
Theorem	sbthlem7 4440	Lemma for sbth 4444.
Theorem	sbthlem8 4441	Lemma for sbth 4444.
Theorem	sbthlem9 4442	Lemma for sbth 4444.
Theorem	sbthlem10 4443	Lemma for sbth 4444.
Theorem	sbth 4444	Schroeder-Bernstein Theorem. Theorem 18 of [Suppes] p. 95. This theorem states that if set A is smaller (has lower cardinality) than B and vice-versa, then A and B 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 4434 through sbthlem10 4443; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlem10 4443. We follow closely the proof in Suppes, which you should consult to understand our proof at a higher level.
|- ((A ~<_ B /\ B ~<_ A) -> A ~~ B)
Theorem	sbthbg 4445	Schroeder-Bernstein Theorem and its converse.
|- (B e. C -> ((A ~<_ B /\ B ~<_ A) <-> A ~~ B))
Theorem	sbthcl 4446	Schroeder-Bernstein Theorem in class form.
|- ~~ = ( ~<_ i^i `' ~<_ )
Theorem	dfsdom2 4447	Alternate definition of strict dominance. Compare Definition 3 of [Suppes] p. 97.
|- ~< = ( ~<_ \ `' ~<_ )
Theorem	brsdom2 4448	Alternate definition of strict dominance. Definition 3 of [Suppes] p. 97.
|- A e. V   &   |- B e. V   =>   |- (A ~< B <-> (A ~<_ B /\ -. B ~<_ A))
Theorem	sdomnsym 4449	Strict dominance is not symmetric. Theorem 21(ii) of [Suppes] p. 97.
|- (A ~< B -> -. B ~< A)
Theorem	domnsym 4450	Theorem 22(i) of [Suppes] p. 97.
|- (A ~<_ B -> -. B ~< A)
Theorem	0dom 4451	Any set dominates the empty set.
|- (/) ~<_ A
Theorem	dom0 4452	A set dominated by the empty set is empty.
|- (A ~<_ (/) <-> A = (/))
Theorem	0sdomg 4453	A set strictly dominates the empty set iff it is not empty.
|- (A e. B -> ((/) ~< A <-> A =/= (/)))
Theorem	0sdom 4454	A set strictly dominates the empty set iff it is not empty.
|- A e. V   =>   |- ((/) ~< A <-> A =/= (/))
Theorem	sdom0 4455	The empty set does not strictly dominate any set.
|- -. A ~< (/)
Theorem	sdomdomtr 4456	Transitivity of strict dominance and dominance. Theorem 22(iii) of [Suppes] p. 97.
|- (C e. D -> ((A ~< B /\ B ~<_ C) -> A ~< C))
Theorem	sdomentr 4457	Transitivity of strict dominance and equinumerosity. Exercise 11 of [Suppes] p. 98.
|- (C e. D -> ((A ~< B /\ B ~~ C) -> A ~< C))
Theorem	ensdomtr 4458	Transitivity of equinumerosity and strict dominance.
|- ((A ~~ B /\ B ~< C) -> A ~< C)
Theorem	sdomirr 4459	Strict dominance is irreflexive. Theorem 21(i) of [Suppes] p. 97.
|- -. A ~< A
Theorem	sdomex 4460	Technical lemma for simplifying proofs involving strict dominance.
|- (A ~< B -> (A e. V /\ B e. V))
Theorem	sdomtr 4461	Strict dominance is transitive. Theorem 21(iii) of [Suppes] p. 97.
|- ((A ~< B /\ B ~< C) -> A ~< C)
Theorem	sdomn2lp 4462	Strict dominance has no 2-cycle loops.
|- -. (A ~< B /\ B ~< A)
Theorem	domsdomtr 4463	Transitivity of dominance and strict dominance. Theorem 22(ii) of [Suppes] p. 97.
|- ((A ~<_ B /\ B ~< C) -> A ~< C)
Theorem	enen1 4464	Equality-like theorem for equinumerosity.
|- ((B e. D /\ A ~~ B) -> (A ~~ C <-> B ~~ C))
Theorem	enen2 4465	Equality-like theorem for equinumerosity.
|- ((B e. D /\ A ~~ B) -> (C ~~ A <-> C ~~ B))
Theorem	domen1 4466	Equality-like theorem for equinumerosity and dominance.
|- ((B e. D /\ A ~~ B) -> (A ~<_ C <-> B ~<_ C))
Theorem	domen2 4467	Equality-like theorem for equinumerosity and dominance.
|- ((B e. D /\ A ~~ B) -> (C ~<_ A <-> C ~<_ B))
Theorem	sdomen1 4468	Equality-like theorem for equinumerosity and strict dominance.
|- ((B e. D /\ A ~~ B) -> (A ~< C <-> B ~< C))
Theorem	sdomen2 4469	Equality-like theorem for equinumerosity and strict dominance.
|- ((B e. D /\ A ~~ B) -> (C ~< A <-> C ~< B))
Theorem	fodomr 4470	There exists a mapping from a set onto any (non-empty) set that it dominates.
|- ((A e. C /\ (/) ~< B /\ B ~<_ A) -> E.f f:A-onto->B)
Theorem	canth2 4471	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 3899.
|- A e. V   =>   |- A ~< P~A
Theorem	canth2g 4472	Cantor's theorem with the sethood requirement expressed as an antecedent. Theorem 23 of [Suppes] p. 97.
|- (A e. B -> A ~< P~A)
Theorem	pwuninel 4473	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.
|- -. P~U.A e. A
Theorem	2pwuninel 4474	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.
|- -. P~P~U.A e. A
Theorem	xpen 4475	Equinumerosity law for cross product. Proposition 4.22(b) of [Mendelson] p. 254.
|- A e. V   &   |- B e. V   &   |- C e. V   &   |- D e. V   =>   |- ((A ~~ B /\ C ~~ D) -> (A X. C) ~~ (B X. D))
Theorem	mapenlem1 4476	Lemma for mapen 4478.
Theorem	mapenlem2 4477	Lemma for mapen 4478.
Theorem	mapen 4478	Two set exponentiations are equinumerous when their bases and exponents are equinumerous. Theorem 6H(c) of [Enderton] p. 139.
|- A e. V   &   |- B e. V   &   |- C e. V   &   |- D e. V   =>   |- ((A ~~ B /\ C ~~ D) -> (A ^m C) ~~ (B ^m D))
Theorem	mapdom1 4479	Order-preserving property of set exponentiation. Theorem 6L(c) of [Enderton] p. 149.
|- A e. V   &   |- B e. V   &   |- C e. V   =>   |- (A ~<_ B -> (A ^m C) ~<_ (B ^m C))
Theorem	mapdom2lem 4480	Lemma for mapdom2 4481.
Theorem	mapdom2 4481	Order-preserving property of set exponentiation. Theorem 6L(d) of [Enderton] p. 149.
|- A e. V   &   |- B e. V   &   |- C e. V   =>   |- ((A ~<_ B /\ -. (A = (/) /\ C = (/))) -> (C ^m A) ~<_ (C ^m B))
Theorem	mapxpen 4482	Equinumerosity law for double set exponentiation. Proposition 10.45 of [TakeutiZaring] p. 96.
|-