P. 160 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 15901-16000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ipoval 15901*	Value of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- I = (toInc ` F )   &    |- .<_ = { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) }   =>    |- ( F e. V -> I = ( { <. ( Base ` ndx ) , F >. , <. (TopSet ` ndx ) , (ordTop ` .<_ ) >. } u. { <. ( le ` ndx ) , .<_ >. , <. ( oc ` ndx ) , ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) >. } ) )
Theorem	ipobas 15902	Base set of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Revised by Mario Carneiro, 25-Oct-2015.)
|- I = (toInc ` F )   =>    |- ( F e. V -> F = ( Base ` I ) )
Theorem	ipolerval 15903*	Relation of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- I = (toInc ` F )   =>    |- ( F e. V -> { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } = ( le ` I ) )
Theorem	ipotset 15904	Topology of the inclusion poset. (Contributed by Mario Carneiro, 24-Oct-2015.)
|- I = (toInc ` F )   &    |- .<_ = ( le ` I )   =>    |- ( F e. V -> (ordTop ` .<_ ) = (TopSet ` I ) )
Theorem	ipole 15905	Weak order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- I = (toInc ` F )   &    |- .<_ = ( le ` I )   =>    |- ( ( F e. V /\ X e. F /\ Y e. F ) -> ( X .<_ Y <-> X C_ Y ) )
Theorem	ipolt 15906	Strict order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- I = (toInc ` F )   &    |- .< = ( lt ` I )   =>    |- ( ( F e. V /\ X e. F /\ Y e. F ) -> ( X .< Y <-> X C. Y ) )
Theorem	ipopos 15907	The inclusion poset on a family of sets is actually a poset. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- I = (toInc ` F )   =>    |- I e. Poset
Theorem	isipodrs 15908*	Condition for a family of sets to be directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.)
|- ( (toInc ` A ) e. Dirset <-> ( A e. _V /\ A =/= (/) /\ A. x e. A A. y e. A E. z e. A ( x u. y ) C_ z ) )
Theorem	ipodrscl 15909	Direction by inclusion as used here implies sethood. (Contributed by Stefan O'Rear, 2-Apr-2015.)
|- ( (toInc ` A ) e. Dirset -> A e. _V )
Theorem	ipodrsfi 15910*	Finite upper bound property for directed collections of sets. (Contributed by Stefan O'Rear, 2-Apr-2015.)
|- ( ( (toInc ` A ) e. Dirset /\ X C_ A /\ X e. Fin ) -> E. z e. A U. X C_ z )
Theorem	fpwipodrs 15911	The finite subsets of any set are directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.)
|- ( A e. V -> (toInc ` ( ~P A i^i Fin ) ) e. Dirset )
Theorem	ipodrsima 15912*	The monotone image of a directed set. (Contributed by Stefan O'Rear, 2-Apr-2015.)
|- ( ph -> F Fn ~P A )   &    |- ( ( ph /\ ( u C_ v /\ v C_ A ) ) -> ( F ` u ) C_ ( F ` v ) )   &    |- ( ph -> (toInc ` B ) e. Dirset )   &    |- ( ph -> B C_ ~P A )   &    |- ( ph -> ( F " B ) e. V )   =>    |- ( ph -> (toInc ` ( F " B ) ) e. Dirset )
Theorem	isacs3lem 15913*	An algebraic closure system satisfies isacs3 15921. (Contributed by Stefan O'Rear, 2-Apr-2015.)
|- ( C e. (ACS ` X ) -> ( C e. (Moore ` X ) /\ A. s e. ~P C ( (toInc ` s ) e. Dirset -> U. s e. C ) ) )
Theorem	acsdrsel 15914	An algebraic closure system contains all directed unions of closed sets. (Contributed by Stefan O'Rear, 2-Apr-2015.)
|- ( ( C e. (ACS ` X ) /\ Y C_ C /\ (toInc ` Y ) e. Dirset ) -> U. Y e. C )
Theorem	isacs4lem 15915*	In a closure system in which directed unions of closed sets are closed, closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.)
|- F = (mrCls ` C )   =>    |- ( ( C e. (Moore ` X ) /\ A. s e. ~P C ( (toInc ` s ) e. Dirset -> U. s e. C ) ) -> ( C e. (Moore ` X ) /\ A. t e. ~P ~P X ( (toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) )
Theorem	isacs5lem 15916*	If closure commutes with directed unions, then the closure of a set is the closure of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.)
|- F = (mrCls ` C )   =>    |- ( ( C e. (Moore ` X ) /\ A. t e. ~P ~P X ( (toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) -> ( C e. (Moore ` X ) /\ A. s e. ~P X ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) )
Theorem	acsdrscl 15917	In an algebraic closure system, closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.)
|- F = (mrCls ` C )   =>    |- ( ( C e. (ACS ` X ) /\ Y C_ ~P X /\ (toInc ` Y ) e. Dirset ) -> ( F ` U. Y ) = U. ( F " Y ) )
Theorem	acsficl 15918	A closure in an algebraic closure system is the union of the closures of finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.)
|- F = (mrCls ` C )   =>    |- ( ( C e. (ACS ` X ) /\ S C_ X ) -> ( F ` S ) = U. ( F " ( ~P S i^i Fin ) ) )
Theorem	isacs5 15919*	A closure system is algebraic iff the closure of a generating set is the union of the closures of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.)
|- F = (mrCls ` C )   =>    |- ( C e. (ACS ` X ) <-> ( C e. (Moore ` X ) /\ A. s e. ~P X ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) )
Theorem	isacs4 15920*	A closure system is algebraic iff closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.)
|- F = (mrCls ` C )   =>    |- ( C e. (ACS ` X ) <-> ( C e. (Moore ` X ) /\ A. s e. ~P ~P X ( (toInc ` s ) e. Dirset -> ( F ` U. s ) = U. ( F " s ) ) ) )
Theorem	isacs3 15921*	A closure system is algebraic iff directed unions of closed sets are closed. (Contributed by Stefan O'Rear, 2-Apr-2015.)
|- ( C e. (ACS ` X ) <-> ( C e. (Moore ` X ) /\ A. s e. ~P C ( (toInc ` s ) e. Dirset -> U. s e. C ) ) )
Theorem	acsficld 15922	In an algebraic closure system, the closure of a set is the union of the closures of its finite subsets. Deduction form of acsficl 15918. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (ACS ` X ) )   &    |- N = (mrCls ` A )   &    |- ( ph -> S C_ X )   =>    |- ( ph -> ( N ` S ) = U. ( N " ( ~P S i^i Fin ) ) )
Theorem	acsficl2d 15923*	In an algebraic closure system, an element is in the closure of a set if and only if it is in the closure of a finite subset. Alternate form of acsficl 15918. Deduction form. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (ACS ` X ) )   &    |- N = (mrCls ` A )   &    |- ( ph -> S C_ X )   =>    |- ( ph -> ( Y e. ( N ` S ) <-> E. x e. ( ~P S i^i Fin ) Y e. ( N ` x ) ) )
Theorem	acsfiindd 15924	In an algebraic closure system, a set is independent if and only if all its finite subsets are independent. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (ACS ` X ) )   &    |- N = (mrCls ` A )   &    |- I = (mrInd ` A )   &    |- ( ph -> S C_ X )   =>    |- ( ph -> ( S e. I <-> ( ~P S i^i Fin ) C_ I ) )
Theorem	acsmapd 15925*	In an algebraic closure system, if T is contained in the closure of S, there is a map f from T into the set of finite subsets of S such that the closure of U. ran f contains T. This is proven by applying acsficl2d 15923 to each element of T. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (ACS ` X ) )   &    |- N = (mrCls ` A )   &    |- ( ph -> S C_ X )   &    |- ( ph -> T C_ ( N ` S ) )   =>    |- ( ph -> E. f ( f : T --> ( ~P S i^i Fin ) /\ T C_ ( N ` U. ran f ) ) )
Theorem	acsmap2d 15926*	In an algebraic closure system, if S and T have the same closure and S is independent, then there is a map f from T into the set of finite subsets of S such that S equals the union of ran f. This is proven by taking the map f from acsmapd 15925 and observing that, since S and T have the same closure, the closure of U. ran f must contain S. Since S is independent, by mrissmrcd 15047, U. ran f must equal S. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (ACS ` X ) )   &    |- N = (mrCls ` A )   &    |- I = (mrInd ` A )   &    |- ( ph -> S e. I )   &    |- ( ph -> T C_ X )   &    |- ( ph -> ( N ` S ) = ( N ` T ) )   =>    |- ( ph -> E. f ( f : T --> ( ~P S i^i Fin ) /\ S = U. ran f ) )
Theorem	acsinfd 15927	In an algebraic closure system, if S and T have the same closure and S is infinite independent, then T is infinite. This follows from applying unirnffid 7727 to the map given in acsmap2d 15926. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (ACS ` X ) )   &    |- N = (mrCls ` A )   &    |- I = (mrInd ` A )   &    |- ( ph -> S e. I )   &    |- ( ph -> T C_ X )   &    |- ( ph -> ( N ` S ) = ( N ` T ) )   &    |- ( ph -> -. S e. Fin )   =>    |- ( ph -> -. T e. Fin )
Theorem	acsdomd 15928	In an algebraic closure system, if S and T have the same closure and S is infinite independent, then T dominates S. This follows from applying acsinfd 15927 and then applying unirnfdomd 8855 to the map given in acsmap2d 15926. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (ACS ` X ) )   &    |- N = (mrCls ` A )   &    |- I = (mrInd ` A )   &    |- ( ph -> S e. I )   &    |- ( ph -> T C_ X )   &    |- ( ph -> ( N ` S ) = ( N ` T ) )   &    |- ( ph -> -. S e. Fin )   =>    |- ( ph -> S ~<_ T )
Theorem	acsinfdimd 15929	In an algebraic closure system, if two independent sets have equal closure and one is infinite, then they are equinumerous. This is proven by using acsdomd 15928 twice with acsinfd 15927. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (ACS ` X ) )   &    |- N = (mrCls ` A )   &    |- I = (mrInd ` A )   &    |- ( ph -> S e. I )   &    |- ( ph -> T e. I )   &    |- ( ph -> ( N ` S ) = ( N ` T ) )   &    |- ( ph -> -. S e. Fin )   =>    |- ( ph -> S ~~ T )
Theorem	acsexdimd 15930*	In an algebraic closure system whose closure operator has the exchange property, if two independent sets have equal closure, they are equinumerous. See mreexfidimd 15057 for the finite case and acsinfdimd 15929 for the infinite case. This is a special case of Theorem 4.2.2 in [FaureFrolicher] p. 87. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> A e. (ACS ` X ) )   &    |- N = (mrCls ` A )   &    |- I = (mrInd ` A )   &    |- ( ph -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )   &    |- ( ph -> S e. I )   &    |- ( ph -> T e. I )   &    |- ( ph -> ( N ` S ) = ( N ` T ) )   =>    |- ( ph -> S ~~ T )
Theorem	mrelatglb 15931	Greatest lower bounds in a Moore space are realized by intersections. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- I = (toInc ` C )   &    |- G = ( glb ` I )   =>    |- ( ( C e. (Moore ` X ) /\ U C_ C /\ U =/= (/) ) -> ( G ` U ) = |^| U )
Theorem	mrelatglb0 15932	The empty intersection in a Moore space is realized by the base set. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- I = (toInc ` C )   &    |- G = ( glb ` I )   =>    |- ( C e. (Moore ` X ) -> ( G ` (/) ) = X )
Theorem	mrelatlub 15933	Least upper bounds in a Moore space are realized by the closure of the union. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- I = (toInc ` C )   &    |- F = (mrCls ` C )   &    |- L = ( lub ` I )   =>    |- ( ( C e. (Moore ` X ) /\ U C_ C ) -> ( L ` U ) = ( F ` U. U ) )
Theorem	mreclatBAD 15934*	A Moore space is a complete lattice under inclusion. (Contributed by Stefan O'Rear, 31-Jan-2015.) TODO (df-riota 6158 update): Reprove using isclat 15856 instead of the isclatBAD. hypothesis. See commented-out mreclat above.
|- I = (toInc ` C )   &    |- ( I e. CLat <-> ( I e. Poset /\ A. x ( x C_ ( Base ` I ) -> ( ( ( lub ` I ) ` x ) e. ( Base ` I ) /\ ( ( glb ` I ) ` x ) e. ( Base ` I ) ) ) ) )   =>    |- ( C e. (Moore ` X ) -> I e. CLat )
9.2.5  Distributive lattices
Theorem	latmass 15935	Lattice meet is associative. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- B = ( Base ` K )   &    |- ./\ = ( meet ` K )   =>    |- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ./\ Y ) ./\ Z ) = ( X ./\ ( Y ./\ Z ) ) )
Theorem	latdisdlem 15936*	Lemma for latdisd 15937. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   =>    |- ( K e. Lat -> ( A. u e. B A. v e. B A. w e. B ( u .\/ ( v ./\ w ) ) = ( ( u .\/ v ) ./\ ( u .\/ w ) ) -> A. x e. B A. y e. B A. z e. B ( x ./\ ( y .\/ z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) ) )
Theorem	latdisd 15937*	In a lattice, joins distribute over meets if and only if meets distribute over joins; the distributive property is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   =>    |- ( K e. Lat -> ( A. x e. B A. y e. B A. z e. B ( x .\/ ( y ./\ z ) ) = ( ( x .\/ y ) ./\ ( x .\/ z ) ) <-> A. x e. B A. y e. B A. z e. B ( x ./\ ( y .\/ z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) ) )
Syntax	cdlat 15938	The class of distributive lattices.
class DLat
Definition	df-dlat 15939*	A distributive lattice is a lattice in which meets distribute over joins, or equivalently (latdisd 15937) joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- DLat = { k e. Lat | [. ( Base ` k ) / b ]. [. ( join ` k ) / j ]. [. ( meet ` k ) / m ]. A. x e. b A. y e. b A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) }
Theorem	isdlat 15940*	Property of being a distributive lattice. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   =>    |- ( K e. DLat <-> ( K e. Lat /\ A. x e. B A. y e. B A. z e. B ( x ./\ ( y .\/ z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) ) )
Theorem	dlatmjdi 15941	In a distributive lattice, meets distribute over joins. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   =>    |- ( ( K e. DLat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ ( Y .\/ Z ) ) = ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) )
Theorem	dlatl 15942	A distributive lattice is a lattice. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- ( K e. DLat -> K e. Lat )
Theorem	odudlatb 15943	The dual of a distributive lattice is a distributive lattice and conversely. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- D = (ODual ` K )   =>    |- ( K e. V -> ( K e. DLat <-> D e. DLat ) )
Theorem	dlatjmdi 15944	In a distributive lattice, joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   =>    |- ( ( K e. DLat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .\/ ( Y ./\ Z ) ) = ( ( X .\/ Y ) ./\ ( X .\/ Z ) ) )
9.2.6  Posets and lattices as relations
Syntax	cps 15945	Extend class notation with the class of all posets.
class PosetRel
Syntax	ctsr 15946	Extend class notation with the class of all totally ordered sets.
class TosetRel
Definition	df-ps 15947	Define the class of all posets (partially ordered sets) with weak ordering (e.g. "less than or equal to" instead of "less than"). A poset is a relation which is transitive, reflexive, and antisymmetric. (Contributed by NM, 11-May-2008.)
|- PosetRel = { r | ( Rel r /\ ( r o. r ) C_ r /\ ( r i^i `' r ) = ( _I |` U. U. r ) ) }
Definition	df-tsr 15948	Define the class of all totally ordered sets. (Contributed by FL, 1-Nov-2009.)
|- TosetRel = { r e. PosetRel | ( dom r X. dom r ) C_ ( r u. `' r ) }
Theorem	isps 15949	The predicate "is a poset" i.e. a transitive, reflexive, antisymmetric relation. (Contributed by NM, 11-May-2008.)
|- ( R e. A -> ( R e. PosetRel <-> ( Rel R /\ ( R o. R ) C_ R /\ ( R i^i `' R ) = ( _I |` U. U. R ) ) ) )
Theorem	psrel 15950	A poset is a relation. (Contributed by NM, 12-May-2008.)
|- ( A e. PosetRel -> Rel A )
Theorem	psref2 15951	A poset is antisymmetric and reflexive. (Contributed by FL, 3-Aug-2009.)
|- ( R e. PosetRel -> ( R i^i `' R ) = ( _I |` U. U. R ) )
Theorem	pstr2 15952	A poset is transitive. (Contributed by FL, 3-Aug-2009.)
|- ( R e. PosetRel -> ( R o. R ) C_ R )
Theorem	pslem 15953	Lemma for psref 15955 and others. (Contributed by NM, 12-May-2008.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- ( R e. PosetRel -> ( ( ( A R B /\ B R C ) -> A R C ) /\ ( A e. U. U. R -> A R A ) /\ ( ( A R B /\ B R A ) -> A = B ) ) )
Theorem	psdmrn 15954	The domain and range of a poset equal its field. (Contributed by NM, 13-May-2008.)
|- ( R e. PosetRel -> ( dom R = U. U. R /\ ran R = U. U. R ) )
Theorem	psref 15955	A poset is reflexive. (Contributed by NM, 13-May-2008.)
|- X = dom R   =>    |- ( ( R e. PosetRel /\ A e. X ) -> A R A )
Theorem	psrn 15956	The range of a poset equals it domain. (Contributed by NM, 7-Jul-2008.)
|- X = dom R   =>    |- ( R e. PosetRel -> X = ran R )
Theorem	psasym 15957	A poset is antisymmetric. (Contributed by NM, 12-May-2008.)
|- ( ( R e. PosetRel /\ A R B /\ B R A ) -> A = B )
Theorem	pstr 15958	A poset is transitive. (Contributed by NM, 12-May-2008.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- ( ( R e. PosetRel /\ A R B /\ B R C ) -> A R C )
Theorem	cnvps 15959	The converse of a poset is a poset. In the general case ( `' R e. PosetRel -> R e. PosetRel ) is not true. See cnvpsb 15960 for a special case where the property holds. (Contributed by FL, 5-Jan-2009.) (Proof shortened by Mario Carneiro, 3-Sep-2015.)
|- ( R e. PosetRel -> `' R e. PosetRel )
Theorem	cnvpsb 15960	The converse of a poset is a poset. (Contributed by FL, 5-Jan-2009.)
|- ( Rel R -> ( R e. PosetRel <-> `' R e. PosetRel ) )
Theorem	psss 15961	Any subset of a partially ordered set is partially ordered. (Contributed by FL, 24-Jan-2010.)
|- ( R e. PosetRel -> ( R i^i ( A X. A ) ) e. PosetRel )
Theorem	psssdm2 15962	Field of a subposet. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- X = dom R   =>    |- ( R e. PosetRel -> dom ( R i^i ( A X. A ) ) = ( X i^i A ) )
Theorem	psssdm 15963	Field of a subposet. (Contributed by FL, 19-Sep-2011.) (Revised by Mario Carneiro, 9-Sep-2015.)
|- X = dom R   =>    |- ( ( R e. PosetRel /\ A C_ X ) -> dom ( R i^i ( A X. A ) ) = A )
Theorem	istsr 15964	The predicate is a toset. (Contributed by FL, 1-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- X = dom R   =>    |- ( R e. TosetRel <-> ( R e. PosetRel /\ ( X X. X ) C_ ( R u. `' R ) ) )
Theorem	istsr2 15965*	The predicate is a toset. (Contributed by FL, 1-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- X = dom R   =>    |- ( R e. TosetRel <-> ( R e. PosetRel /\ A. x e. X A. y e. X ( x R y \/ y R x ) ) )
Theorem	tsrlin 15966	A toset is a linear order. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- X = dom R   =>    |- ( ( R e. TosetRel /\ A e. X /\ B e. X ) -> ( A R B \/ B R A ) )
Theorem	tsrlemax 15967	Two ways of saying a number is less than or equal to the maximum of two others. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- X = dom R   =>    |- ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A R if ( B R C , C , B ) <-> ( A R B \/ A R C ) ) )
Theorem	tsrps 15968	A toset is a poset. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- ( R e. TosetRel -> R e. PosetRel )
Theorem	cnvtsr 15969	The converse of a toset is a toset. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- ( R e. TosetRel -> `' R e. TosetRel )
Theorem	tsrss 15970	Any subset of a totally ordered set is totally ordered. (Contributed by FL, 24-Jan-2010.) (Proof shortened by Mario Carneiro, 21-Nov-2013.)
|- ( R e. TosetRel -> ( R i^i ( A X. A ) ) e. TosetRel )
Theorem	ledm 15971	domain of <_ is RR*. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 4-May-2015.)
|- RR* = dom <_
Theorem	lern 15972	The range of <_ is RR*. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 3-Sep-2015.)
|- RR* = ran <_
Theorem	lefld 15973	The field of the 'less or equal to' relationship on the extended real. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 4-May-2015.)
|- RR* = U. U. <_
Theorem	letsr 15974	The "less than or equal to" relationship on the extended reals is a toset. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 3-Sep-2015.)
|- <_ e. TosetRel
9.2.7  Directed sets, nets
Syntax	cdir 15975	Extend class notation with the class of all directed sets.
class DirRel
Syntax	ctail 15976	Extend class notation with the tail function.
class tail
Definition	df-dir 15977	Define the class of all directed sets/directions. (Contributed by Jeff Hankins, 25-Nov-2009.)
|- DirRel = { r | ( ( Rel r /\ ( _I |` U. U. r ) C_ r ) /\ ( ( r o. r ) C_ r /\ ( U. U. r X. U. U. r ) C_ ( `' r o. r ) ) ) }
Definition	df-tail 15978*	Define the tail function for directed sets. (Contributed by Jeff Hankins, 25-Nov-2009.)
|- tail = ( r e. DirRel |-> ( x e. U. U. r |-> ( r " { x } ) ) )
Theorem	isdir 15979	A condition for a relation to be a direction. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- A = U. U. R   =>    |- ( R e. V -> ( R e. DirRel <-> ( ( Rel R /\ ( _I |` A ) C_ R ) /\ ( ( R o. R ) C_ R /\ ( A X. A ) C_ ( `' R o. R ) ) ) ) )
Theorem	reldir 15980	A direction is a relation. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- ( R e. DirRel -> Rel R )
Theorem	dirdm 15981	A direction's domain is equal to its field. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- ( R e. DirRel -> dom R = U. U. R )
Theorem	dirref 15982	A direction is reflexive. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- X = dom R   =>    |- ( ( R e. DirRel /\ A e. X ) -> A R A )
Theorem	dirtr 15983	A direction is transitive. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- ( ( ( R e. DirRel /\ C e. V ) /\ ( A R B /\ B R C ) ) -> A R C )
Theorem	dirge 15984*	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.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- X = dom R   =>    |- ( ( R e. DirRel /\ A e. X /\ B e. X ) -> E. x e. X ( A R x /\ B R x ) )
Theorem	tsrdir 15985	A totally ordered set is a directed set. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- ( A e. TosetRel -> A e. DirRel )
PART 10  BASIC ALGEBRAIC STRUCTURES
10.1  Monoids
10.1.1  Magmas According to Wikipedia ("Magma (algebra)", 08-Jan-2020, https://en.wikipedia.org/wiki/magma_(algebra)) "In abstract algebra, a magma [...] is a basic kind of algebraic structure. Specifically, a magma consists of a set equipped with a single binary operation. The binary operation must be closed by definition but no other properties are imposed.". Since the concept of a "binary operation" is used in different variants, these differences are explained in more detail in the following: With df-mpt2 6201, binary operations are defined by a rule, and with df-ov 6199, the value of a binary operation applied to two operands can be expressed. In both cases, the two operands can belong to different sets, and the result can be an element of a third set. However, according to Wikipedia "Binary operation", see https://en.wikipedia.org/wiki/Binary_operation (19-Jan-2020), "... a binary operation on a set S is a mapping of the elements of the Cartesian product S X. S to S: f : ( S X. S --> S ). Because the result of performing the operation on a pair of elements of S is again an element of S, the operation is called a closed binary operation on S (or sometimes expressed as having the property of closure).". To distinguish this more restrictive definition (in Wikipedia and most of the literature) from the general case, binary operations mapping the elements of the Cartesian product S X. S are more precisely called internal binary operations. If, in addition, the result is also contained in the set S, the operation should be called closed internal binary operation. Therefore, a "binary operation on a set S" according to Wikipedia is a "closed internal binary operation" in a more precise terminology. If the sets are different, the operation is explicitly called external binary operation (see Wikipedia https://en.wikipedia.org/wiki/Binary_operation#External_binary_operations ). The definition of magmas (Mgm, see df-mgm 15989) concentrates on the closure property of the associated operation, and poses no additional restrictions on it. In this way, it is most general and flexible.
Syntax	cplusf 15986	Extend class notation with group addition as a function.
class +f
Syntax	cmgm 15987	Extend class notation with class of all magmas.
class Mgm
Definition	df-plusf 15988*	Define group addition function. Usually we will use +g directly instead of +f, and they have the same behavior in most cases. The main advantage of +f for any magma is that it is a guaranteed function (mgmplusf 15998), while +g only has closure (mgmcl 15992). (Contributed by Mario Carneiro, 14-Aug-2015.)
|- +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
Definition	df-mgm 15989*	A magma is a set equipped with an everywhere defined internal operation. Definition 1 in [BourbakiAlg1] p. 1, or definition of a groupoid in section I.1 of [Bruck] p. 1. Note: The term "groupoid" is now widely used to refer to other objects: (small) categories all of whose morphisms are invertible, or groups with a partial function replacing the binary operation. Therefore, we will only use the term "magma" for the present notion in set.mm. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
Theorem	ismgm 15990*	The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( M e. V -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) )
Theorem	ismgmn0 15991*	The predicate "is a magma" for a structure with a nonempty base set. (Contributed by AV, 29-Jan-2020.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( A e. B -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) )
Theorem	mgmcl 15992	Closure of the operation of a magma. (Contributed by FL, 14-Sep-2010.) (Revised by AV, 13-Jan-2020.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( ( M e. Mgm /\ X e. B /\ Y e. B ) -> ( X .o. Y ) e. B )
Theorem	isnmgm 15993	A condition for a structure not to be a magma. (Contributed by AV, 30-Jan-2020.) (Proof shortened by NM, 5-Feb-2020.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( ( X e. B /\ Y e. B /\ ( X .o. Y ) e/ B ) -> M e/ Mgm )
Theorem	plusffval 15994*	The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( +f ` G )   =>    |- .+^ = ( x e. B , y e. B |-> ( x .+ y ) )
Theorem	plusfval 15995	The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( +f ` G )   =>    |- ( ( X e. B /\ Y e. B ) -> ( X .+^ Y ) = ( X .+ Y ) )
Theorem	plusfeq 15996	If the addition operation is already a function, the functionalization of it is equal to the original operation. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( +f ` G )   =>    |- ( .+ Fn ( B X. B ) -> .+^ = .+ )
Theorem	plusffn 15997	The group addition operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.)
|- B = ( Base ` G )   &    |- .+^ = ( +f ` G )   =>    |- .+^ Fn ( B X. B )
Theorem	mgmplusf 15998	The group addition function of a magma is a function into its base set. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revisd by AV, 28-Jan-2020.)
|- B = ( Base ` M )   &    |- .+^ = ( +f ` M )   =>    |- ( M e. Mgm -> .+^ : ( B X. B ) --> B )
Theorem	intopsn 15999	The internal operation for a set is the trivial operation iff the set is a singleton. Formerly part of proof of ring1zr 18036. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 23-Jan-2020.)
|- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( B = { Z } <-> .o. = { <. <. Z , Z >. , Z >. } ) )
Theorem	mgmb1mgm1 16000	The only magma with a base set consisting of one element is the trivial magma (at least if its operation is an internal binary operation). (Contributed by AV, 23-Jan-2020.) (Revised by AV, 7-Feb-2020.)
|- B = ( Base ` M )   &    |- .+ = ( +g ` M )   =>    |- ( ( M e. Mgm /\ Z e. B /\ .+ Fn ( B X. B ) ) -> ( B = { Z } <-> .+ = { <. <. Z , Z >. , Z >. } ) )