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

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

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