mmtheorems76 - 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-10783

Statement List for Metamath Proof Explorer - 7501-7600 - Page 76 of 108

Type	Label	Description
Statement
Theorem	xpnnen 7501	The cross product of the set of natural numbers with itself is equinumerous to the set of natural numbers. The key idea is to use nn0opth2t 6670 to show that the mapping from natural numbers z and w to ((z + w)^2) + w is one-to-one.
|- (NN X. NN) ~~ NN
Theorem	xpomen 7502	The cross product of omega (the set of ordinal natural numbers) with itself is equinumerous to omega. Exercise 1 of [Enderton] p. 133 (which proves this with a direct, but longer, proof; ours uses instead the Schroeder-Bernstein Theorem sbth 4457 in xpnnen 7501).
|- (om X. om) ~~ om
Theorem	znnenlem 7503	Lemma for znnen 7504.
Theorem	znnen 7504	The set of integers and the set of natural numbers are equinumerous. Exercise 1 of [Gleason] p. 140.
|- ZZ ~~ NN
Theorem	qnnen 7505	The rational numbers are countable. (This unusual proof uses the Axiom of Choice via fodom 4798 to make it much shorter, but this theorem can also be proved without it. See, for example, Exercise 2 of [Enderton] p. 133.)
|- QQ ~~ NN
Infinite primes theorem
Theorem	unbenlem 7506	Lemma for unben 7507.
Theorem	unben 7507	An unbounded set of natural numbers is infinite.
|- ((A (_ NN /\ A.m e. NN E.n e. A m < n) -> A ~~ NN)
Theorem	infpnlem1 7508	Lemma for infpn 7510. The smallest divisor (greater than 1) M of N! + 1 is a prime greater than N.
Theorem	infpnlem2 7509	Lemma for infpn 7510. For any natural number N, there exists a prime number j greater than N.
Theorem	infpn 7510	There exist infinitely many prime numbers: for any natural number N, there exists a prime number j greater than N. (See infpn2 7511 for the equinumerosity version.)
|- (N e. NN -> E.j e. NN (N < j /\ A.k e. NN ((j / k) e. NN -> (k = 1 \/ k = j))))
Theorem	infpn2 7511	There exist infinitely many prime numbers: the set of all primes S is unbounded by infpn 7510, so by unben 7507 it is infinite.
|- S = {n e. NN | (1 < n /\ A.m e. NN ((n / m) e. NN -> (m = 1 \/ m = n)))}   =>   |- S ~~ NN
The reals are uncountable
Theorem	ruclem1 7512	Lemma for ruc 7551 (the reals are uncountable). This is an arithmetic fact that will be used to compute ordering relations.
Theorem	ruclem2 7513	Lemma for ruc 7551. Arithmetic fact that will be used to compute ordering relations.
Theorem	ruclem3 7514	Lemma for ruc 7551. Arithmetic fact that will be used to compute ordering relations.
Theorem	ruclem4 7515	Lemma for ruc 7551. Helper lemma showing a tedious equality used several times.
Theorem	ruclem5 7516	Lemma for ruc 7551. Helper lemma showing the input function used for our recursive sequence builder (defined in ruclem13 7524) is a set.
Theorem	ruclem6 7517	Lemma for ruc 7551. Helper lemma showing the input function used for our recursive sequence builder (defined in ruclem13 7524) matches our input mapping F for successor values.
Theorem	ruclem7 7518	Lemma for ruc 7551. Helper lemma showing the initial value of the input function for our recursive sequence builder (defined in ruclem13 7524).
Theorem	ruclem8 7519	Lemma for ruc 7551. Helper lemma showing the successor value of the input function for our recursive sequence builder (defined in ruclem13 7524).
Theorem	ruclem9 7520	Lemma for ruc 7551. Helper lemma showing the operation used for our recursive sequence builder (defined in ruclem13 7524) is a set.
Theorem	ruclem10 7521	Lemma for ruc 7551. The values of our recursive sequence builder are pairs of real numbers. The values of our constructed function G are the first of these pairs.
Theorem	ruclem11 7522	Lemma for ruc 7551. The values of our recursive sequence builder are pairs of real numbers. The values of our constructed function H are the second of these pairs.
Theorem	ruclem12 7523	Lemma for ruc 7551. A helper lemma that changes bound variables.
Theorem	ruclem13 7524	Lemma for ruc 7551. A helper lemma showing the recursive sequence builder used for our construction maps natural numbers to pairs of reals.
Theorem	ruclem14 7525	Lemma for ruc 7551. A helper lemma showing the initial value of the recursive sequence builder used for our construction.
Theorem	ruclem15 7526	Lemma for ruc 7551. A helper lemma showing the successor value of the recursive sequence builder used for our construction.
Theorem	ruclem16 7527	Lemma for ruc 7551. A helper lemma showing the initial value of our constructed G.
Theorem	ruclem17 7528	Lemma for ruc 7551. A helper lemma showing our constructed function G maps NN to real numbers.
Theorem	ruclem18 7529	Lemma for ruc 7551. The value of our constructed function G when the value of the input function F lies between the previous values of G and H. This assignment to G defines a new interval between G and H (see also ruclem19 7530) that avoids the value of F.
Theorem	ruclem19 7530	Lemma for ruc 7551. The value of our constructed function H when the value of the input function F lies between the previous values of G and H. This assignment to H defines a new interval between G and H (see also ruclem18 7529) that avoids the value of F.
Theorem	ruclem20 7531	Lemma for ruc 7551. The value of our constructed function G when the value of the input function F does not lie between the previous values of G and H. This assignment to G just shrinks the interval between G and H by some arbitrary amount.
Theorem	ruclem21 7532	Lemma for ruc 7551. The value of our constructed function H when the value of the input function F does not lie between the previous values of G and H. This assignment to H just shrinks the interval between G and H by some arbitrary amount.
Theorem	ruclem22 7533	Lemma for ruc 7551. Each value of our constructed function G is a real number.
Theorem	ruclem23 7534	Lemma for ruc 7551. Each value of our constructed function H is a real number.
Theorem	ruclem24 7535	Lemma for ruc 7551. A helper lemma for the induction hypothesis in ruclem25 7536.
Theorem	ruclem25 7536	Lemma for ruc 7551. At any index A, the value of G is less than the value of H.
Theorem	ruclem26 7537	Lemma for ruc 7551. Our constructed function G has an ever-increasing set of values.
Theorem	ruclem27 7538	Lemma for ruc 7551. Our constructed function H has an ever-decreasing set of values.
Theorem	ruclem28 7539	Lemma for ruc 7551. A helper lemma for ruclem29 7540.
Theorem	ruclem29 7540	Lemma for ruc 7551. At any index A, the interval between our constructed functions G and H does not include the corresponding value of input function F. In other words, our constructed functions define, by ruclem26 7537 and ruclem27 7538, an ever-shrinking interval that eventually squeezes out all values of F.
Theorem	ruclem30 7541	Lemma for ruc 7551. A helper lemma for ruclem32 7543.
Theorem	ruclem31 7542	Lemma for ruc 7551. A helper lemma for ruclem32 7543.
Theorem	ruclem32 7543	Lemma for ruc 7551. All values of function G are less than all values of function H.
Theorem	ruclem33 7544	Lemma for ruc 7551. The set of values of our constructed function G is a non-empty subset of RR. This is a helper lemma for theorems involving supremum.
Theorem	ruclem34 7545	Lemma for ruc 7551. The supremum of the set of values of our constructed function G is a real number.
Theorem	ruclem35 7546	Lemma for ruc 7551. The supremum we have constructed lies between all values of the G and H functions. Compare ruclem29 7540, which states the opposite for the input function F.
Theorem	ruclem36 7547	Lemma for ruc 7551. No value of F is equal to the supremum we have constructed.
Theorem	ruclem37 7548	Lemma for ruc 7551. If F is any function that maps NN into RR, then F cannot be onto RR.
Theorem	ruclem38 7549	Lemma for ruc 7551. If F is any function that maps NN into RR, then F cannot be onto RR. Using eqid 1475, this lemma eliminates those hypotheses of ruclem37 7548 that are no longer needed.
Theorem	ruclem39 7550	Lemma for ruc 7551. There is no function that maps NN onto RR. (Use nex 1101 if you want this in the form -. E.ff:NN-onto->RR.)
Theorem	ruc 7551	The set of natural numbers is strictly dominated by the set of real numbers, i.e. the real numbers are uncountable. The proof consists of lemmas ruclem1 7512 through ruclem39 7550 and this final piece. Our proof is based on the proof of Theorem 5.18 of [Truss] p. 114. See ruclem39 7550 for the function existence version of this theorem. For an informal discussion of this proof, see http://us.metamath.org/mpegif/mmcomplex.html#uncountable.
|- NN ~< RR
Theorem	resdomq 7552	The set of rationals is strictly less equinumerous than the set of reals (RR strictly dominates QQ).
|- QQ ~< RR
Theorem	aleph1re 7553	There are at least aleph-one real numbers.
|- (aleph` 1o) ~<_ RR
Cardinal arithmetic (cont.)
Theorem	infxpidmlem1 7554	Lemma for infxpidm 7566. An infinite idempotent set x is equinumerous to the union of any two sets A and B equinumerous to it.
Theorem	infxpidmlem2 7555	Lemma for infxpidm 7566. A necessary and sufficient condition for a set B to belong to H.
Theorem	infxpidmlem3 7556	Lemma for infxpidm 7566. A sufficient condition for a set B to belong to H.
Theorem	infxpidmlem4 7557	Lemma for infxpidm 7566. The domain of a member of H is the cross product of its range.
Theorem	infxpidmlem5 7558	Lemma for infxpidm 7566. Two members in the range of a member of a subset of H form an ordered pair belonging to the domain of the union of the subset.
Theorem	infxpidmlem6 7559	Lemma for infxpidm 7566. A simple but frequently used fact.
Theorem	infxpidmlem7 7560	Lemma for infxpidm 7566. The union of a collection C of chains in H is a bijection.
Theorem	infxpidmlem8 7561	Lemma for infxpidm 7566. The union of a collection of chains C in the collection of bijections H belongs to H. This property will be needed to apply Zorn's Lemma in infxpidmlem9 7562.
Theorem	infxpidmlem9 7562	Lemma for infxpidm 7566. By Zorn's Lemma zorn 4797, the collection H (which we show here to be a set) has a maximal element.
Theorem	infxpidmlem10 7563	Lemma for infxpidm 7566. A maximal bijection g in H is non-empty.
Theorem	infxpidmlem11 7564	Lemma for infxpidm 7566. We show that the union of a bijection g in H with a disjoint bijection u is a member h of H that is larger than (properly extends) g. Thus if the antecedent is true then g cannot be maximal.
Theorem	infxpidmlem12 7565	Lemma for infxpidm 7566. Letting x be the range of a maximal bijection g in H, infxpidmlem11 7564 lets us show that assuming x ~<_ (A \ x) leads to the contradiction E.h e. Hg (. h meaning g is not maximal. Thus (A \ x) ~< x. This allows us to show that x is as big as A. Since x is idempotent, and g exists by Zorn's Lemma in infxpidmlem9 7562, A is also idempotent.
Theorem	infxpidm 7566	The cross product of an infinite set with itself is idempotent. This theorem provides the basis for infinite cardinal arithmetic. Lemma 6R of [Enderton] p. 162, whose proof we follow closely. The main proof consists of infxpidmlem1 7554 through infxpidmlem12 7565. This final piece eliminates the first hypothesis of infxpidmlem12 7565.
|- A e. V   =>   |- (om ~<_ A -> (A X. A) ~~ A)
Theorem	infunabs 7567	An infinite set is equinumerous to its union with a smaller one.
|- A e. V   &   |- B e. V   =>   |- ((om ~<_ A /\ B ~<_ A) -> (A u. B) ~~ A)
Theorem	infcdaabs 7568	Absorption law for addition to an infinite cardinal.
|- A e. V   &   |- B e. V   =>   |- ((om ~<_ A /\ B ~<_ A) -> (A +c B) ~~ A)
Theorem	infcda 7569	The sum of two cardinal numbers is their maximum, if one of them is infinite. Proposition 10.41 of [TakeutiZaring] p. 95.
|- A e. V   &   |- B e. V   =>   |- (om ~<_ A -> (A +c B) ~~ (A u. B))
Theorem	infdif 7570	The cardinality of an infinite set does not change after subtracting a strictly smaller one. Example in [Enderton] p. 164.
|- A e. V   &   |- B e. V   =>   |- ((om ~<_ A /\ B ~< A) -> (A \ B) ~~ A)
Theorem	infdif2 7571	Cardinality ordering for an infinite set difference.
|- A e. V   &   |- B e. V   =>   |- (om ~<_ A -> ((A \ B) ~<_ B <-> A ~<_ B))
Theorem	infxpabs 7572	Absorption law for multiplication with an infinite cardinal.
|- A e. V   &   |- B e. V   =>   |- ((om ~<_ A /\ B =/= (/) /\ B ~<_ A) -> (A X. B) ~~ A)
Theorem	infxpdom 7573	Dominance law for multiplication with an infinite cardinal.
|- A e. V   &   |- B e. V   =>   |- ((om ~<_ A /\ B ~<_ A) -> (A X. B) ~<_ A)
Theorem	infxp 7574	Absorption law for multiplication with an infinite cardinal. Equivalent to Proposition 10.41 of [TakeutiZaring] p. 95.
|- A e. V   &   |- B e. V   =>   |- ((om ~<_ A /\ B =/= (/)) -> (A X. B) ~~ (A u. B))
Theorem	infmap1 7575	An exponentiation law for infinite cardinals. Exercise 34 of [Enderton] p. 165.
|- A e. V   &   |- B e. V   =>   |- (((2o ~<_ A /\ om ~<_ B) /\ A ~<_ B) -> (A ^m B) ~~ (2o ^m B))
Theorem	infpss 7576	Every infinite set has an equinumerous proper subset. Exercise 7 of [TakeutiZaring] p. 91.
|- A e. V   =>   |- (om ~<_ A -> E.x(x (. A /\ x ~~ A))
Theorem	iunctb 7577	The countable union of countable sets is countable (indexed union version of unictb 7578).
|- A e. V   &   |- B e. V   =>   |- ((A ~<_ om /\ A.x e. A B ~<_ om) -> U_x e. A B ~<_ om)
Theorem	unictb 7578	The countable union of countable sets is countable. Theorem 6Q of [Enderton] p. 159. See iunctb 7577 for indexed union version.
|- A e. V   =>   |- ((A ~<_ om /\ A.x e. A x ~<_ om) -> U.A ~<_ om)
Theorem	unctb 7579	The union of two countable sets is countable. (Contributed by FL, 25-Aug-2006.)
|- ((A ~<_ om /\ B ~<_ om) -> (A u. B) ~<_ om)
Theorem	aleph1irr 7580	There are at least aleph-one irrationals.
|- (aleph` 1o) ~<_ (RR \ QQ)
Theorem	infmap2lem1 7581	Lemma for infmap2 7583. Technical result that is used several times.
Theorem	infmap2lem2 7582	Lemma for infmap2 7583. Given the relation R, we use the Axiom of Choice ac7g 4749 to extract a function f that provides the one-to-one mapping for the dominance relation.
Theorem	infmap2 7583	An exponentiation law for infinite cardinals. Similar to Lemma 6.2 of [Jech] p. 43. We start with infmap2lem2 7582 and also prove the other direction of the dominance relation. We obtain equinumerosity with Schroeder-Bernstein sbth 4457 and finally eliminate the degenerate case B = (/).
|- A e. V   &   |- B e. V   =>   |- ((om ~<_ A /\ B ~<_ A) -> (A ^m B) ~~ {x | (x (_ A /\ x ~~ B)})
Theorem	alephadd 7584	The sum of two alephs is their maximum. Equation 6.1 of [Jech] p. 42.
|- ((aleph` A) +c (aleph` B)) ~~ ((aleph` A) u. (aleph` B))
Theorem	alephmul 7585	The product of two alephs is their maximum. Equation 6.1 of [Jech] p. 42.
|- ((A e. On /\ B e. On) -> ((aleph` A) X. (aleph` B)) ~~ ((aleph` A) u. (aleph` B)))
Theorem	alephexp1 7586	An exponentiation law for alephs. Lemma 6.1 of [Jech] p. 42.
|- (((A e. On /\ B e. On) /\ A (_ B) -> ((aleph` A) ^m (aleph` B)) ~~ (2o ^m (aleph` B)))
Theorem	alephsuc3 7587	An alternate representation of a successor aleph. Compare alephsuc 4866 and alephsuc2 4881. Equality can be obtained by taking the card of the right-hand side then using alephcard 4867 and carden 4831.
|- (A e. On -> (aleph` suc A) ~~ {x e. On | x ~~ (aleph` A)})
Theorem	alephexp2 7588	An expression equinumerous to 2 to an aleph power. The proof equates the two laws for cardinal exponentiation alephexp1 7586 (which works if the base is less than or equal to the exponent) and infmap2 7583 (which works if the exponent is less than or equal to the base). They can be equated only when the base is equal to the exponent, and this is the result.
|- (A e. On -> (2o ^m (aleph` A)) ~~ {x | (x (_ (aleph` A) /\ x ~~ (aleph` A))})
Continuum Hypothesis
Theorem	gch-kn 7589	The equivalence of two versions of the Generalized Continuum Hypothesis. The right-hand side is the standard version in the literature. The left-hand side is a version devised by Kannan Nambiar, which he calls the Axiom of Combinatorial Sets. For the notation and motivation behind this axiom, see his paper, "Derivation of Continuum Hypothesis from Axiom of Combinatorial Sets," available at http://www.e-atheneum.net/science/derivation_ch.pdf. The equivalence of the two sides provides a negative answer to Open Problem 2 in http://www.e-atheneum.net/science/open_problem_print.pdf. The key idea in the proof below is to equate both sides of alephexp2 7588 to the successor aleph using enen2 4478.
|- (A e. On -> ((aleph` suc A) ~~ {x | (x (_ (aleph` A) /\ x ~~ (aleph` A))} <-> (aleph` suc A) ~~ (2o ^m (aleph` A))))
Topology
Topological spaces
Syntax	ctop 7590	Extend class notation with the class of all topologies.
class Top
Syntax	ctps 7591	Extend class notation with the class of all topological spaces.
class TopSp
Syntax	ctb 7592	Extend class notation with the class of all topological bases.
class Bases
Syntax	ctg 7593	Extend class notation with a function that converts a basis to its corresponding topology.
class topGen
Definition	df-top 7594	Define the (proper) class of all topologies. See istop2g (future) for an alternate way to express finite intersection and istps5 (future) for a standard definition in terms of both members of a topological space.
|- Top = {x | (A.y(y (_ x -> U.y e. x) /\ A.y e. x A.z e. x (y i^i z) e. x)}
Definition	df-topsp 7595	Define the class of all topological spaces, each of which is an ordered pair the second of which is a topology on the first. See istps5 (future) for a standard way to express a topological space.
|- TopSp = {<.x, y>. | (y e. Top /\ x = U.y)}
Definition	df-bases 7596	Define the class of all topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 7614</