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

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

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