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-10700 108 10701-10781

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

Type	Label	Description
Statement
Theorem	en3d 4401	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 4402	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 4403	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 4404	A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its range.
|- (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 4405	A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its range. 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 4406	Equality implies equinumerosity.
|- I (_ ~~
Theorem	dmen 4407	The domain of equinumerosity.
|- dom ~~ = V
Theorem	ssdomg 4408	A set dominates its subsets. Theorem 16 of [Suppes] p. 94.
|- (A e. C -> (A (_ B -> A ~<_ B))
Theorem	ssdom2g 4409	A set dominates its subsets. Theorem 16 of [Suppes] p. 94.
|- (B e. C -> (A (_ B -> A ~<_ B))
Theorem	ener 4410	Equinumerosity is an equivalence relation.
|- Er ~~
Theorem	ensymg 4411	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92.
|- (B e. C -> (A ~~ B -> B ~~ A))
Theorem	ensym 4412	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92.
|- B e. V   =>   |- (A ~~ B -> B ~~ A)
Theorem	ensymi 4413	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92.
|- B e. V   &   |- A ~~ B   =>   |- B ~~ A
Theorem	entrt 4414	Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92.
|- ((A ~~ B /\ B ~~ C) -> A ~~ C)
Theorem	domtr 4415	Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94.
|- ((A ~<_ B /\ B ~<_ C) -> A ~<_ C)
Theorem	entr 4416	A chained equinumerosity inference.
|- A ~~ B   &   |- B ~~ C   =>   |- A ~~ C
Theorem	entr2 4417	A chained equinumerosity inference.
|- C e. V   &   |- A ~~ B   &   |- B ~~ C   =>   |- C ~~ A
Theorem	entr3 4418	A chained equinumerosity inference.
|- B e. V   &   |- A ~~ B   &   |- A ~~ C   =>   |- B ~~ C
Theorem	entr4 4419	A chained equinumerosity inference.
|- B e. V   &   |- A ~~ B   &   |- C ~~ B   =>   |- A ~~ C
Theorem	endomtr 4420	Transitivity of equinumerosity and dominance.
|- ((A ~~ B /\ B ~<_ C) -> A ~<_ C)
Theorem	domentr 4421	Transitivity of dominance and equinumerosity.
|- ((A ~<_ B /\ B ~~ C) -> A ~<_ C)
Theorem	f1imaen 4422	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 4423	The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88.
|- (A ~~ (/) <-> A = (/))
Theorem	ensn1 4424	A singleton is equinumerous to ordinal one.
|- A e. V   =>   |- {A} ~~ 1o
Theorem	ensn1g 4425	A singleton is equinumerous to ordinal one.
|- (A e. B -> {A} ~~ 1o)
Theorem	en1 4426	A set is equinumerous to ordinal one iff it is a singleton.
|- (A ~~ 1o <-> E.x A = {x})
Theorem	2dom 4427	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 4428	A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98.
|- F e. V   =>   |- (Fun F -> dom F ~~ F)
Theorem	mapsnen 4429	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 4430	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 4431	Two singletons are equinumerous.
|- ((A e. C /\ B e. D) -> {A} ~~ {B})
Theorem	snfi 4432	A singleton is finite.
|- {A} e. Fin
Theorem	snfiOLD 4433	A singleton is finite.
|- E.x e. om {A} ~~ x
Theorem	unen 4434	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 4435	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 4436	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 4437	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 4438	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 4439	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 4440	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 4441	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 4442	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 4443	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 4444	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 4445	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 4446	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 4447	Lemma for sbth 4457.
Theorem	sbthlem2 4448	Lemma for sbth 4457.
Theorem	sbthlem3 4449	Lemma for sbth 4457.
Theorem	sbthlem4 4450	Lemma for sbth 4457.
Theorem	sbthlem5 4451	Lemma for sbth 4457.
Theorem	sbthlem6 4452	Lemma for sbth 4457.
Theorem	sbthlem7 4453	Lemma for sbth 4457.
Theorem	sbthlem8 4454	Lemma for sbth 4457.
Theorem	sbthlem9 4455	Lemma for sbth 4457.
Theorem	sbthlem10 4456	Lemma for sbth 4457.
Theorem	sbth 4457	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 4447 through sbthlem10 4456; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlem10 4456. 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 4458	Schroeder-Bernstein Theorem and its converse.
|- (B e. C -> ((A ~<_ B /\ B ~<_ A) <-> A ~~ B))
Theorem	sbthcl 4459	Schroeder-Bernstein Theorem in class form.
|- ~~ = ( ~<_ i^i `' ~<_ )
Theorem	dfsdom2 4460	Alternate definition of strict dominance. Compare Definition 3 of [Suppes] p. 97.
|- ~< = ( ~<_ \ `' ~<_ )
Theorem	brsdom2 4461	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 4462	Strict dominance is not symmetric. Theorem 21(ii) of [Suppes] p. 97.
|- (A ~< B -> -. B ~< A)
Theorem	domnsym 4463	Theorem 22(i) of [Suppes] p. 97.
|- (A ~<_ B -> -. B ~< A)
Theorem	0dom 4464	Any set dominates the empty set.
|- (/) ~<_ A
Theorem	dom0 4465	A set dominated by the empty set is empty.
|- (A ~<_ (/) <-> A = (/))
Theorem	0sdomg 4466	A set strictly dominates the empty set iff it is not empty.
|- (A e. B -> ((/) ~< A <-> A =/= (/)))
Theorem	0sdom 4467	A set strictly dominates the empty set iff it is not empty.
|- A e. V   =>   |- ((/) ~< A <-> A =/= (/))
Theorem	sdom0 4468	The empty set does not strictly dominate any set.
|- -. A ~< (/)
Theorem	sdomdomtr 4469	Transitivity of strict dominance and dominance. Theorem 22(iii) of [Suppes] p. 97.
|- (C e. D -> ((A ~< B /\ B ~<_ C) -> A ~< C))
Theorem	sdomentr 4470	Transitivity of strict dominance and equinumerosity. Exercise 11 of [Suppes] p. 98.
|- (C e. D -> ((A ~< B /\ B ~~ C) -> A ~< C))
Theorem	ensdomtr 4471	Transitivity of equinumerosity and strict dominance.
|- ((A ~~ B /\ B ~< C) -> A ~< C)
Theorem	sdomirr 4472	Strict dominance is irreflexive. Theorem 21(i) of [Suppes] p. 97.
|- -. A ~< A
Theorem	sdomex 4473	Technical lemma for simplifying proofs involving strict dominance.
|- (A ~< B -> (A e. V /\ B e. V))
Theorem	sdomtr 4474	Strict dominance is transitive. Theorem 21(iii) of [Suppes] p. 97.
|- ((A ~< B /\ B ~< C) -> A ~< C)
Theorem	sdomn2lp 4475	Strict dominance has no 2-cycle loops.
|- -. (A ~< B /\ B ~< A)
Theorem	domsdomtr 4476	Transitivity of dominance and strict dominance. Theorem 22(ii) of [Suppes] p. 97.
|- ((A ~<_ B /\ B ~< C) -> A ~< C)
Theorem	enen1 4477	Equality-like theorem for equinumerosity.
|- ((B e. D /\ A ~~ B) -> (A ~~ C <-> B ~~ C))
Theorem	enen2 4478	Equality-like theorem for equinumerosity.