P. 158 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 15701-15800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	latmlej21 15701	Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   =>    |- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y ./\ X ) .<_ ( X .\/ Z ) )
Theorem	latmlej22 15702	Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   =>    |- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y ./\ X ) .<_ ( Z .\/ X ) )
Theorem	lubsn 15703	The least upper bound of a singleton. (chsupsn 26309 analog.) (Contributed by NM, 20-Oct-2011.)
|- B = ( Base ` K )   &    |- U = ( lub ` K )   =>    |- ( ( K e. Lat /\ X e. B ) -> ( U ` { X } ) = X )
Theorem	latjass 15704	Lattice join is associative. Lemma 2.2 in [MegPav2002] p. 362. (chjass 26429 analog.) (Contributed by NM, 17-Sep-2011.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   =>    |- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .\/ Y ) .\/ Z ) = ( X .\/ ( Y .\/ Z ) ) )
Theorem	latj12 15705	Swap 1st and 2nd members of lattice join. (chj12 26430 analog.) (Contributed by NM, 4-Jun-2012.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   =>    |- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .\/ ( Y .\/ Z ) ) = ( Y .\/ ( X .\/ Z ) ) )
Theorem	latj32 15706	Swap 2nd and 3rd members of lattice join. Lemma 2.2 in [MegPav2002] p. 362. (Contributed by NM, 2-Dec-2011.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   =>    |- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .\/ Y ) .\/ Z ) = ( ( X .\/ Z ) .\/ Y ) )
Theorem	latj13 15707	Swap 1st and 3rd members of lattice join. (Contributed by NM, 4-Jun-2012.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   =>    |- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .\/ ( Y .\/ Z ) ) = ( Z .\/ ( Y .\/ X ) ) )
Theorem	latj31 15708	Swap 2nd and 3rd members of lattice join. Lemma 2.2 in [MegPav2002] p. 362. (Contributed by NM, 23-Jun-2012.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   =>    |- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .\/ Y ) .\/ Z ) = ( ( Z .\/ Y ) .\/ X ) )
Theorem	latjrot 15709	Rotate lattice join of 3 classes. (Contributed by NM, 23-Jul-2012.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   =>    |- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .\/ Y ) .\/ Z ) = ( ( Z .\/ X ) .\/ Y ) )
Theorem	latj4 15710	Rearrangement of lattice join of 4 classes. (chj4 26431 analog.) (Contributed by NM, 14-Jun-2012.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   =>    |- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .\/ Y ) .\/ ( Z .\/ W ) ) = ( ( X .\/ Z ) .\/ ( Y .\/ W ) ) )
Theorem	latj4rot 15711	Rotate lattice join of 4 classes. (Contributed by NM, 11-Jul-2012.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   =>    |- ( ( K e. Lat /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .\/ Y ) .\/ ( Z .\/ W ) ) = ( ( W .\/ X ) .\/ ( Y .\/ Z ) ) )
Theorem	latjjdi 15712	Lattice join distributes over itself. (Contributed by NM, 30-Jul-2012.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   =>    |- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .\/ ( Y .\/ Z ) ) = ( ( X .\/ Y ) .\/ ( X .\/ Z ) ) )
Theorem	latjjdir 15713	Lattice join distributes over itself. (Contributed by NM, 2-Aug-2012.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   =>    |- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .\/ Y ) .\/ Z ) = ( ( X .\/ Z ) .\/ ( Y .\/ Z ) ) )
Theorem	mod1ile 15714	The weak direction of the modular law (e.g. pmod1i 35447, atmod1i1 35456) that holds in any lattice. (Contributed by NM, 11-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   =>    |- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ Z -> ( X .\/ ( Y ./\ Z ) ) .<_ ( ( X .\/ Y ) ./\ Z ) ) )
Theorem	mod2ile 15715	The weak direction of the modular law (e.g. pmod2iN 35448) that holds in any lattice. (Contributed by NM, 11-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   =>    |- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Z .<_ X -> ( ( X ./\ Y ) .\/ Z ) .<_ ( X ./\ ( Y .\/ Z ) ) ) )
Syntax	ccla 15716	Extend class notation with complete lattices.
class CLat
Definition	df-clat 15717	Define the class of all complete lattices, where every subset of the base set has an LUB and a GLB. (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.)
|- CLat = { p e. Poset | ( dom ( lub ` p ) = ~P ( Base ` p ) /\ dom ( glb ` p ) = ~P ( Base ` p ) ) }
Theorem	isclat 15718	The predicate "is a complete lattice." (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.)
|- B = ( Base ` K )   &    |- U = ( lub ` K )   &    |- G = ( glb ` K )   =>    |- ( K e. CLat <-> ( K e. Poset /\ ( dom U = ~P B /\ dom G = ~P B ) ) )
Theorem	clatpos 15719	A complete lattice is a poset. (Contributed by NM, 8-Sep-2018.)
|- ( K e. CLat -> K e. Poset )
Theorem	clatlem 15720	Lemma for properties of a complete lattice. (Contributed by NM, 14-Sep-2011.)
|- B = ( Base ` K )   &    |- U = ( lub ` K )   &    |- G = ( glb ` K )   =>    |- ( ( K e. CLat /\ S C_ B ) -> ( ( U ` S ) e. B /\ ( G ` S ) e. B ) )
Theorem	clatlubcl 15721	Any subset of the base set has an LUB in a complete lattice. (Contributed by NM, 14-Sep-2011.)
|- B = ( Base ` K )   &    |- U = ( lub ` K )   =>    |- ( ( K e. CLat /\ S C_ B ) -> ( U ` S ) e. B )
Theorem	clatlubcl2 15722	Any subset of the base set has an LUB in a complete lattice. (Contributed by NM, 13-Sep-2018.)
|- B = ( Base ` K )   &    |- U = ( lub ` K )   =>    |- ( ( K e. CLat /\ S C_ B ) -> S e. dom U )
Theorem	clatglbcl 15723	Any subset of the base set has a GLB in a complete lattice. (Contributed by NM, 14-Sep-2011.)
|- B = ( Base ` K )   &    |- G = ( glb ` K )   =>    |- ( ( K e. CLat /\ S C_ B ) -> ( G ` S ) e. B )
Theorem	clatglbcl2 15724	Any subset of the base set has a GLB in a complete lattice. (Contributed by NM, 13-Sep-2018.)
|- B = ( Base ` K )   &    |- G = ( glb ` K )   =>    |- ( ( K e. CLat /\ S C_ B ) -> S e. dom G )
Theorem	clatl 15725	A complete lattice is a lattice. (Contributed by NM, 18-Sep-2011.) TODO: use eqrelrdv2 5092 to shorten proof and eliminate joindmss 15616 and meetdmss 15630?
|- ( K e. CLat -> K e. Lat )
Theorem	isglbd 15726*	Properties that determine the greatest lower bound of a complete lattice. (Contributed by Mario Carneiro, 19-Mar-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- G = ( glb ` K )   &    |- ( ( ph /\ y e. S ) -> H .<_ y )   &    |- ( ( ph /\ x e. B /\ A. y e. S x .<_ y ) -> x .<_ H )   &    |- ( ph -> K e. CLat )   &    |- ( ph -> S C_ B )   &    |- ( ph -> H e. B )   =>    |- ( ph -> ( G ` S ) = H )
Theorem	lublem 15727*	Lemma for the least upper bound properties in a complete lattice. (Contributed by NM, 19-Oct-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- U = ( lub ` K )   =>    |- ( ( K e. CLat /\ S C_ B ) -> ( A. y e. S y .<_ ( U ` S ) /\ A. z e. B ( A. y e. S y .<_ z -> ( U ` S ) .<_ z ) ) )
Theorem	lubub 15728	The LUB of a complete lattice subset is an upper bound. (Contributed by NM, 19-Oct-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- U = ( lub ` K )   =>    |- ( ( K e. CLat /\ S C_ B /\ X e. S ) -> X .<_ ( U ` S ) )
Theorem	lubl 15729*	The LUB of a complete lattice subset is the least bound. (Contributed by NM, 19-Oct-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- U = ( lub ` K )   =>    |- ( ( K e. CLat /\ S C_ B /\ X e. B ) -> ( A. y e. S y .<_ X -> ( U ` S ) .<_ X ) )
Theorem	lubss 15730	Subset law for least upper bounds. (chsupss 26238 analog.) (Contributed by NM, 20-Oct-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- U = ( lub ` K )   =>    |- ( ( K e. CLat /\ T C_ B /\ S C_ T ) -> ( U ` S ) .<_ ( U ` T ) )
Theorem	lubel 15731	An element of a set is less than or equal to the least upper bound of the set. (Contributed by NM, 21-Oct-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- U = ( lub ` K )   =>    |- ( ( K e. CLat /\ X e. S /\ S C_ B ) -> X .<_ ( U ` S ) )
Theorem	lubun 15732	The LUB of a union. (Contributed by NM, 5-Mar-2012.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   &    |- U = ( lub ` K )   =>    |- ( ( K e. CLat /\ S C_ B /\ T C_ B ) -> ( U ` ( S u. T ) ) = ( ( U ` S ) .\/ ( U ` T ) ) )
Theorem	clatglb 15733*	Properties of greatest lower bound of a complete lattice. (Contributed by NM, 5-Dec-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- G = ( glb ` K )   =>    |- ( ( K e. CLat /\ S C_ B ) -> ( A. y e. S ( G ` S ) .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ ( G ` S ) ) ) )
Theorem	clatglble 15734	The greatest lower bound is the least element. (Contributed by NM, 5-Dec-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- G = ( glb ` K )   =>    |- ( ( K e. CLat /\ S C_ B /\ X e. S ) -> ( G ` S ) .<_ X )
Theorem	clatleglb 15735*	Two ways of expressing "less than or equal to the greatest lower bound." (Contributed by NM, 5-Dec-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- G = ( glb ` K )   =>    |- ( ( K e. CLat /\ X e. B /\ S C_ B ) -> ( X .<_ ( G ` S ) <-> A. y e. S X .<_ y ) )
Theorem	clatglbss 15736	Subset law for greatest lower bound. (Contributed by Mario Carneiro, 16-Apr-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- G = ( glb ` K )   =>    |- ( ( K e. CLat /\ T C_ B /\ S C_ T ) -> ( G ` T ) .<_ ( G ` S ) )
9.2.3  The dual of an ordered set
Syntax	codu 15737	Class function defining dual orders.
class ODual
Definition	df-odu 15738	Define the dual of an ordered structure, which replaces the order component of the structure with its reverse. See odubas 15742, oduleval 15740, and oduleg 15741 for its principal properties. EDITORIAL: likely usable to simplify many lattice proofs, as it allows for duality arguments to be formalized; for instance latmass 15797. (Contributed by Stefan O'Rear, 29-Jan-2015.)
|- ODual = ( w e. _V |-> ( w sSet <. ( le ` ndx ) , `' ( le ` w ) >. ) )
Theorem	oduval 15739	Value of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.)
|- D = (ODual ` O )   &    |- .<_ = ( le ` O )   =>    |- D = ( O sSet <. ( le ` ndx ) , `' .<_ >. )
Theorem	oduleval 15740	Value of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.)
|- D = (ODual ` O )   &    |- .<_ = ( le ` O )   =>    |- `' .<_ = ( le ` D )
Theorem	oduleg 15741	Truth of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.)
|- D = (ODual ` O )   &    |- .<_ = ( le ` O )   &    |- G = ( le ` D )   =>    |- ( ( A e. V /\ B e. W ) -> ( A G B <-> B .<_ A ) )
Theorem	odubas 15742	Base set of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.)
|- D = (ODual ` O )   &    |- B = ( Base ` O )   =>    |- B = ( Base ` D )
Theorem	pospropd 15743*	Posethood is determined only by structure components and only by the value of the relation within the base set. (Contributed by Stefan O'Rear, 29-Jan-2015.)
|- ( ph -> K e. V )   &    |- ( ph -> L e. W )   &    |- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( le ` K ) y <-> x ( le ` L ) y ) )   =>    |- ( ph -> ( K e. Poset <-> L e. Poset ) )
Theorem	odupos 15744	Being a poset is a self-dual property. (Contributed by Stefan O'Rear, 29-Jan-2015.)
|- D = (ODual ` O )   =>    |- ( O e. Poset -> D e. Poset )
Theorem	oduposb 15745	Being a poset is a self-dual property. (Contributed by Stefan O'Rear, 29-Jan-2015.)
|- D = (ODual ` O )   =>    |- ( O e. V -> ( O e. Poset <-> D e. Poset ) )
Theorem	meet0 15746	Lemma for odujoin 15751. (Contributed by Stefan O'Rear, 29-Jan-2015.) Todo (df-riota 6242 update): This proof increased from 152 bytes to 547 bytes after the df-riota 6242 change. Any way to shorten it? join0 15747 also.
|- ( meet ` (/) ) = (/)
Theorem	join0 15747	Lemma for odumeet 15749. (Contributed by Stefan O'Rear, 29-Jan-2015.)
|- ( join ` (/) ) = (/)
Theorem	oduglb 15748	Greatest lower bounds in a dual order are least upper bounds in the original order. (Contributed by Stefan O'Rear, 29-Jan-2015.)
|- D = (ODual ` O )   &    |- U = ( lub ` O )   =>    |- ( O e. V -> U = ( glb ` D ) )
Theorem	odumeet 15749	Meets in a dual order are joins in the original. (Contributed by Stefan O'Rear, 29-Jan-2015.)
|- D = (ODual ` O )   &    |- .\/ = ( join ` O )   =>    |- .\/ = ( meet ` D )
Theorem	odulub 15750	Least upper bounds in a dual order are greatest lower bounds in the original order. (Contributed by Stefan O'Rear, 29-Jan-2015.)
|- D = (ODual ` O )   &    |- L = ( glb ` O )   =>    |- ( O e. V -> L = ( lub ` D ) )
Theorem	odujoin 15751	Joins in a dual order are meets in the original. (Contributed by Stefan O'Rear, 29-Jan-2015.)
|- D = (ODual ` O )   &    |- ./\ = ( meet ` O )   =>    |- ./\ = ( join ` D )
Theorem	odulatb 15752	Being a lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.)
|- D = (ODual ` O )   =>    |- ( O e. V -> ( O e. Lat <-> D e. Lat ) )
Theorem	oduclatb 15753	Being a complete lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.)
|- D = (ODual ` O )   =>    |- ( O e. CLat <-> D e. CLat )
Theorem	odulat 15754	Being a lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.)
|- D = (ODual ` O )   =>    |- ( O e. Lat -> D e. Lat )
Theorem	poslubmo 15755*	Least upper bounds in a poset are unique if they exist. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by NM, 16-Jun-2017.)
|- .<_ = ( le ` K )   &    |- B = ( Base ` K )   =>    |- ( ( K e. Poset /\ S C_ B ) -> E* x e. B ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) )
Theorem	posglbmo 15756*	Greatest lower bounds in a poset are unique if they exist. (Contributed by NM, 20-Sep-2018.)
|- .<_ = ( le ` K )   &    |- B = ( Base ` K )   =>    |- ( ( K e. Poset /\ S C_ B ) -> E* x e. B ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) )
Theorem	poslubd 15757*	Properties which determine the least upper bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- .<_ = ( le ` K )   &    |- B = ( Base ` K )   &    |- U = ( lub ` K )   &    |- ( ph -> K e. Poset )   &    |- ( ph -> S C_ B )   &    |- ( ph -> T e. B )   &    |- ( ( ph /\ x e. S ) -> x .<_ T )   &    |- ( ( ph /\ y e. B /\ A. x e. S x .<_ y ) -> T .<_ y )   =>    |- ( ph -> ( U ` S ) = T )
Theorem	poslubdg 15758*	Properties which determine the least upper bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- .<_ = ( le ` K )   &    |- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> U = ( lub ` K ) )   &    |- ( ph -> K e. Poset )   &    |- ( ph -> S C_ B )   &    |- ( ph -> T e. B )   &    |- ( ( ph /\ x e. S ) -> x .<_ T )   &    |- ( ( ph /\ y e. B /\ A. x e. S x .<_ y ) -> T .<_ y )   =>    |- ( ph -> ( U ` S ) = T )
Theorem	posglbd 15759*	Properties which determine the greatest lower bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- .<_ = ( le ` K )   &    |- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> G = ( glb ` K ) )   &    |- ( ph -> K e. Poset )   &    |- ( ph -> S C_ B )   &    |- ( ph -> T e. B )   &    |- ( ( ph /\ x e. S ) -> T .<_ x )   &    |- ( ( ph /\ y e. B /\ A. x e. S y .<_ x ) -> y .<_ T )   =>    |- ( ph -> ( G ` S ) = T )
9.2.4  Subset order structures
Syntax	cipo 15760	Class function defining inclusion posets.
class toInc
Definition	df-ipo 15761*	For any family of sets, define the poset of that family ordered by inclusion. See ipobas 15764, ipolerval 15765, and ipole 15767 for its contract. EDITORIAL: I'm not thrilled with the name. Any suggestions? (Contributed by Stefan O'Rear, 30-Jan-2015.) (New usage is discouraged.)
|- toInc = ( f e. _V |-> [_ { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) } / o ]_ ( { <. ( Base ` ndx ) , f >. , <. (TopSet ` ndx ) , (ordTop ` o ) >. } u. { <. ( le ` ndx ) , o >. , <. ( oc ` ndx ) , ( x e. f |-> U. { y e. f | ( y i^i x ) = (/) } ) >. } ) )
Theorem	ipostr 15762	The structure of df-ipo 15761 is a structure defining indexes up to 11. (Contributed by Mario Carneiro, 25-Oct-2015.)
|- ( { <. ( Base ` ndx ) , B >. , <. (TopSet ` ndx ) , J >. } u. { <. ( le ` ndx ) , .<_ >. , <. ( oc ` ndx ) , ._|_ >. } ) Struct <. 1 , ; 1 1 >.
Theorem	ipoval 15763*	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 15764	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 15765*	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 15766	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 15767	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 15768	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 15769	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 15770*	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 15771	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 15772*	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 15773	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 15774*	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 15775*	An algebraic closure system satisfies isacs3 15783. (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 15776	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 15777*	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 15778*	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 15779	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 15780	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 15781*	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 15782*	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 15783*	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 15784	In an algebraic closure system, the closure of a set is the union of the closures of its finite subsets. Deduction form of acsficl 15780. (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 15785*	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 15780. 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 15786	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 15787*	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 15785 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 15788*	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 15787 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 15019, 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 15789	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 7814 to the map given in acsmap2d 15788. 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 15790	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 15789 and then applying unirnfdomd 8945 to the map given in acsmap2d 15788. 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 15791	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 15790 twice with acsinfd 15789. 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 15792*	In an algebraic closure system whose closure operator has the exchange property, if two independent sets have equal closure, they are equinumerous. See mreexfidimd 15029 for the finite case and acsinfdimd 15791 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 15793	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 15794	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 15795	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 15796*	A Moore space is a complete lattice under inclusion. (Contributed by Stefan O'Rear, 31-Jan-2015.) TODO (df-riota 6242 update): Reprove using isclat 15718 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 15797	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 15798*	Lemma for latdisd 15799. (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 15799*	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 15800	The class of distributive lattices.
class DLat