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-10684

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

Type	Label	Description
Statement
Theorem	ruclem30 7501	Lemma for ruc 7511. A helper lemma for ruclem32 7503.
Theorem	ruclem31 7502	Lemma for ruc 7511. A helper lemma for ruclem32 7503.
Theorem	ruclem32 7503	Lemma for ruc 7511. All values of function G are less than all values of function H.
Theorem	ruclem33 7504	Lemma for ruc 7511. 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 7505	Lemma for ruc 7511. The supremum of the set of values of our constructed function G is a real number.
Theorem	ruclem35 7506	Lemma for ruc 7511. The supremum we have constructed lies between all values of the G and H functions. Compare ruclem29 7500, which states the opposite for the input function F.
Theorem	ruclem36 7507	Lemma for ruc 7511. No value of F is equal to the supremum we have constructed.
Theorem	ruclem37 7508	Lemma for ruc 7511. If F is any function that maps NN into RR, then F cannot be onto RR.
Theorem	ruclem38 7509	Lemma for ruc 7511. If F is any function that maps NN into RR, then F cannot be onto RR. Using eqid 1473, this lemma eliminates those hypotheses of ruclem37 7508 that are no longer needed.
Theorem	ruclem39 7510	Lemma for ruc 7511. There is no function that maps NN onto RR. (Use nex 1099 if you want this in the form -. E.ff:NN-onto->RR.)
Theorem	ruc 7511	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 7472 through ruclem39 7510 and this final piece. Our proof is based on the proof of Theorem 5.18 of [Truss] p. 114. See ruclem39 7510 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 7512	The set of rationals is strictly less equinumerous than the set of reals (RR strictly dominates QQ).
|- QQ ~< RR
Theorem	aleph1re 7513	There are at least aleph-one real numbers.
|- (aleph` 1o) ~<_ RR
Cardinal arithmetic (cont.)
Theorem	infxpidmlem1 7514	Lemma for infxpidm 7526. An infinite idempotent set x is equinumerous to the union of any two sets A and B equinumerous to it.
Theorem	infxpidmlem2 7515	Lemma for infxpidm 7526. A necessary and sufficient condition for a set B to belong to H.
Theorem	infxpidmlem3 7516	Lemma for infxpidm 7526. A sufficient condition for a set B to belong to H.
Theorem	infxpidmlem4 7517	Lemma for infxpidm 7526. The domain of a member of H is the cross product of its range.
Theorem	infxpidmlem5 7518	Lemma for infxpidm 7526. 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 7519	Lemma for infxpidm 7526. A simple but frequently used fact.
Theorem	infxpidmlem7 7520	Lemma for infxpidm 7526. The union of a collection C of chains in H is a bijection.
Theorem	infxpidmlem8 7521	Lemma for infxpidm 7526. 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 7522.
Theorem	infxpidmlem9 7522	Lemma for infxpidm 7526. By Zorn's Lemma zorn 4788, the collection H (which we show here to be a set) has a maximal element.
Theorem	infxpidmlem10 7523	Lemma for infxpidm 7526. A maximal bijection g in H is non-empty.
Theorem	infxpidmlem11 7524	Lemma for infxpidm 7526. 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 7525	Lemma for infxpidm 7526. Letting x be the range of a maximal bijection g in H, infxpidmlem11 7524 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 7522, A is also idempotent.
Theorem	infxpidm 7526	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 7514 through infxpidmlem12 7525. This final piece eliminates the first hypothesis of infxpidmlem12 7525.
|- A e. V   =>   |- (om ~<_ A -> (A X. A) ~~ A)
Theorem	infunabs 7527	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 7528	Absorption law for addition to an infinite cardinal.
|- A e. V   &   |- B e. V   =>   |- ((om ~<_ A /\ B ~<_ A) -> (A +c B) ~~ A)
Theorem	infcda 7529	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 7530	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 7531	Cardinality ordering for an infinite set difference.
|- A e. V   &   |- B e. V   =>   |- (om ~<_ A -> ((A \ B) ~<_ B <-> A ~<_ B))
Theorem	infxpabs 7532	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 7533	Dominance law for multiplication with an infinite cardinal.
|- A e. V   &   |- B e. V   =>   |- ((om ~<_ A /\ B ~<_ A) -> (A X. B) ~<_ A)
Theorem	infxp 7534	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 7535	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	iunctb 7536	The countable union of countable sets is countable (indexed union version of unictb 7537).
|- A e. V   &   |- B e. V   =>   |- ((A ~<_ om /\ A.x e. A B ~<_ om) -> U_x e. A B ~<_ om)
Theorem	unictb 7537	The countable union of countable sets is countable. Theorem 6Q of [Enderton] p. 159. See iunctb 7536 for indexed union version.
|- A e. V   =>   |- ((A ~<_ om /\ A.x e. A x ~<_ om) -> U.A ~<_ om)
Theorem	unctb 7538	The union of two countable sets is countable. (Contributed by FL, 25-Aug-2006.)
|- ((A ~<_ om /\ B ~<_ om) -> (A u. B) ~<_ om)
Theorem	aleph1irr 7539	There are at least aleph-one irrationals.
|- (aleph` 1o) ~<_ (RR \ QQ)
Theorem	infmap2lem1 7540	Lemma for infmap2 7542. Technical result that is used several times.
Theorem	infmap2lem2 7541	Lemma for infmap2 7542. Given the relation R, we use the Axiom of Choice ac7g 4740 to extract a function f that provides the one-to-one mapping for the dominance relation.
Theorem	infmap2 7542	An exponentiation law for infinite cardinals. Similar to Lemma 6.2 of [Jech] p. 43. We start with infmap2lem2 7541 and also prove the other direction of the dominance relation. We obtain equinumerosity with Schroeder-Bernstein sbth 4453 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 7543	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 7544	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 7545	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 7546	An alternate representation of a successor aleph. Compare alephsuc 4857 and alephsuc2 4872. Equality can be obtained by taking the card of the right-hand side then using alephcard 4858 and carden 4822.
|- (A e. On -> (aleph` suc A) ~~ {x e. On | x ~~ (aleph` A)})
Theorem	alephexp2 7547	An expression equinumerous to 2 to an aleph power. The proof equates the two laws for cardinal exponentiation alephexp1 7545 (which works if the base is less than or equal to the exponent) and infmap2 7542 (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 7548	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 7547 to the successor aleph using enen2 4474.
|- (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 7549	Extend class notation with the class of all topologies.
class Top
Syntax	ctps 7550	Extend class notation with the class of all topological spaces.
class TopSp
Syntax	ctb 7551	Extend class notation with the class of all topological bases.
class Bases
Syntax	ctg 7552	Extend class notation with a function that converts a basis to its corresponding topology.
class topGen
Definition	df-top 7553	Define the (proper) class of all topologies. See istop2g 7558 for an alternate way to express finite intersection and istps5 7571 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 7554	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 7571 for a standard way to express a topological space.
|- TopSp = {<.x, y>. | (y e. Top /\ x = U.y)}
Definition	df-bases 7555	Define the class of all topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 7573). Note that "bases" is the plural of "basis."
|- Bases = {x | A.y e. x A.z e. x (y i^i z) (_ U.(x i^i P~(y i^i z))}
Definition	df-topgen 7556	Define a function that converts a basis to its corresponding topology. Equivalent to the definition of a topology generated by a basis in [Munkres] p. 78 (see tgval2t 7578). See tgval3t 7586 for an alternate expression for the value.
|- topGen = {<.x, y>. | (x e. Bases /\ y = {z | z (_ U.(x i^i P~z)})}
Theorem	istopg 7557	Express the predicate "J is a topology." Note: In the literature, a topology is often represented by a script letter T, which resembles the letter J. This confusion has led to J being used by some authors - e.g. K. D. Joshi, Introduction to General Topology (1983), p. 114 - and it is convenient for us since we later use T to represent linear transformations (operators). (Contributed by Stefan Allan, 3-Mar-2006.)
|- (J e. A -> (J e. Top <-> (A.x(x (_ J -> U.x e. J) /\ A.x e. J A.y e. J (x i^i y) e. J)))
Theorem	istop2g 7558	Express the predicate "J is a topology," using "the intersection of the elements of any finite subcollection" instead of the intersection of any two elements.
|- (J e. A -> (J e. Top <-> (A.x(x (_ J -> U.x e. J) /\ A.x((x (_ J /\ x =/= (/) /\ E.y e. om x ~~ y) -> |^|x e. J))))
Theorem	uniopnt 7559	The union of a subset of a topology is an open set. (Contributed by Stefan Allan, 27-Feb-2006.)
|- ((J e. Top /\ A (_ J) -> U.A e. J)
Theorem	iunopnt 7560	The indexed union of a subset of a topology is an open set.
|- ((J e. Top /\ A.x e. A B e. J) -> U_x e. A B e. J)
Theorem	inopnt 7561	The intersection of two open sets of a topology is also an open set.
|- ((J e. Top /\ A e. J /\ B e. J) -> (A i^i B) e. J)
Theorem	0opnt 7562	The empty set is an open subset of a topology. (Contributed by Stefan Allan, 27-Feb-2006.)
|- (J e. Top -> (/) e. J)
Theorem	topopn 7563	The underlying set of a topology is an open set.
|- X = U.J   =>   |- (J e. Top -> X e. J)
Theorem	eltopss 7564	A member of a topology is a subset of its underlying set.
|- X = U.J   =>   |- ((J e. Top /\ A e. J) -> A (_ X)
Theorem	eltopsp 7565	Construct a topological space from a topology and vice-versa. We say that A is a topology on U.A. (This could be proved more efficiently from istps 7567, but the proof here does not require the Axiom of Regularity.)
|- (<.U.J, J>. e. TopSp <-> J e. Top)
Theorem	tpsex 7566	Existence implied by membership in a topological space. This technical lemma, which can help eliminate unnecessary antecedents, uses the Axiom of Regularity (via elirr 4590) along with definitional tricks.
|- (<.A, J>. e. TopSp -> (A e. V /\ J e. V))
Theorem	istps 7567	Express the predicate "is a topological space."
|- (<.A, J>. e. TopSp <-> (J e. Top /\ A = U.J))
Theorem	istps2 7568	Express the predicate "is a topological space."
|- (<.A, J>. e. TopSp <-> ((J e. Top /\ J (_ P~A) /\ ((/) e. J /\ A e. J)))
Theorem	istps3 7569	A standard textbook definition of a topological space.
|- (<.A, J>. e. TopSp <-> ((J (_ P~A /\ (/) e. J /\ A e. J) /\ (A.x(x (_ J -> U.x e. J) /\ A.x e. J A.y e. J (x i^i y) e. J)))
Theorem	istps4 7570	A standard textbook definition of a topological space.
|- (<.A, J>. e. TopSp <-> ((J (_ P~A /\ (/) e. J /\ A e. J) /\ (A.x(x (_ J -> U.x e. J) /\ A.x((x (_ J /\ x =/= (/) /\ E.y e. om x ~~ y