mmtheorems78 - 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-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Statement List for Metamath Proof Explorer - 7701-7800 - Page 78 of 123

Type	Label	Description
Statement
Theorem	acdc2lem2 7701	Lemma for acdc2 7702. Build a sequence G starting at value c, as follows. Given a previous value x of G, we construct, for the next value of G, the v such that A.u e. (yFx)-. urv, which is unique when r is a well-ordering on A.
Theorem	acdc2 7702	A more general version of acdc 7707 that allows the function F to vary with k.
|- A e. V   =>   |- ((A =/= (/) /\ F:(NN X. A)-->(P~A \ {(/)})) -> E.g(g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))))
Theorem	acdc5lem1 7703	Lemma for acdc5 7705.
Theorem	acdc5lem2 7704	Lemma for acdc5 7705. Build a sequence G starting at value c, as follows. Given a previous value x of G, we construct, for the next value of G, the v such that A.u e. (yFx)-. urv, which is unique when r is a well-ordering on A.
Theorem	acdc5 7705	A more general version of acdc 7707 that has an initial value and where the function F depends on k.
|- A e. V   =>   |- ((F:(NN X. A)-->(P~A \ {(/)}) /\ C e. A) -> E.g(g:NN-->A /\ (g` 1) = C /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))))
Theorem	acdclem 7706	Lemma for acdc 7707. Build a sequence G starting at value c, as follows. Given a previous value x of G, we construct, for the next value of G, the v such that A.u e. (F` x)-. urv, which is unique when r is a well-ordering on A.
Theorem	acdc 7707	Dependent Choice. Axiom DC1 of [Schechter] p. 149. This theorem is weaker than the Axiom of Choice but is stronger than Countable Choice. It shows the existence of a sequence whose values can only be shown to exist (but cannot be constructed explicitly) and also depend on earlier values in the sequence.
|- A e. V   =>   |- ((A =/= (/) /\ F:A-->(P~A \ {(/)})) -> E.g(g:NN-->A /\ A.k e. NN (g` (k + 1)) e. (F` (g` k))))
Theorem	acdcALT 7708	Dependent Choice. Axiom DC1 of [Schechter] p. 149. This theorem is weaker than the Axiom of Choice but is stronger than Countable Choice. It shows the existence of a sequence whose values can only be shown to exist (but cannot be constructed explicitly) and also depend on earlier values in the sequence.
|- A e. V   =>   |- ((A =/= (/) /\ F:A-->(P~A \ {(/)})) -> E.g(g:NN-->A /\ A.k e. NN (g` (k + 1)) e. (F` (g` k))))
Cardinality and cardinal arithmetic (cont.)
Countability of integers and rationals
Theorem	nn0ennn 7709	The nonnegative integers are equinumerous to the natural numbers.
|- NN0 ~~ NN
Theorem	nnenom 7710	The set of natural numbers (as a subset of complex numbers) is equinumerous to omega (the set of finite ordinal numbers).
|- NN ~~ om
Theorem	xpnnen 7711	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 nn0opth2 6869 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 7712	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 4602 in xpnnen 7711).
|- (om X. om) ~~ om
Theorem	znnenlem 7713	Lemma for znnen 7714.
Theorem	znnen 7714	The set of integers and the set of natural numbers are equinumerous. Exercise 1 of [Gleason] p. 140.
|- ZZ ~~ NN
Theorem	qnnen 7715	The rational numbers are countable. (This unusual proof uses the Axiom of Choice via fodom 4944 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 7716	Lemma for unben 7717.
Theorem	unben 7717	An unbounded set of natural numbers is infinite.
|- ((A (_ NN /\ A.m e. NN E.n e. A m < n) -> A ~~ NN)
Theorem	infpnlem1 7718	Lemma for infpn 7720. The smallest divisor (greater than 1) M of N! + 1 is a prime greater than N.
Theorem	infpnlem2 7719	Lemma for infpn 7720. For any natural number N, there exists a prime number j greater than N.
Theorem	infpn 7720	There exist infinitely many prime numbers: for any natural number N, there exists a prime number j greater than N. (See infpn2 7721 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 7721	There exist infinitely many prime numbers: the set of all primes S is unbounded by infpn 7720, so by unben 7717 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 7722	Lemma for ruc 7761 (the reals are uncountable). This is an arithmetic fact that will be used to compute ordering relations.
Theorem	ruclem2 7723	Lemma for ruc 7761. Arithmetic fact that will be used to compute ordering relations.
Theorem	ruclem3 7724	Lemma for ruc 7761. Arithmetic fact that will be used to compute ordering relations.
Theorem	ruclem4 7725	Lemma for ruc 7761. Helper lemma showing a tedious equality used several times.
Theorem	ruclem5 7726	Lemma for ruc 7761. Helper lemma showing the input function used for our recursive sequence builder (defined in ruclem13 7734) is a set.
Theorem	ruclem6 7727	Lemma for ruc 7761. Helper lemma showing the input function used for our recursive sequence builder (defined in ruclem13 7734) matches our input mapping F for successor values.
Theorem	ruclem7 7728	Lemma for ruc 7761. Helper lemma showing the initial value of the input function for our recursive sequence builder (defined in ruclem13 7734).
Theorem	ruclem8 7729	Lemma for ruc 7761. Helper lemma showing the successor value of the input function for our recursive sequence builder (defined in ruclem13 7734).
Theorem	ruclem9 7730	Lemma for ruc 7761. Helper lemma showing the operation used for our recursive sequence builder (defined in ruclem13 7734) is a set.
Theorem	ruclem10 7731	Lemma for ruc 7761. 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 7732	Lemma for ruc 7761. 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 7733	Lemma for ruc 7761. A helper lemma that changes bound variables.
Theorem	ruclem13 7734	Lemma for ruc 7761. A helper lemma showing the recursive sequence builder used for our construction maps natural numbers to pairs of reals.
Theorem	ruclem14 7735	Lemma for ruc 7761. A helper lemma showing the initial value of the recursive sequence builder used for our construction.
Theorem	ruclem15 7736	Lemma for ruc 7761. A helper lemma showing the successor value of the recursive sequence builder used for our construction.
Theorem	ruclem16 7737	Lemma for ruc 7761. A helper lemma showing the initial value of our constructed G.
Theorem	ruclem17 7738	Lemma for ruc 7761. A helper lemma showing our constructed function G maps NN to real numbers.
Theorem	ruclem18 7739	Lemma for ruc 7761. 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 7740) that avoids the value of F.
Theorem	ruclem19 7740	Lemma for ruc 7761. 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 7739) that avoids the value of F.
Theorem	ruclem20 7741	Lemma for ruc 7761. 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 7742	Lemma for ruc 7761. 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 7743	Lemma for ruc 7761. Each value of our constructed function G is a real number.
Theorem	ruclem23 7744	Lemma for ruc 7761. Each value of our constructed function H is a real number.
Theorem	ruclem24 7745	Lemma for ruc 7761. A helper lemma for the induction hypothesis in ruclem25 7746.
Theorem	ruclem25 7746	Lemma for ruc 7761. At any index A, the value of G is less than the value of H.
Theorem	ruclem26 7747	Lemma for ruc 7761. Our constructed function G has an ever-increasing set of values.
Theorem	ruclem27 7748	Lemma for ruc 7761. Our constructed function H has an ever-decreasing set of values.
Theorem	ruclem28 7749	Lemma for ruc 7761. A helper lemma for ruclem29 7750.
Theorem	ruclem29 7750	Lemma for ruc 7761. 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 7747 and ruclem27 7748, an ever-shrinking interval that eventually squeezes out all values of F.
Theorem	ruclem30 7751	Lemma for ruc 7761. A helper lemma for ruclem32 7753.
Theorem	ruclem31 7752	Lemma for ruc 7761. A helper lemma for ruclem32 7753.
Theorem	ruclem32 7753	Lemma for ruc 7761. All values of function G are less than all values of function H.
Theorem	ruclem33 7754	Lemma for ruc 7761. 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 7755	Lemma for ruc 7761. The supremum of the set of values of our constructed function G is a real number.
Theorem	ruclem35 7756	Lemma for ruc 7761. The supremum we have constructed lies between all values of the G and H functions. Compare ruclem29 7750, which states the opposite for the input function F.
Theorem	ruclem36 7757	Lemma for ruc 7761. No value of F is equal to the supremum we have constructed.
Theorem	ruclem37 7758	Lemma for ruc 7761. If F is any function that maps NN into RR, then F cannot be onto RR.
Theorem	ruclem38 7759	Lemma for ruc 7761. If F is any function that maps NN into RR, then F cannot be onto RR. Using eqid 1518, this lemma eliminates those hypotheses of ruclem37 7758 that are no longer needed.
Theorem	ruclem39 7760	Lemma for ruc 7761. There is no function that maps NN onto RR. (Use nex 1137 if you want this in the form -. E.ff:NN-onto->RR.)
Theorem	ruc 7761	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 7722 through ruclem39 7760 and this final piece. Our proof is based on the proof of Theorem 5.18 of [Truss] p. 114. See ruclem39 7760 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 7762	The set of rationals is strictly less equinumerous than the set of reals (RR strictly dominates QQ).
|- QQ ~< RR
Theorem	aleph1re 7763	There are at least aleph-one real numbers.
|- (aleph` 1o) ~<_ RR
Cardinal arithmetic (cont.)
Theorem	infxpidmlem1 7764	Lemma for infxpidm 7776. An infinite idempotent set x is equinumerous to the union of any two sets A and B equinumerous to it.
Theorem	infxpidmlem2 7765	Lemma for infxpidm 7776. A necessary and sufficient condition for a set B to belong to H.
Theorem	infxpidmlem3 7766	Lemma for infxpidm 7776. A sufficient condition for a set B to belong to H.
Theorem	infxpidmlem4 7767	Lemma for infxpidm 7776. The domain of a member of H is the cross product of its range.
Theorem	infxpidmlem5 7768	Lemma for infxpidm 7776. 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 7769	Lemma for infxpidm 7776. A simple but frequently used fact.
Theorem	infxpidmlem7 7770	Lemma for infxpidm 7776. The union of a collection C of chains in H is a bijection.
Theorem	infxpidmlem8 7771	Lemma for infxpidm 7776. 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 7772.
Theorem	infxpidmlem9 7772	Lemma for infxpidm 7776. By Zorn's Lemma zorn 4943, the collection H (which we show here to be a set) has a maximal element.
Theorem	infxpidmlem10 7773	Lemma for infxpidm 7776. A maximal bijection g in H is non-empty.
Theorem	infxpidmlem11 7774	Lemma for infxpidm 7776. 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 7775	Lemma for infxpidm 7776. Letting x be the range of a maximal bijection g in H, infxpidmlem11 7774 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 7772, A is also idempotent.
Theorem	infxpidm 7776	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 7764 through infxpidmlem12 7775. This final piece eliminates the first hypothesis of infxpidmlem12 7775.
|- A e. V   =>   |- (om ~<_ A -> (A X. A) ~~ A)
Theorem	infunabs 7777	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 7778	Absorption law for addition to an infinite cardinal.
|- A e. V   &   |- B e. V   =>   |- ((om ~<_ A /\ B ~<_ A) -> (A +c B) ~~ A)
Theorem	infcda 7779	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 7780	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 7781	Cardinality ordering for an infinite set difference.
|- A e. V   &   |- B e. V   =>   |- (om ~<_ A -> ((A \ B) ~<_ B <-> A ~<_ B))
Theorem	infxpabs 7782	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 7783	Dominance law for multiplication with an infinite cardinal.
|- A e. V   &   |- B e. V   =>   |- ((om ~<_ A /\ B ~<_ A) -> (A X. B) ~<_ A)
Theorem	infxp 7784	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 7785	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 7786	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 7787	The countable union of countable sets is countable (indexed union version of unictb 7788).
|- A e. V   &   |- B e. V   =>   |- ((A ~<_ om /\ A.x e. A B ~<_ om) -> U_x e. A B ~<_ om)
Theorem	unictb 7788	The countable union of countable sets is countable. Theorem 6Q of [Enderton] p. 159. See iunctb 7787 for indexed union version.
|- A e. V   =>   |- ((A ~<_ om /\ A.x e. A x ~<_ om) -> U.A ~<_ om)
Theorem	unctb 7789	The union of two countable sets is countable. (Contributed by FL, 25-Aug-2006.)
|- ((A ~<_ om /\ B ~<_ om) -> (A u. B) ~<_ om)
Theorem	aleph1irr 7790	There are at least aleph-one irrationals.
|- (aleph` 1o) ~<_ (RR \ QQ)
Theorem	infmap2lem1 7791	Lemma for infmap2 7793. Technical result that is used several times.
Theorem	infmap2lem2 7792	Lemma for infmap2 7793. Given the relation R, we use the Axiom of Choice ac7g 4895 to extract a function f that provides the one-to-one mapping for the dominance relation.
Theorem	infmap2 7793	An exponentiation law for infinite cardinals. Similar to Lemma 6.2 of [Jech] p. 43. We start with infmap2lem2 7792 and also prove the other direction of the dominance relation. We obtain equinumerosity with Schroeder-Bernstein sbth 4602 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 7794	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 7795	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 7796	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 7797	An alternate representation of a successor aleph. Compare alephsuc 5016 and alephsuc2 5031. Equality can be obtained by taking the card of the right-hand side then using alephcard 5017 and carden 4979.
|- (A e. On -> (aleph` suc A) ~~ {x e. On | x ~~ (aleph` A)})
Theorem	alephexp2 7798	An expression equinumerous to 2 to an aleph power. The proof equates the two laws for cardinal exponentiation alephexp1 7796 (which works if the base is less than or equal to the exponent) and infmap2 7793 (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 7799	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 7798 to the successor aleph using enen2 4623.
|- (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 7800	Extend class notation with the class of all topologies.
class Top