mmtheorems104 - 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-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17411

Statement List for Metamath Proof Explorer - 10301-10400 - Page 104 of 175

Type	Label	Description
Statement
Theorem	flimnei 10301	A filter contains all of the neighborhoods of its limit points. (Contributed by Jeff Hankins, 4-Sep-2009.)
|- X = U.J   &   |- Y = U.F   =>   |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fLim1` J)` F) /\ N e. ((nei` J)` {A})) -> N e. F)
Theorem	neifil 10302	The neighborhoods of a non empty set is a filter. Bourbaki TG I.36, example 2. (Contributed by FL, 19-Sep-2007.)
|- X = U.J   =>   |- ((J e. Top /\ S C_ X /\ S =/= (/)) -> ((nei` J)` S) e. Fil)
Theorem	hausfillim 10303	A condition for a topology to be Hausdorff in terms of filters. A topology is Hausdorff iff every filter has at most one limit point. (Contributed by Jeff Hankins, 5-Sep-2009.)
|- X = U.J   =>   |- (J e. Top -> (J e. Haus <-> A.f e. Fil (X = U.f -> E*x x e. ((fLim1` J)` f))))
Syntax	cfilmap 10304	Extend class definition to include the neighborhood filter mapping function.
class FilMap
Syntax	cflimf 10305	Extend class definition to include the function for filter-based function limits.
class fLimf
Definition	df-filmap 10306	Define a function that takes a filter to a neighborhood filter of the range. (Contributed by Jeff Hankins, 5-Sep-2009.)
|- FilMap = {<.<.x, y>., z>. | (y e. fBas /\ z = {<.f, s>. | (f:U.y-->x /\ s = (filGen` ({w | E.t e. y w = (f"t)} u. {x})))})}
Theorem	filmapf 10307	Given a function from a filtered set to a topology, return the filter of supersets of images of filter elements. (Contributed by Jeff Hankins, 5-Sep-2009.)
|- Y = U.B   =>   |- ((X e. A /\ B e. fBas) -> (X FilMap B) = {<.f, s>. | (f:Y-->X /\ s = (filGen` ({w | E.t e. B w = (f"t)} u. {X})))})
Theorem	isfilmap 10308	Introduce a function that takes a function from a filtered domain to a set and produces a filter which consists of supersets of images of filter elements. The functions which are dealt with by this function are similar to nets in topology. For example, suppose we have a sequence filtered by the filter generated by its tails under the usual natural number ordering. Then the elements of this filter are precisely the supersets of tails of this sequence. Under this definition, it is not too difficult to see that the limit of a function in the filter sense captures the notion of convergence of a sequence. As a result, the notion of a filter generalizes many ideas associated with sequences, and this function is one way to make that relationship precise in Metamath. (Contributed by Jeff Hankins, 5-Sep-2009.)
|- Y = U.B   =>   |- ((X e. A /\ B e. fBas /\ F:Y-->X) -> ((X FilMap B)` F) = (filGen` ({w | E.t e. B w = (F"t)} u. {X})))
Theorem	filmapss 10309	A finer filter produces a finer image filter. (Contributed by Jeff Hankins, 16-Nov-2009.)
|- Y = U.B   &   |- Z = U.C   =>   |- (((X e. A /\ B e. fBas /\ C e. fBas) /\ (F:Y-->X /\ Y = Z /\ B C_ C)) -> ((X FilMap B)` F) C_ ((X FilMap C)` F))
Theorem	fmf 10310	A mapping filter is a filter. (Contributed by Jeff Hankins, 18-Sep-2009.)
|- Y = U.B   =>   |- ((X e. A /\ B e. fBas /\ F:Y-->X) -> ((X FilMap B)` F) e. Fil)
Theorem	fmbas 10311	The base set of a mapping filter is the first argument. (Contributed by Jeff Hankins, 18-Sep-2009.)
|- Y = U.B   =>   |- ((X e. A /\ B e. fBas /\ F:Y-->X) -> U.((X FilMap B)` F) = X)
Theorem	elfilmap 10312	An element of a mapping filter. (Contributed by Jeff Hankins, 8-Sep-2009.)
|- Y = U.B   =>   |- ((X e. C /\ B e. fBas /\ F:Y-->X) -> (A e. ((X FilMap B)` F) <-> (A C_ X /\ E.x e. B (F"x) C_ A)))
Theorem	elfilmap2 10313	An element of a mapping filter. (Contributed by Jeff Hankins, 26-Sep-2009.)
|- Y = U.B   &   |- L = (filGen` B)   =>   |- ((X e. C /\ B e. fBas /\ F:Y-->X) -> (A e. ((X FilMap B)` F) <-> (A C_ X /\ E.x e. L (F"x) C_ A)))
Theorem	elfilmap3 10314	An alternate formulation of elementhood in a mapping filter that requires F to be onto. (Contributed by Jeff Hankins, 1-Oct-2009.)
|- Y = U.B   &   |- L = (filGen` B)   =>   |- ((B e. fBas /\ F:Y-onto->X) -> (A e. ((X FilMap B)` F) <-> E.x e. L A = (F"x)))
Theorem	fbfgfmeq 10315	The image filter of a filter base is the same as the image filter of its generated filter. (Contributed by Jeff Hankins, 18-Nov-2009.)
|- Y = U.B   &   |- L = (filGen` B)   =>   |- ((X e. C /\ B e. fBas /\ F:Y-->X) -> ((X FilMap B)` F) = ((X FilMap L)` F))
Definition	df-flimf 10316	Define a function that gives the limits of a function f in the filter sense. (Contributed by Jeff Hankins, 5-Sep-2009.)
|- fLimf = {<.<.x, y>., z>. | (x e. Top /\ y e. Fil /\ z = {<.f, s>. | (f:U.y-->U.x /\ s = ((fLim1` x)` ((U.x FilMap y)` f)))})}
Theorem	flimff 10317	Given a topology and a filtered set, return the convergence function on the functions from the filtered set to the base set of the topological space. (Contributed by Jeff Hankins, 14-Oct-2009.)
|- X = U.J   &   |- Y = U.F   =>   |- ((J e. Top /\ F e. Fil) -> (J fLimf F) = {<.f, s>. | (f:Y-->X /\ s = ((fLim1` J)` ((X FilMap F)` f)))})
Theorem	sflimf 10318	Given a function from a filtered set to a topological space, define the set of limit points of the function. (Contributed by Jeff Hankins, 8-Nov-2009.)
|- X = U.J   &   |- Y = U.L   =>   |- ((J e. Top /\ L e. Fil /\ F:Y-->X) -> ((J fLimf L)` F) = ((fLim1` J)` ((X FilMap L)` F)))
Theorem	flimfnei 10319	The property of being a limit point of a function in terms of neighborhoods. (Contributed by Jeff Hankins, 9-Nov-2009.)
|- X = U.J   &   |- Y = U.L   =>   |- ((J e. Top /\ L e. Fil /\ F:Y-->X) -> (A e. ((J fLimf L)` F) <-> (A e. X /\ A.n e. ((nei` J)` {A})E.s e. L (F"s) C_ n)))
Theorem	flimfneii 10320	A neighborhood of a limit point of a function contains the image of a filter element. (Contributed by Jeff Hankins, 11-Nov-2009.)
|- X = U.J   &   |- Y = U.L   =>   |- (((J e. Top /\ L e. Fil /\ F:Y-->X) /\ A e. ((J fLimf L)` F) /\ N e. ((nei` J)` {A})) -> E.s e. L (F"s) C_ N)
Theorem	flimopn 10321	The condition for being a limit point of a filter still holds if one only considers open neighborhoods. (Contributed by Jeff Hankins, 4-Sep-2009.)
|- X = U.J   &   |- Y = U.F   =>   |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) -> (A e. ((fLim1` J)` F) <-> A.o e. J (A e. o -> o e. F)))
Theorem	fbaslim 10322	A condition for a filter to converge to a point involving one of its bases. (Contributed by Jeff Hankins, 4-Sep-2009.)
|- X = U.J   &   |- Y = U.B   &   |- F = (filGen` B)   =>   |- (((J e. Top /\ B e. fBas /\ X = Y) /\ A e. X) -> (A e. ((fLim1` J)` F) <-> A.o e. J (A e. o -> E.x e. B x C_ o)))
Theorem	isflimf 10323	The property of being a limit point of a function. (Contributed by Jeff Hankins, 8-Nov-2009.)
|- X = U.J   &   |- Y = U.L   =>   |- ((J e. Top /\ L e. Fil /\ F:Y-->X) -> (A e. ((J fLimf L)` F) <-> (A e. X /\ A.o e. J (A e. o -> E.s e. L (F"s) C_ o))))
Theorem	flimfelbas 10324	A limit point of a function is in the topological space. (Contributed by Jeff Hankins, 10-Nov-2009.)
|- X = U.J   &   |- Y = U.L   =>   |- (((J e. Top /\ L e. Fil /\ F:Y-->X) /\ A e. ((J fLimf L)` F)) -> A e. X)
Theorem	hausfillim2 10325	A condition for a topology to be Hausdorff in terms of filters. A topology is Hausdorff iff every filter has at most one limit point. (Contributed by FL, 6-Dec-2010.)
|- X = U.J   =>   |- ((J e. Haus /\ F e. Fil /\ X = U.F) -> E*x x e. ((fLim1` J)` F))
Theorem	holimf 10326	If a function has its values in a Hausdorff space then it has at most one limit value. (Contributed by FL, 6-Dec-2010.)
|- Y = U.L   &   |- X = U.J   =>   |- ((L e. Fil /\ J e. Haus /\ F:Y-->X) -> E*x x e. ((J fLimf L)` F))
Theorem	holimf2 10327	If a convergent function has its values in a Hausdorff space then it has only one limit value. (Contributed by FL, 6-Dec-2010.)
|- Y = U.L   &   |- X = U.J   =>   |- (((L e. Fil /\ J e. Haus /\ F:Y-->X) /\ ((J fLimf L)` F) =/= (/)) -> E!x x e. ((J fLimf L)` F))
Compactness
Syntax	ccomp 10328	Extend class notation with the class of all compact spaces.
class Comp
Definition	df-comp 10329	Definition of a compact topology. A topology is compact iff any open covering of its underlying set contains a finite sub-covering (Heine-Borel property). Bourbaki TG I.59 prop C''' . Note: Bourbaki uses the term quasi-compact topology but it is not the modern usage (which we follow). (Contributed by FL, 22-Dec-2008.)
|- Comp = {x e. Top | A.y e. ~P x(U.x = U.y -> E.z e. (~Py i^i Fin)U.x = U.z)}
Theorem	iscomp 10330	The predicate "is a compact topology". (Contributed by FL, 22-Dec-2008.)
|- (J e. Comp <-> (J e. Top /\ A.y e. ~P J(U.J = U.y -> E.z e. (~Py i^i Fin)U.J = U.z)))
Theorem	cncomp 10331	Compactness is respected by a continuous onto map. (Contributed by Jeff Hankins, 12-Jul-2009.)
|- X = U.J   &   |- Y = U.K   =>   |- (((J e. Comp /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) -> K e. Comp)
Theorem	comptoppr 10332	Compactness is a topological property-that is, for any two homeomorphic topologies, either both are compact or neither is. (Contributed by Jeff Hankins, 30-Jun-2009.)
|- ((J e. Top /\ K e. Top /\ J ~= K) -> (J e. Comp <-> K e. Comp))
Theorem	fintopcomp 10333	A finite topology is compact. (Contributed by FL, 22-Dec-2008.)
|- (J e. (Top i^i Fin) -> J e. Comp)
Separated spaces: T0, T1, T2 (Hausdorff) ...
Syntax	ct1 10334	Extend class notation to include T1-spaces.
class Fre
Definition	df-t1 10335	The class of all T1-spaces also called Frechet spaces. Morris, Topology without tears, p. 30 ex. 3. (Contributed by FL, 18-Jun-2007.)
|- Fre = {x e. Top | A.a e. U.x{a} e. (Clsd` x)}
Theorem	ist1 10336	The predicate J is T1. (Contributed by FL, 18-Jun-2007.)
|- X = U.J   =>   |- (J e. Fre <-> (J e. Top /\ A.a e. X {a} e. (Clsd` J)))
Connectedness
Syntax	ccon 10337	Extend class notation with the the class of all connected topologies.
class Con
Definition	df-con 10338	Topologies are connected when only (/) and U.j are both open and closed.
|- Con = {j e. Top | (j i^i (Clsd` j)) = {(/), U.j}}
Theorem	iscon 10339	The predicate J is a connected topology . (Contributed by FL, 17-Nov-2008.)
|- (J e. Top -> (J e. Con <-> (J i^i (Clsd` J)) = {(/), U.J}))
Theorem	iscon2 10340	The predicate J is a connected topology . (Contributed by FL, 17-Nov-2008.)
|- (J e. Con <-> (J e. Top /\ (J i^i (Clsd` J)) = {(/), U.J}))
Theorem	usinuniop 10341	If a topology is connected, its underlying set can't be partitioned into two non empty non-overlapping open sets. (Contributed by FL, 17-Nov-2008.)
|- X = U.J   =>   |- (J e. Con -> A.x e. J A.y e. J ((x =/= (/) /\ y =/= (/) /\ (x i^i y) = (/)) -> X =/= (x u. y)))
Theorem	contop 10342	A connected topology is a topology. (Contributed by FL, 22-Dec-2008.)
|- Con C_ Top
Planar incidence geometry
Syntax	cplig 10343	Extend class notation with the class of all planar incidence geometries.
class Plig
Definition	df-plig 10344	Planar incidence geometry. I use Hilbert's "axioms" adapted to planar geometry. e. is the incidence relation. I could take a generic incidence relation but I'm lazy and I'm not sure the gain is worth the extra work. Much of what follows is directly borrowed from Aitken. http://public.csusm.edu/aitken_html/m410/betweenness.pdf (Contributed by FL, 2-Aug-2009.)
|- Plig = {x | (A.a e. U.xA.b e. U.x(a =/= b -> E!l e. x (a e. l /\ b e. l)) /\ A.l e. x E.a e. U.xE.b e. U.x(a =/= b /\ a e. l /\ b e. l) /\ E.a e. U.xE.b e. U.xE.c e. U.xA.l e. x -. (a e. l /\ b e. l /\ c e. l))}
Theorem	isplig 10345	The predicate "is a planar incidence geometry". (Contributed by FL, 2-Aug-2009.)
|- P = U.L   =>   |- (L e. A -> (L e. Plig <-> (A.a e. P A.b e. P (a =/= b -> E!l e. L (a e. l /\ b e. l)) /\ A.l e. L E.a e. P E.b e. P (a =/= b /\ a e. l /\ b e. l) /\ E.a e. P E.b e. P E.c e. P A.l e. L -. (a e. l /\ b e. l /\ c e. l))))
Theorem	tncp 10346	There exist three non colinear points. (Contributed by FL, 3-Aug-2009.)
|- P = U.L   =>   |- (L e. Plig -> E.a e. P E.b e. P E.c e. P A.l e. L -. (a e. l /\ b e. l /\ c e. l))
Theorem	lpni 10347	For any line, there exists a point not on the line. (Contributed by Jeff Hankins, 15-Aug-2009.)
|- P = U.G   =>   |- ((G e. Plig /\ L e. G) -> E.a e. P a e/ L)
Directed sets, nets
Syntax	cdir 10348	Extend class notation with the class of all directed sets.
class Dir
Syntax	ctail 10349	Extend class notation with the tail function.
class tail
Definition	df-dir 10350	Define the class of all directed sets/directions.
|- Dir = {d | ((Rel d /\ ( _I |` U.U.d) C_ d) /\ ((d o. d) C_ d /\ A.x e. U.U.dA.y e. U.U.dE.z e. U.U.d(xdz /\ ydz)))}
Definition	df-tail 10351	Define the tail function for directed sets.
|- tail = {<.x, y>. | (x e. Dir /\ y = {<.z, w>. | (z e. U.U.x /\ w = {t | zxt})})}
Theorem	isdir 10352	A condition for a relation to be a direction. (Contributed by Jeff Hankins, 25-Nov-2009.) )
|- A = U.U.D   =>   |- (D e. B -> (D e. Dir <-> ((Rel D /\ ( _I |` A) C_ D) /\ ((D o. D) C_ D /\ A.x e. A A.y e. A E.z e. A (xDz /\ yDz)))))
Theorem	reldir 10353	A direction is a relation. (Contributed by Jeff Hankins, 25-Nov-2009.)
|- (D e. Dir -> Rel D)
Theorem	dirdm 10354	A direction's domain is equal to its field. (Contributed by Jeff Hankins, 25-Nov-2009.)
|- (D e. Dir -> dom D = U.U.D)
Theorem	dirref 10355	A direction is reflexive. (Contributed by Jeff Hankins, 25-Nov-2009.)
|- X = dom D   =>   |- ((D e. Dir /\ A e. X) -> ADA)
Theorem	dirtr 10356	A direction is transitive. (Contributed by Jeff Hankins, 25-Nov-2009.)
|- (((D e. Dir /\ C e. H) /\ (ADB /\ BDC)) -> ADC)
Theorem	dirge 10357	For any two elements of a directed set, there exists a third element greater than or equal to both. (Note that this does not say that the two elements have a least upper bound.) (Contributed by Jeff Hankins, 25-Nov-2009.)
|- X = dom D   =>   |- ((D e. Dir /\ A e. X /\ B e. X) -> E.x e. X (ADx /\ BDx))
Theorem	tosdir 10358	A totally ordered set is a directed set. (Contributed by Jeff Hankins, 25-Nov-2009.)
|- Toset C_ Dir
Operation properties
Syntax	cass 10359	Extend class notation with a device to add associativity to internal operations.
class Ass
Definition	df-ass 10360	A device to add associativity to various sorts of internal operations. The definition is meaningful when g is a magma at least.
|- Ass = {g | A.x e. dom dom gA.y e. dom dom gA.z e. dom dom g((xgy)gz) = (xg(ygz))}
Syntax	cexid 10361	Extend class notation with the class of all the internal operations with an identity element.
class ExId
Definition	df-exid 10362	A device to add an identity element to various sorts of internal operations.
|- ExId = {g | E.x e. dom dom gA.y e. dom dom g((ygx) = y /\ (xgy) = y)}
Theorem	isass 10363	The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009.)
|- X = dom dom G   =>   |- (G e. A -> (G e. Ass <-> A.x e. X A.y e. X A.z e. X ((xGy)Gz) = (xG(yGz))))
Theorem	isexid 10364	The predicate G has a left and right identity element. (Contributed by FL, 2-Nov-2009.)
|- X = dom dom G   =>   |- (G e. A -> (G e. ExId <-> E.x e. X A.y e. X ((yGx) = y /\ (xGy) = y)))
Groups and related structures
Syntax	cmagm 10365	Extend class notation with the class of all magmas.
class Magma
Definition	df-mgm 10366	A magma is a binary internal operation.
|- Magma = {g | E.t g:(t X. t)-->t}
Theorem	ismgm 10367	The predicate "is a magma". (Contributed by FL, 2-Nov-2009.)
|- X = dom dom G   =>   |- (G e. A -> (G e. Magma <-> G:(X X. X)-->X))
Theorem	clmgm 10368	Closure of a magma. (Contributed by FL, 14-Sep-2010.)
|- X = dom dom G   =>   |- ((G e. Magma /\ A e. X /\ B e. X) -> (AGB) e. X)
Theorem	opidon 10369	An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009.)
|- X = dom dom G   =>   |- (G e. (Magma i^i ExId ) -> G:(X X. X)-onto->X)
Theorem	rngopid 10370	Range of an operation with a left and right identity element. (Contributed by FL, 2-Nov-2009.)
|- (G e. (Magma i^i ExId ) -> ran G = dom dom G)
Theorem	opidon2 10371	An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009.)
|- X = ran G   =>   |- (G e. (Magma i^i ExId ) -> G:(X X. X)-onto->X)
Theorem	isexid2 10372	If G e. (Magma i^i ExId ) then it has a left and right identity element that belongs to the range of the operation. (Contributed by FL, 12-Dec-2009.)
|- X = ran G   =>   |- (G e. (Magma i^i ExId ) -> E.u e. X A.y e. X ((yGu) = y /\ (uGy) = y))
Theorem	exidu1 10373	Unicity of the left and right identity element of a magma when it exists. (Contributed by FL, 12-Dec-2009.)
|- X = ran G   =>   |- (G e. (Magma i^i ExId ) -> E!u e. X A.x e. X ((uGx) = x /\ (xGu) = x))
Theorem	idrval 10374	The value of the identity element. (Contributed by FL, 12-Dec-2009.)
|- X = ran G   &   |- U = (Id` G)   =>   |- (G e. A -> U = U.{u e. X | A.x e. X ((uGx) = x /\ (xGu) = x)})
Theorem	iorlid 10375	A magma right and left identity belongs to the underlying set of the operation. (Contributed by FL, 12-Dec-2009.)
|- X = ran G   &   |- U = (Id` G)   =>   |- (G e. (Magma i^i ExId ) -> U e. X)
Theorem	cmpidelt 10376	A magma right and left identity element keeps the other elements unchanged. (Contributed by FL, 12-Dec-2009.)
|- X = ran G   &   |- U = (Id` G)   =>   |- ((G e. (Magma i^i ExId ) /\ A e. X) -> ((UGA) = A /\ (AGU) = A))
Syntax	csem 10377	Extend class notation with the class of all semi-groups.
class SemiGrp
Definition	df-sgr 10378	A semi-group is an associative magma.
|- SemiGrp = (Magma i^i Ass)
Theorem	smgrpismgm 10379	A semi-group is a magma. (Contributed by FL, 2-Nov-2009.)
|- (G e. SemiGrp -> G e. Magma)
Theorem	smgrpisass 10380	A semi-group is associative. (Contributed by FL, 2-Nov-2009.)
|- (G e. SemiGrp -> G e. Ass)
Theorem	issmgrp 10381	The predicate "is a semi-group". (Contributed by FL, 2-Nov-2009.)
|- X = dom dom G   =>   |- (G e. A -> (G e. SemiGrp <-> (G:(X X. X)-->X /\ A.x e. X A.y e. X A.z e. X ((xGy)Gz) = (xG(yGz)))))
Theorem	smgrpmgm 10382	A semi-group is a magma. (Contributed by FL, 2-Nov-2009.)
|- X = dom dom G   =>   |- (G e. SemiGrp -> G:(X X. X)-->X)
Theorem	smgrpass 10383	A semi-group is associative. (Contributed by FL, 2-Nov-2009.)
|- X = dom dom G   =>   |- (G e. SemiGrp -> A.x e. X A.y e. X A.z e. X ((xGy)Gz) = (xG(yGz)))
Syntax	cmnd 10384	Extend class notation with the class of all monoids.
class Mnd
Definition	df-mnd 10385	A monoid is a semi-group with an identity element.
|- Mnd = (SemiGrp i^i ExId )
Theorem	mndissmgrp 10386	A monoid is a semi-group. (Contributed by FL, 2-Nov-2009.)
|- (G e. Mnd -> G e. SemiGrp)
Theorem	mndisexid 10387	A monoid has an identity element. (Contributed by FL, 2-Nov-2009.)
|- (G e. Mnd -> G e. ExId )
Theorem	mndismgm 10388	A monoid is a magma. (Contributed by FL, 2-Nov-2009.)
|- (G e. Mnd -> G e. Magma)
Theorem	mndmgmid 10389	A monoid is a magma with an identity element. (Contributed by FL, 18-Feb-2010.)
|- (G e. Mnd -> G e. (Magma i^i ExId ))
Theorem	ismnd 10390	The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.)
|- X = dom dom G   =>   |- (G e. A -> (G e. Mnd <-> (G e. SemiGrp /\ E.x e. X A.y e. X ((yGx) = y /\ (xGy) = y))))
Theorem	ismnd1 10391	The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.)
|- X = dom dom G   =>   |- (G e. A -> (G e. Mnd <-> (G:(X X. X)-->X /\ A.x e. X A.y e. X A.z e. X ((xGy)Gz) = (xG(yGz)) /\ E.x e. X A.y e. X ((yGx) = y /\ (xGy) = y))))
Theorem	ismnd2 10392	The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.)
|- X = ran G   =>   |- (G e. A -> (G e. Mnd <-> (G:(X X. X)-->X /\ A.x e. X A.y e. X A.z e. X ((xGy)Gz) = (xG(yGz)) /\ E.x e. X A.y e. X ((yGx) = y /\ (xGy) = y))))
Theorem	grpmnd 10393	A group is a monoid. (Contributed by FL, 2-Nov-2009.)
|- (G e. Grp -> G e. Mnd)
Fields and Rings
Syntax	ccm2 10394	Extend class notation with a class that adds commutativity to various flavors of rings.
class Com2
Definition	df-com2 10395	A device to add commutativity to various sorts of rings. I use ran g because I suppose g has a neutral element and therefore is onto.
|- Com2 = {<.g, h>. | A.a e. ran gA.b e. ran g(ahb) = (bha)}
Theorem	iscom2 10396	A device to add commutativity to various sorts of rings. (Contributed by FL, 6-Sep-2009.)
|- ((G e. A /\ H e. B) -> (<.G, H>. e. Com2 <-> A.a e. ran GA.b e. ran G(aHb) = (bHa)))
Syntax	cfld 10397	Extend class notation with the class of all fields.
class Fld
Definition	df-fld 10398	Definition of a field. A field is a commutative division ring.
|- Fld = (DivRing i^i Com2)
Theorem	relrng 10399	The class of all unital rings is a relation. (Contributed by FL, 31-Aug-2009.)
|- Rel Ring
Theorem	rngn0 10400	The base set of a ring is not empty. (Contributed by FL, 24-Jan-2010.)
|- G = (1st` R)   &   |- X = ran G   =>   |- (R e. Ring -> X =/= (/))