mmtheorems77 - 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-10774

Statement List for Metamath Proof Explorer - 7601-7700 - Page 77 of 108

Type	Label	Description
Statement
Theorem	alephexp2 7601	An expression equinumerous to 2 to an aleph power. The proof equates the two laws for cardinal exponentiation alephexp1 7599 (which works if the base is less than or equal to the exponent) and infmap2 7596 (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 7602	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 7601 to the successor aleph using enen2 4488.
|- (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 7603	Extend class notation with the class of all topologies.
class Top
Syntax	ctps 7604	Extend class notation with the class of all topological spaces.
class TopSp
Syntax	ctb 7605	Extend class notation with the class of all topological bases.
class Bases
Syntax	ctg 7606	Extend class notation with a function that converts a basis to its corresponding topology.
class topGen
Definition	df-top 7607	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 7608	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 7609	Define the class of all topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 7624). 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 7610	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 7629). See tgval3t 7637 for an alternate expression for the value.
|- topGen = {<.x, y>. | (x e. Bases /\ y = {z | z (_ U.(x i^i P~z)})}
Theorem	istopg 7611	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	uniopnt 7612	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 7613	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 7614	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 7615	The empty set is an open subset of a topology. (Contributed by Stefan Allan, 27-Feb-2006.)
|- (J e. Top -> (/) e. J)
Theorem	topopn 7616	The underlying set of a topology is an open set.
|- X = U.J   =>   |- (J e. Top -> X e. J)
Theorem	eltopss 7617	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 7618	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 7620, but the proof here does not require the Axiom of Regularity.)
|- (<.U.J, J>. e. TopSp <-> J e. Top)
Theorem	tpsex 7619	Existence implied by membership in a topological space. This technical lemma, which can help eliminate unnecessary antecedents, uses the Axiom of Regularity (via elirr 4618) along with definitional tricks.
|- (<.A, J>. e. TopSp -> (A e. V /\ J e. V))
Theorem	istps 7620	Express the predicate "is a topological space."
|- (<.A, J>. e. TopSp <-> (J e. Top /\ A = U.J))
Theorem	istps2 7621	Express the predicate "is a topological space."
|- (<.A, J>. e. TopSp <-> ((J e. Top /\ J (_ P~A) /\ ((/) e. J /\ A e. J)))
Theorem	istps3 7622	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)))
Bases for topologies
Theorem	isbasisg 7623	Express the predicate "B is a basis for a topology."
|- (B e. C -> (B e. Bases <-> A.x e. B A.y e. B (x i^i y) (_ U.(B i^i P~(x i^i y))))
Theorem	isbasis2g 7624	Express the predicate "B is a basis for a topology."
|- (B e. C -> (B e. Bases <-> A.x e. B A.y e. B A.z e. (x i^i y)E.w e. B (z e. w /\ w (_ (x i^i y))))
Theorem	isbasis3g 7625	Express the predicate "B is a basis for a topology." Definition of basis in [Munkres] p. 78.
|- (B e. C -> (B e. Bases <-> (A.x e. B x (_ U.B /\ A.x e. U.BE.y e. B x e. y /\ A.x e. B A.y e. B A.z e. (x i^i y)E.w e. B (z e. w /\ w (_ (x i^i y)))))
Theorem	basis1t 7626	Property of a basis.
|- ((B e. Bases /\ C e. B /\ D e. B) -> (C i^i D) (_ U.(B i^i P~(C i^i D)))
Theorem	basis2t 7627	Property of a basis.
|- (((B e. Bases /\ C e. B) /\ (D e. B /\ A e. (C i^i D))) -> E.x e. B (A e. x /\ x (_ (C i^i D)))
Theorem	tgvalt 7628	The topology generated by a basis.
|- (B e. Bases -> (topGen` B) = {x | x (_ U.(B i^i P~x)})
Theorem	tgval2t 7629	Definition of a topology generated by a basis in [Munkres] p. 78. Later we show (in tgclt 7636) that (topGen` B) is indeed a topology (on U.B; see unitgt 7635).
|- (B e. Bases -> (topGen` B) = {x | (x (_ U.B /\ A.y e. x E.z e. B (y e. z /\ z (_ x))})
Theorem	eltgt 7630	Membership in a topology generated by a basis.
|- (B e. Bases -> (A e. (topGen` B) <-> A (_ U.(B i^i P~A)))
Theorem	eltg2t 7631	Membership in a topology generated by a basis.
|- (B e. Bases -> (A e. (topGen` B) <-> (A (_ U.B /\ A.x e. A E.y e. B (x e. y /\ y (_ A))))
Theorem	tg1t 7632	Property of a member of a topology generated by a basis.
|- ((B e. Bases /\ A e. (topGen` B)) -> A (_ U.B)
Theorem	tg2t 7633	Property of a member of a topology generated by a basis.
|- ((B e. Bases /\ A e. (topGen` B) /\ C e. A) -> E.x e. B (C e. x /\ x (_ A))
Theorem	bastgt 7634	A member of a basis is a subset of the topology it generates.
|- (B e. Bases -> B (_ (topGen` B))
Theorem	unitgt 7635	The topology generated by a basis B is a topology on U.B. Importantly, this theorem means that we don't have to specify separately the base set for the topological space generated by a basis. In other words, any member of the class Bases completely specifies the basis it corresponds to.
|- (B e. Bases -> U.(topGen` B) = U.B)
Theorem	tgclt 7636	Show that a basis generates a topology. Remark in [Munkres] p. 79.
|- (B e. Bases -> (topGen` B) e. Top)
Theorem	tgval3t 7637	Alternate expression for the topology generated by a basis. Lemma 2.1 of [Munkres] p. 80.
|- (B e. Bases -> (topGen` B) = {x | E.y(y (_ B /\ x = U.y)})
Theorem	eltg3t 7638	Membership in a topology generated by a basis.
|- (B e. Bases -> (A e. (topGen` B) <-> E.x(x (_ B /\ A = U.x)))
Theorem	topbast 7639	A topology is its own basis.
|- (J e. Top -> J e. Bases)
Theorem	tgtopt 7640	A topology is its own basis.
|- (J e. Top -> (topGen` J) = J)
Theorem	eltopt 7641	Membership in a topology, expressed without quantifiers.
|- (J e. Top -> (A e. J <-> A (_ U.(J i^i P~A)))
Theorem	eltop2t 7642	Membership in a topology.
|- (J e. Top -> (A e. J <-> (A (_ U.J /\ A.x e. A E.y e. J (x e. y /\ y (_ A))))
Theorem	eltop3t 7643	Membership in a topology.
|- (J e. Top -> (A e. J <-> E.x(x (_ J /\ A = U.x)))
Theorem	tgidmt 7644	The topology generator function is idempotent.
|- (B e. Bases -> (topGen` (topGen` B)) = (topGen` B))
Theorem	bastopt 7645	Two ways to express that a basis is a topology.
|- (B e. Bases -> (B e. Top <-> (topGen` B) = B))
Theorem	tgtop11t 7646	The topology generation function is one-to-one when applied to completed topologies.
|- ((J e. Top /\ K e. Top /\ (topGen` J) = (topGen` K)) -> J = K)
Theorem	0top 7647	The singleton of the empty set is the only topology possible for an empty underlying set.
|- (J e. Top -> (U.J = (/) <-> J = {(/)}))
Theorem	tgsst 7648	Subset relation for generated topologies.
|- ((B e. Bases /\ C e. Bases /\ B (_ C) -> (topGen` B) (_ (topGen` C))
Theorem	tgss2t 7649	A criterion for determining whether one topology is finer than another, based on a comparison of their bases. Lemma 2.2 of [Munkres] p. 80.
|- ((B e. Bases /\ C e. Bases /\ U.B = U.C) -> ((topGen` B) (_ (topGen` C) <-> A.x e. U.BA.y e. B (x e. y -> E.z e. C (x e. z /\ z (_ y))))
Theorem	tgss3t 7650	A criterion for determining whether one topology is finer than another. Lemma 2.2 of [Munkres] p. 80 using abbreviations.
|- ((B e. Bases /\ C e. Bases /\ U.B = U.C) -> ((topGen` B) (_ (topGen` C) <-> A.x e. B (U.B i^i x) (_ U.(C i^i P~x)))
Theorem	basgen2t 7651	Given a topology J, show that a subset B satisfying the third antecedent is a basis for it. Lemma 2.3 of [Munkres] p. 81.
|- ((J e. Top /\ B (_ J /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z (_ x)) -> (B e. Bases /\ (topGen` B) = J))
Theorem	basgent 7652	Given a topology J, show that a subset B satisfying the third antecedent is a basis for it. Lemma 2.3 of [Munkres] p. 81 using abbreviations.
|- ((J e. Top /\ B (_ J /\ A.x e. J x (_ U.(B i^i P~x)) -> (B e. Bases /\ (topGen` B) = J))
Theorem	2basgent 7653	Conditions that determine the equality of two generated topologies.
|- (((B e. Bases /\ C e. Bases) /\ (B (_ C /\ C (_ (topGen` B))) -> (topGen` B) = (topGen` C))
Theorem	bastop 7654	A subset of a topology is a basis for the topology iff every member of the topology is a union of members of the basis. We use the idiom "B e. Bases /\ (topGen` B) = J" to express "B is a basis for topology J," since we do not have a separate notation for this. Definition 15.35 of [Schechter] p. 428.
|- ((J e. Top /\ B (_ J) -> ((B e. Bases /\ (topGen` B) = J) <-> A.x e. J E.y(y (_ B /\ x = U.y)))
Theorem	bastop2 7655	A version of bastop 7654 that doesn't have B (_ J in the antecedent.
|- (