P. 163 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16201-16300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hofpropd 16201	If two categories have the same set of objects, morphisms, and compositions, then they have the same Hom functor. (Contributed by Mario Carneiro, 26-Jan-2017.)
|- ( ph -> ( Hom f ` C ) = ( Hom f ` D ) )   &    |- ( ph -> (compf ` C ) = (compf ` D ) )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   =>    |- ( ph -> (HomF ` C ) = (HomF ` D ) )
Theorem	yonpropd 16202	If two categories have the same set of objects, morphisms, and compositions, then they have the same Yoneda functor. (Contributed by Mario Carneiro, 26-Jan-2017.)
|- ( ph -> ( Hom f ` C ) = ( Hom f ` D ) )   &    |- ( ph -> (compf ` C ) = (compf ` D ) )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   =>    |- ( ph -> (Yon ` C ) = (Yon ` D ) )
Theorem	oppcyon 16203	Value of the opposite Yoneda embedding. (Contributed by Mario Carneiro, 26-Jan-2017.)
|- O = (oppCat ` C )   &    |- Y = (Yon ` O )   &    |- M = (HomF ` C )   &    |- ( ph -> C e. Cat )   =>    |- ( ph -> Y = ( <. O , C >. curryF M ) )
Theorem	oyoncl 16204	The opposite Yoneda embedding is a functor from oppCat ` C to the functor category C -> SetCat. (Contributed by Mario Carneiro, 26-Jan-2017.)
|- O = (oppCat ` C )   &    |- Y = (Yon ` O )   &    |- ( ph -> C e. Cat )   &    |- S = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   &    |- Q = ( C FuncCat S )   =>    |- ( ph -> Y e. ( O Func Q ) )
Theorem	oyon1cl 16205	The opposite Yoneda embedding at an object of C is a functor from C to Set, also known as the covariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.)
|- O = (oppCat ` C )   &    |- Y = (Yon ` O )   &    |- ( ph -> C e. Cat )   &    |- S = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   &    |- B = ( Base ` C )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( ( 1st ` Y ) ` X ) e. ( C Func S ) )
Theorem	yonedalem1 16206	Lemma for yoneda 16217. (Contributed by Mario Carneiro, 28-Jan-2017.)
|- Y = (Yon ` C )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- O = (oppCat ` C )   &    |- S = ( SetCat ` U )   &    |- T = ( SetCat ` V )   &    |- Q = ( O FuncCat S )   &    |- H = (HomF ` Q )   &    |- R = ( ( Q X.c O ) FuncCat T )   &    |- E = ( O evalF S )   &    |- Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ⟨,⟩F ( Q 1stF O ) ) )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> V e. W )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   &    |- ( ph -> ( ran ( Hom f ` Q ) u. U ) C_ V )   =>    |- ( ph -> ( Z e. ( ( Q X.c O ) Func T ) /\ E e. ( ( Q X.c O ) Func T ) ) )
Theorem	yonedalem21 16207	Lemma for yoneda 16217. (Contributed by Mario Carneiro, 28-Jan-2017.)
|- Y = (Yon ` C )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- O = (oppCat ` C )   &    |- S = ( SetCat ` U )   &    |- T = ( SetCat ` V )   &    |- Q = ( O FuncCat S )   &    |- H = (HomF ` Q )   &    |- R = ( ( Q X.c O ) FuncCat T )   &    |- E = ( O evalF S )   &    |- Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ⟨,⟩F ( Q 1stF O ) ) )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> V e. W )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   &    |- ( ph -> ( ran ( Hom f ` Q ) u. U ) C_ V )   &    |- ( ph -> F e. ( O Func S ) )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( F ( 1st ` Z ) X ) = ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) )
Theorem	yonedalem3a 16208*	Lemma for yoneda 16217. (Contributed by Mario Carneiro, 29-Jan-2017.)
|- Y = (Yon ` C )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- O = (oppCat ` C )   &    |- S = ( SetCat ` U )   &    |- T = ( SetCat ` V )   &    |- Q = ( O FuncCat S )   &    |- H = (HomF ` Q )   &    |- R = ( ( Q X.c O ) FuncCat T )   &    |- E = ( O evalF S )   &    |- Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ⟨,⟩F ( Q 1stF O ) ) )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> V e. W )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   &    |- ( ph -> ( ran ( Hom f ` Q ) u. U ) C_ V )   &    |- ( ph -> F e. ( O Func S ) )   &    |- ( ph -> X e. B )   &    |- M = ( f e. ( O Func S ) , x e. B |-> ( a e. ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) |-> ( ( a ` x ) ` ( .1. ` x ) ) ) )   =>    |- ( ph -> ( ( F M X ) = ( a e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) |-> ( ( a ` X ) ` ( .1. ` X ) ) ) /\ ( F M X ) : ( F ( 1st ` Z ) X ) --> ( F ( 1st ` E ) X ) ) )
Theorem	yonedalem4a 16209*	Lemma for yoneda 16217. (Contributed by Mario Carneiro, 29-Jan-2017.)
|- Y = (Yon ` C )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- O = (oppCat ` C )   &    |- S = ( SetCat ` U )   &    |- T = ( SetCat ` V )   &    |- Q = ( O FuncCat S )   &    |- H = (HomF ` Q )   &    |- R = ( ( Q X.c O ) FuncCat T )   &    |- E = ( O evalF S )   &    |- Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ⟨,⟩F ( Q 1stF O ) ) )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> V e. W )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   &    |- ( ph -> ( ran ( Hom f ` Q ) u. U ) C_ V )   &    |- ( ph -> F e. ( O Func S ) )   &    |- ( ph -> X e. B )   &    |- N = ( f e. ( O Func S ) , x e. B |-> ( u e. ( ( 1st ` f ) ` x ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) x ) |-> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) ) ) ) )   &    |- ( ph -> A e. ( ( 1st ` F ) ` X ) )   =>    |- ( ph -> ( ( F N X ) ` A ) = ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) ) )
Theorem	yonedalem4b 16210*	Lemma for yoneda 16217. (Contributed by Mario Carneiro, 29-Jan-2017.)
|- Y = (Yon ` C )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- O = (oppCat ` C )   &    |- S = ( SetCat ` U )   &    |- T = ( SetCat ` V )   &    |- Q = ( O FuncCat S )   &    |- H = (HomF ` Q )   &    |- R = ( ( Q X.c O ) FuncCat T )   &    |- E = ( O evalF S )   &    |- Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ⟨,⟩F ( Q 1stF O ) ) )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> V e. W )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   &    |- ( ph -> ( ran ( Hom f ` Q ) u. U ) C_ V )   &    |- ( ph -> F e. ( O Func S ) )   &    |- ( ph -> X e. B )   &    |- N = ( f e. ( O Func S ) , x e. B |-> ( u e. ( ( 1st ` f ) ` x ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) x ) |-> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) ) ) ) )   &    |- ( ph -> A e. ( ( 1st ` F ) ` X ) )   &    |- ( ph -> P e. B )   &    |- ( ph -> G e. ( P ( Hom ` C ) X ) )   =>    |- ( ph -> ( ( ( ( F N X ) ` A ) ` P ) ` G ) = ( ( ( X ( 2nd ` F ) P ) ` G ) ` A ) )
Theorem	yonedalem4c 16211*	Lemma for yoneda 16217. (Contributed by Mario Carneiro, 29-Jan-2017.)
|- Y = (Yon ` C )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- O = (oppCat ` C )   &    |- S = ( SetCat ` U )   &    |- T = ( SetCat ` V )   &    |- Q = ( O FuncCat S )   &    |- H = (HomF ` Q )   &    |- R = ( ( Q X.c O ) FuncCat T )   &    |- E = ( O evalF S )   &    |- Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ⟨,⟩F ( Q 1stF O ) ) )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> V e. W )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   &    |- ( ph -> ( ran ( Hom f ` Q ) u. U ) C_ V )   &    |- ( ph -> F e. ( O Func S ) )   &    |- ( ph -> X e. B )   &    |- N = ( f e. ( O Func S ) , x e. B |-> ( u e. ( ( 1st ` f ) ` x ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) x ) |-> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) ) ) ) )   &    |- ( ph -> A e. ( ( 1st ` F ) ` X ) )   =>    |- ( ph -> ( ( F N X ) ` A ) e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) )
Theorem	yonedalem22 16212	Lemma for yoneda 16217. (Contributed by Mario Carneiro, 29-Jan-2017.)
|- Y = (Yon ` C )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- O = (oppCat ` C )   &    |- S = ( SetCat ` U )   &    |- T = ( SetCat ` V )   &    |- Q = ( O FuncCat S )   &    |- H = (HomF ` Q )   &    |- R = ( ( Q X.c O ) FuncCat T )   &    |- E = ( O evalF S )   &    |- Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ⟨,⟩F ( Q 1stF O ) ) )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> V e. W )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   &    |- ( ph -> ( ran ( Hom f ` Q ) u. U ) C_ V )   &    |- ( ph -> F e. ( O Func S ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> G e. ( O Func S ) )   &    |- ( ph -> P e. B )   &    |- ( ph -> A e. ( F ( O Nat S ) G ) )   &    |- ( ph -> K e. ( P ( Hom ` C ) X ) )   =>    |- ( ph -> ( A ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) K ) = ( ( ( P ( 2nd ` Y ) X ) ` K ) ( <. ( ( 1st ` Y ) ` X ) , F >. ( 2nd ` H ) <. ( ( 1st ` Y ) ` P ) , G >. ) A ) )
Theorem	yonedalem3b 16213*	Lemma for yoneda 16217. (Contributed by Mario Carneiro, 29-Jan-2017.)
|- Y = (Yon ` C )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- O = (oppCat ` C )   &    |- S = ( SetCat ` U )   &    |- T = ( SetCat ` V )   &    |- Q = ( O FuncCat S )   &    |- H = (HomF ` Q )   &    |- R = ( ( Q X.c O ) FuncCat T )   &    |- E = ( O evalF S )   &    |- Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ⟨,⟩F ( Q 1stF O ) ) )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> V e. W )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   &    |- ( ph -> ( ran ( Hom f ` Q ) u. U ) C_ V )   &    |- ( ph -> F e. ( O Func S ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> G e. ( O Func S ) )   &    |- ( ph -> P e. B )   &    |- ( ph -> A e. ( F ( O Nat S ) G ) )   &    |- ( ph -> K e. ( P ( Hom ` C ) X ) )   &    |- M = ( f e. ( O Func S ) , x e. B |-> ( a e. ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) |-> ( ( a ` x ) ` ( .1. ` x ) ) ) )   =>    |- ( ph -> ( ( G M P ) ( <. ( F ( 1st ` Z ) X ) , ( G ( 1st ` Z ) P ) >. (comp ` T ) ( G ( 1st ` E ) P ) ) ( A ( <. F , X >. ( 2nd ` Z ) <. G , P >. ) K ) ) = ( ( A ( <. F , X >. ( 2nd ` E ) <. G , P >. ) K ) ( <. ( F ( 1st ` Z ) X ) , ( F ( 1st ` E ) X ) >. (comp ` T ) ( G ( 1st ` E ) P ) ) ( F M X ) ) )
Theorem	yonedalem3 16214*	Lemma for yoneda 16217. (Contributed by Mario Carneiro, 28-Jan-2017.)
|- Y = (Yon ` C )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- O = (oppCat ` C )   &    |- S = ( SetCat ` U )   &    |- T = ( SetCat ` V )   &    |- Q = ( O FuncCat S )   &    |- H = (HomF ` Q )   &    |- R = ( ( Q X.c O ) FuncCat T )   &    |- E = ( O evalF S )   &    |- Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ⟨,⟩F ( Q 1stF O ) ) )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> V e. W )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   &    |- ( ph -> ( ran ( Hom f ` Q ) u. U ) C_ V )   &    |- M = ( f e. ( O Func S ) , x e. B |-> ( a e. ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) |-> ( ( a ` x ) ` ( .1. ` x ) ) ) )   =>    |- ( ph -> M e. ( Z ( ( Q X.c O ) Nat T ) E ) )
Theorem	yonedainv 16215*	The Yoneda Lemma with explicit inverse. (Contributed by Mario Carneiro, 29-Jan-2017.)
|- Y = (Yon ` C )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- O = (oppCat ` C )   &    |- S = ( SetCat ` U )   &    |- T = ( SetCat ` V )   &    |- Q = ( O FuncCat S )   &    |- H = (HomF ` Q )   &    |- R = ( ( Q X.c O ) FuncCat T )   &    |- E = ( O evalF S )   &    |- Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ⟨,⟩F ( Q 1stF O ) ) )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> V e. W )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   &    |- ( ph -> ( ran ( Hom f ` Q ) u. U ) C_ V )   &    |- M = ( f e. ( O Func S ) , x e. B |-> ( a e. ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) |-> ( ( a ` x ) ` ( .1. ` x ) ) ) )   &    |- I = (Inv ` R )   &    |- N = ( f e. ( O Func S ) , x e. B |-> ( u e. ( ( 1st ` f ) ` x ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) x ) |-> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) ) ) ) )   =>    |- ( ph -> M ( Z I E ) N )
Theorem	yonffthlem 16216*	Lemma for yonffth 16218. (Contributed by Mario Carneiro, 29-Jan-2017.)
|- Y = (Yon ` C )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- O = (oppCat ` C )   &    |- S = ( SetCat ` U )   &    |- T = ( SetCat ` V )   &    |- Q = ( O FuncCat S )   &    |- H = (HomF ` Q )   &    |- R = ( ( Q X.c O ) FuncCat T )   &    |- E = ( O evalF S )   &    |- Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ⟨,⟩F ( Q 1stF O ) ) )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> V e. W )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   &    |- ( ph -> ( ran ( Hom f ` Q ) u. U ) C_ V )   &    |- M = ( f e. ( O Func S ) , x e. B |-> ( a e. ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) |-> ( ( a ` x ) ` ( .1. ` x ) ) ) )   &    |- I = (Inv ` R )   &    |- N = ( f e. ( O Func S ) , x e. B |-> ( u e. ( ( 1st ` f ) ` x ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) x ) |-> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) ) ) ) )   =>    |- ( ph -> Y e. ( ( C Full Q ) i^i ( C Faith Q ) ) )
Theorem	yoneda 16217*	The Yoneda Lemma. There is a natural isomorphism between the functors Z and E, where Z ( F , X ) is the natural transformations from Yon ( X ) = Hom ( - , X ) to F, and E ( F , X ) = F ( X ) is the evaluation functor. Here we need two universes to state the claim: the smaller universe U is used for forming the functor category Q = C op -> SetCat ( U ), which itself does not (necessarily) live in U but instead is an element of the larger universe V. (If U is a Grothendieck universe, then it will be closed under this "presheaf" operation, and so we can set U = V in this case.) (Contributed by Mario Carneiro, 29-Jan-2017.)
|- Y = (Yon ` C )   &    |- B = ( Base ` C )   &    |- .1. = ( Id ` C )   &    |- O = (oppCat ` C )   &    |- S = ( SetCat ` U )   &    |- T = ( SetCat ` V )   &    |- Q = ( O FuncCat S )   &    |- H = (HomF ` Q )   &    |- R = ( ( Q X.c O ) FuncCat T )   &    |- E = ( O evalF S )   &    |- Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ⟨,⟩F ( Q 1stF O ) ) )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> V e. W )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   &    |- ( ph -> ( ran ( Hom f ` Q ) u. U ) C_ V )   &    |- M = ( f e. ( O Func S ) , x e. B |-> ( a e. ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) |-> ( ( a ` x ) ` ( .1. ` x ) ) ) )   &    |- I = ( Iso ` R )   =>    |- ( ph -> M e. ( Z I E ) )
Theorem	yonffth 16218	The Yoneda Lemma. The Yoneda embedding, the curried Hom functor, is full and faithful, and hence is a representation of the category C as a full subcategory of the category Q of presheaves on C. (Contributed by Mario Carneiro, 29-Jan-2017.)
|- Y = (Yon ` C )   &    |- O = (oppCat ` C )   &    |- S = ( SetCat ` U )   &    |- Q = ( O FuncCat S )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> U e. V )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   =>    |- ( ph -> Y e. ( ( C Full Q ) i^i ( C Faith Q ) ) )
Theorem	yoniso 16219*	If the codomain is recoverable from a hom-set, then the Yoneda embedding is injective on objects, and hence is an isomorphism from C into a full subcategory of a presheaf category. (Contributed by Mario Carneiro, 30-Jan-2017.)
|- Y = (Yon ` C )   &    |- O = (oppCat ` C )   &    |- S = ( SetCat ` U )   &    |- D = (CatCat ` V )   &    |- B = ( Base ` D )   &    |- I = ( Iso ` D )   &    |- Q = ( O FuncCat S )   &    |- E = ( Q ↾s ran ( 1st ` Y ) )   &    |- ( ph -> V e. X )   &    |- ( ph -> C e. B )   &    |- ( ph -> U e. W )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   &    |- ( ph -> E e. B )   &    |- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( F ` ( x ( Hom ` C ) y ) ) = y )   =>    |- ( ph -> Y e. ( C I E ) )
PART 9  BASIC ORDER THEORY
9.1  Presets and directed sets using extensible structures
Syntax	cpreset 16220	Extend class notation with the class of all presets.
class Preset
Syntax	cdrs 16221	Extend class notation with the class of all directed sets.
class Dirset
Definition	df-preset 16222*	Define the class of preordered sets (presets). A preset is a set equipped with a transitive and reflexive relation. Preorders are a natural generalization of order for sets where there is a well-defined ordering, but it in some sense "fails to capture the whole story", in that there may be pairs of elements which are indistinguishable under the order. Two elements which are not equal but are less-or-equal to each other behave the same under all order operations and may be thought of as "tied". A preorder can naturally be strengthened by requiring that there are no ties, resulting in a partial order, or by stating that all comparable pairs of elements are tied, resulting in an equivalence relation. Every preorder naturally factors into these two types; the tied relation on a preorder is an equivalence relation and the quotient under that relation is a partial order. (Contributed by FL, 17-Nov-2014.) (Revised by Stefan O'Rear, 31-Jan-2015.)
|- Preset = { f | [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r z ) -> x r z ) ) }
Definition	df-drs 16223*	Define the class of directed sets. A directed set is a nonempty preordered set where every pair of elements have some upper bound. Note that it is not required that there exist a least upper bound. There is no consensus in the literature over whether directed sets are allowed to be empty. It is slightly more convenient for us if they are not. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- Dirset = { f e. Preset | [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. ( b =/= (/) /\ A. x e. b A. y e. b E. z e. b ( x r z /\ y r z ) ) }
Theorem	isprs 16224*	Property of being a preordered set. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   =>    |- ( K e. Preset <-> ( K e. _V /\ A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) )
Theorem	prslem 16225	Lemma for prsref 16226 and prstr 16227. (Contributed by Mario Carneiro, 1-Feb-2015.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   =>    |- ( ( K e. Preset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ X /\ ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) ) )
Theorem	prsref 16226	Less-or-equal is reflexive in a preset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   =>    |- ( ( K e. Preset /\ X e. B ) -> X .<_ X )
Theorem	prstr 16227	Less-or-equal is transitive in a preset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   =>    |- ( ( K e. Preset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Y /\ Y .<_ Z ) ) -> X .<_ Z )
Theorem	isdrs 16228*	Property of being a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   =>    |- ( K e. Dirset <-> ( K e. Preset /\ B =/= (/) /\ A. x e. B A. y e. B E. z e. B ( x .<_ z /\ y .<_ z ) ) )
Theorem	drsdir 16229*	Direction of a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   =>    |- ( ( K e. Dirset /\ X e. B /\ Y e. B ) -> E. z e. B ( X .<_ z /\ Y .<_ z ) )
Theorem	drsprs 16230	A directed set is a preset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- ( K e. Dirset -> K e. Preset )
Theorem	drsbn0 16231	The base of a directed set is not empty. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- B = ( Base ` K )   =>    |- ( K e. Dirset -> B =/= (/) )
Theorem	drsdirfi 16232*	Any finite number of elements in a directed set have a common upper bound. Here is where the non-emptiness constraint in df-drs 16223 first comes into play; without it we would need an additional constraint that X not be empty. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   =>    |- ( ( K e. Dirset /\ X C_ B /\ X e. Fin ) -> E. y e. B A. z e. X z .<_ y )
Theorem	isdrs2 16233*	Directed sets may be defined in terms of finite subsets. Again, without nonemptiness we would need to restrict to nonempty subsets here. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   =>    |- ( K e. Dirset <-> ( K e. Preset /\ A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) )
9.2  Posets and lattices using extensible structures
9.2.1  Posets
Syntax	cpo 16234	Extend class notation with the class of posets.
class Poset
Syntax	cplt 16235	Extend class notation with less-than for posets.
class lt
Syntax	club 16236	Extend class notation with poset least upper bound.
class lub
Syntax	cglb 16237	Extend class notation with poset greatest lower bound.
class glb
Syntax	cjn 16238	Extend class notation with poset join.
class join
Syntax	cmee 16239	Extend class notation with poset meet.
class meet
Definition	df-poset 16240*	Define the class of partially ordered sets (posets). A poset is a set equipped with a partial order, that is, a binary relation which is reflexive, antisymmetric, and transitive. Unlike a total order, in a partial order there may be pairs of elements where neither precedes the other. Definition of poset in [Crawley] p. 1. Note that Crawley-Dilworth require that a poset base set be nonempty, but we follow the convention of most authors who don't make this a requirement. In our formalism of extensible structures, the base set of a poset f is denoted by ( Base ` f ) and its partial order by ( le ` f ) (for "less than or equal to"). The quantifiers E. b E. r provide a notational shorthand to allow us to refer to the base and ordering relation as b and r in the definition rather than having to repeat ( Base ` f ) and ( le ` f ) throughout. These quantifiers can be eliminated with ceqsex2v 3099 and related theorems. (Contributed by NM, 18-Oct-2012.)
|- Poset = { f | E. b E. r ( b = ( Base ` f ) /\ r = ( le ` f ) /\ A. x e. b A. y e. b A. z e. b ( x r x /\ ( ( x r y /\ y r x ) -> x = y ) /\ ( ( x r y /\ y r z ) -> x r z ) ) ) }
Theorem	ispos 16241*	The predicate "is a poset." (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 4-Nov-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   =>    |- ( K e. Poset <-> ( K e. _V /\ A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) )
Theorem	ispos2 16242*	A poset is an antisymmetric preset. EDITORIAL: could become the definition of poset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   =>    |- ( K e. Poset <-> ( K e. Preset /\ A. x e. B A. y e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) )
Theorem	posprs 16243	A poset is a preset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- ( K e. Poset -> K e. Preset )
Theorem	posi 16244	Lemma for poset properties. (Contributed by NM, 11-Sep-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   =>    |- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ X /\ ( ( X .<_ Y /\ Y .<_ X ) -> X = Y ) /\ ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) ) )
Theorem	posref 16245	A poset ordering is reflexive. (Contributed by NM, 11-Sep-2011.) (Proof shortened by OpenAI, 25-Mar-2020.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   =>    |- ( ( K e. Poset /\ X e. B ) -> X .<_ X )
Theorem	posrefOLD 16246	A poset ordering is reflexive. (Contributed by NM, 11-Sep-2011.) Obsolete version of posref 16245 as of 25-Mar-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   =>    |- ( ( K e. Poset /\ X e. B ) -> X .<_ X )
Theorem	posasymb 16247	A poset ordering is asymmetric. (Contributed by NM, 21-Oct-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   =>    |- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( ( X .<_ Y /\ Y .<_ X ) <-> X = Y ) )
Theorem	postr 16248	A poset ordering is transitive. (Contributed by NM, 11-Sep-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   =>    |- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .<_ Y /\ Y .<_ Z ) -> X .<_ Z ) )
Theorem	0pos 16249	Technical lemma to simplify the statement of ipopos 16455. The empty set is (rather pathologically) a poset under our definitions, since it has an empty base set (str0 15210) and any relation partially orders an empty set. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- (/) e. Poset
Theorem	isposd 16250*	Properties that determine a poset (implicit structure version). (Contributed by Mario Carneiro, 29-Apr-2014.)
|- ( ph -> K e. _V )   &    |- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> .<_ = ( le ` K ) )   &    |- ( ( ph /\ x e. B ) -> x .<_ x )   &    |- ( ( ph /\ x e. B /\ y e. B ) -> ( ( x .<_ y /\ y .<_ x ) -> x = y ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) )   =>    |- ( ph -> K e. Poset )
Theorem	isposi 16251*	Properties that determine a poset (implicit structure version). (Contributed by NM, 11-Sep-2011.)
|- K e. _V   &    |- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- ( x e. B -> x .<_ x )   &    |- ( ( x e. B /\ y e. B ) -> ( ( x .<_ y /\ y .<_ x ) -> x = y ) )   &    |- ( ( x e. B /\ y e. B /\ z e. B ) -> ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) )   =>    |- K e. Poset
Theorem	isposix 16252*	Properties that determine a poset (explicit structure version). Note that the numeric indices of the structure components are not mentioned explicitly in either the theorem or its proof. (Contributed by NM, 9-Nov-2012.)
|- B e. _V   &    |- .<_ e. _V   &    |- K = { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , .<_ >. }   &    |- ( x e. B -> x .<_ x )   &    |- ( ( x e. B /\ y e. B ) -> ( ( x .<_ y /\ y .<_ x ) -> x = y ) )   &    |- ( ( x e. B /\ y e. B /\ z e. B ) -> ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) )   =>    |- K e. Poset
Definition	df-plt 16253	Define less-than ordering for posets and related structures. Unlike df-base 15175 and df-ple 15259, this is a derived component extractor and not an extensible structure component extractor that defines the poset. (Contributed by NM, 12-Oct-2011.) (Revised by Mario Carneiro, 8-Feb-2015.)
|- lt = ( p e. _V |-> ( ( le ` p ) \ _I ) )
Theorem	pltfval 16254	Value of the less-than relation. (Contributed by Mario Carneiro, 8-Feb-2015.)
|- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   =>    |- ( K e. A -> .< = ( .<_ \ _I ) )
Theorem	pltval 16255	Less-than relation. (df-pss 3432 analog.) (Contributed by NM, 12-Oct-2011.)
|- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   =>    |- ( ( K e. A /\ X e. B /\ Y e. C ) -> ( X .< Y <-> ( X .<_ Y /\ X =/= Y ) ) )
Theorem	pltle 16256	Less-than implies less-than-or-equal. (pssss 3540 analog.) (Contributed by NM, 4-Dec-2011.)
|- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   =>    |- ( ( K e. A /\ X e. B /\ Y e. C ) -> ( X .< Y -> X .<_ Y ) )
Theorem	pltne 16257	Less-than relation. (df-pss 3432 analog.) (Contributed by NM, 2-Dec-2011.)
|- .< = ( lt ` K )   =>    |- ( ( K e. A /\ X e. B /\ Y e. C ) -> ( X .< Y -> X =/= Y ) )
Theorem	pltirr 16258	The less-than relation is not reflexive. (pssirr 3545 analog.) (Contributed by NM, 7-Feb-2012.)
|- .< = ( lt ` K )   =>    |- ( ( K e. A /\ X e. B ) -> -. X .< X )
Theorem	pleval2i 16259	One direction of pleval2 16260. (Contributed by Mario Carneiro, 8-Feb-2015.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   =>    |- ( ( X e. B /\ Y e. B ) -> ( X .<_ Y -> ( X .< Y \/ X = Y ) ) )
Theorem	pleval2 16260	Less-than-or-equal in terms of less-than. (sspss 3544 analog.) (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 8-Feb-2015.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   =>    |- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( X .< Y \/ X = Y ) ) )
Theorem	pltnle 16261	Less-than implies not inverse less-than-or-equal. (Contributed by NM, 18-Oct-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   =>    |- ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X .< Y ) -> -. Y .<_ X )
Theorem	pltval3 16262	Alternate expression for less-than relation. (dfpss3 3531 analog.) (Contributed by NM, 4-Nov-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   =>    |- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( X .< Y <-> ( X .<_ Y /\ -. Y .<_ X ) ) )
Theorem	pltnlt 16263	The less-than relation implies the negation of its inverse. (Contributed by NM, 18-Oct-2011.)
|- B = ( Base ` K )   &    |- .< = ( lt ` K )   =>    |- ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X .< Y ) -> -. Y .< X )
Theorem	pltn2lp 16264	The less-than relation has no 2-cycle loops. (pssn2lp 3546 analog.) (Contributed by NM, 2-Dec-2011.)
|- B = ( Base ` K )   &    |- .< = ( lt ` K )   =>    |- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> -. ( X .< Y /\ Y .< X ) )
Theorem	plttr 16265	The less-than relation is transitive. (psstr 3549 analog.) (Contributed by NM, 2-Dec-2011.)
|- B = ( Base ` K )   &    |- .< = ( lt ` K )   =>    |- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .< Y /\ Y .< Z ) -> X .< Z ) )
Theorem	pltletr 16266	Transitive law for chained less-than and less-than-or-equal. (psssstr 3551 analog.) (Contributed by NM, 2-Dec-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   =>    |- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .< Y /\ Y .<_ Z ) -> X .< Z ) )
Theorem	plelttr 16267	Transitive law for chained less-than-or-equal and less-than. (sspsstr 3550 analog.) (Contributed by NM, 2-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   =>    |- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .<_ Y /\ Y .< Z ) -> X .< Z ) )
Theorem	pospo 16268	Write a poset structure in terms of the proper-class poset predicate (strict less than version). (Contributed by Mario Carneiro, 8-Feb-2015.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   =>    |- ( K e. V -> ( K e. Poset <-> ( .< Po B /\ ( _I |` B ) C_ .<_ ) ) )
Definition	df-lub 16269*	Define the least upper bound (LUB) of a set of (poset) elements. The domain is restricted to exclude sets s for which the LUB doesn't exist uniquely. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 6-Sep-2018.)
|- lub = ( p e. _V |-> ( ( s e. ~P ( Base ` p ) |-> ( iota_ x e. ( Base ` p ) ( A. y e. s y ( le ` p ) x /\ A. z e. ( Base ` p ) ( A. y e. s y ( le ` p ) z -> x ( le ` p ) z ) ) ) ) |` { s | E! x e. ( Base ` p ) ( A. y e. s y ( le ` p ) x /\ A. z e. ( Base ` p ) ( A. y e. s y ( le ` p ) z -> x ( le ` p ) z ) ) } ) )
Definition	df-glb 16270*	Define the greatest lower bound (GLB) of a set of (poset) elements. The domain is restricted to exclude sets s for which the GLB doesn't exist uniquely. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 6-Sep-2018.)
|- glb = ( p e. _V |-> ( ( s e. ~P ( Base ` p ) |-> ( iota_ x e. ( Base ` p ) ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) ) ) ) |` { s | E! x e. ( Base ` p ) ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) ) } ) )
Definition	df-join 16271*	Define poset join. (Contributed by NM, 12-Sep-2011.) (Revised by Mario Carneiro, 3-Nov-2015.)
|- join = ( p e. _V |-> { <. <. x , y >. , z >. | { x , y } ( lub ` p ) z } )
Definition	df-meet 16272*	Define poset join. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 8-Sep-2018.)
|- meet = ( p e. _V |-> { <. <. x , y >. , z >. | { x , y } ( glb ` p ) z } )
Theorem	lubfval 16273*	Value of the least upper bound function of a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 6-Sep-2018.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- U = ( lub ` K )   &    |- ( ps <-> ( A. y e. s y .<_ x /\ A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) ) )   &    |- ( ph -> K e. V )   =>    |- ( ph -> U = ( ( s e. ~P B |-> ( iota_ x e. B ps ) ) |` { s | E! x e. B ps } ) )
Theorem	lubdm 16274*	Domain of the least upper bound function of a poset. (Contributed by NM, 6-Sep-2018.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- U = ( lub ` K )   &    |- ( ps <-> ( A. y e. s y .<_ x /\ A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) ) )   &    |- ( ph -> K e. V )   =>    |- ( ph -> dom U = { s e. ~P B | E! x e. B ps } )
Theorem	lubfun 16275	The LUB is a function. (Contributed by NM, 9-Sep-2018.)
|- U = ( lub ` K )   =>    |- Fun U
Theorem	lubeldm 16276*	Member of the domain of the least upper bound function of a poset. (Contributed by NM, 7-Sep-2018.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- U = ( lub ` K )   &    |- ( ps <-> ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) )   &    |- ( ph -> K e. V )   =>    |- ( ph -> ( S e. dom U <-> ( S C_ B /\ E! x e. B ps ) ) )
Theorem	lubelss 16277	A member of the domain of the least upper bound function is a subset of the base set. (Contributed by NM, 7-Sep-2018.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- U = ( lub ` K )   &    |- ( ph -> K e. V )   &    |- ( ph -> S e. dom U )   =>    |- ( ph -> S C_ B )
Theorem	lubeu 16278*	Unique existence proper of a member of the domain of the least upper bound function of a poset. (Contributed by NM, 7-Sep-2018.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- U = ( lub ` K )   &    |- ( ps <-> ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) )   &    |- ( ph -> K e. V )   &    |- ( ph -> S e. dom U )   =>    |- ( ph -> E! x e. B ps )
Theorem	lubval 16279*	Value of the least upper bound function of a poset. Out-of-domain arguments (those not satisfying S e. dom U) are allowed for convenience, evaluating to the empty set. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- U = ( lub ` K )   &    |- ( ps <-> ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) )   &    |- ( ph -> K e. V )   &    |- ( ph -> S C_ B )   =>    |- ( ph -> ( U ` S ) = ( iota_ x e. B ps ) )
Theorem	lubcl 16280	The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018.)
|- B = ( Base ` K )   &    |- U = ( lub ` K )   &    |- ( ph -> K e. V )   &    |- ( ph -> S e. dom U )   =>    |- ( ph -> ( U ` S ) e. B )
Theorem	lubprop 16281*	Properties of greatest lower bound of a poset. (Contributed by NM, 22-Oct-2011.) (Revised by NM, 7-Sep-2018.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- U = ( lub ` K )   &    |- ( ph -> K e. V )   &    |- ( ph -> S e. dom U )   =>    |- ( ph -> ( A. y e. S y .<_ ( U ` S ) /\ A. z e. B ( A. y e. S y .<_ z -> ( U ` S ) .<_ z ) ) )
Theorem	luble 16282	The greatest lower bound is the least element. (Contributed by NM, 22-Oct-2011.) (Revised by NM, 7-Sep-2018.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- U = ( lub ` K )   &    |- ( ph -> K e. V )   &    |- ( ph -> S e. dom U )   &    |- ( ph -> X e. S )   =>    |- ( ph -> X .<_ ( U ` S ) )
Theorem	lublecllem 16283*	Lemma for lublecl 16284 and lubid 16285. (Contributed by NM, 8-Sep-2018.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- U = ( lub ` K )   &    |- ( ph -> K e. Poset )   &    |- ( ph -> X e. B )   =>    |- ( ( ph /\ x e. B ) -> ( ( A. z e. { y e. B | y .<_ X } z .<_ x /\ A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) ) <-> x = X ) )
Theorem	lublecl 16284*	The set of all elements less than a given element has an LUB. (Contributed by NM, 8-Sep-2018.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- U = ( lub ` K )   &    |- ( ph -> K e. Poset )   &    |- ( ph -> X e. B )   =>    |- ( ph -> { y e. B | y .<_ X } e. dom U )
Theorem	lubid 16285*	The LUB of elements less than or equal to a fixed value equals that value. (Contributed by NM, 19-Oct-2011.) (Revised by NM, 7-Sep-2018.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- U = ( lub ` K )   &    |- ( ph -> K e. Poset )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( U ` { y e. B | y .<_ X } ) = X )
Theorem	glbfval 16286*	Value of the greatest lower function of a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 6-Sep-2018.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- G = ( glb ` K )   &    |- ( ps <-> ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) )   &    |- ( ph -> K e. V )   =>    |- ( ph -> G = ( ( s e. ~P B |-> ( iota_ x e. B ps ) ) |` { s | E! x e. B ps } ) )
Theorem	glbdm 16287*	Domain of the greatest lower bound function of a poset. (Contributed by NM, 6-Sep-2018.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- G = ( glb ` K )   &    |- ( ps <-> ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) )   &    |- ( ph -> K e. V )   =>    |- ( ph -> dom G = { s e. ~P B | E! x e. B ps } )
Theorem	glbfun 16288	The GLB is a function. (Contributed by NM, 9-Sep-2018.)
|- G = ( glb ` K )   =>    |- Fun G
Theorem	glbeldm 16289*	Member of the domain of the greatest lower bound function of a poset. (Contributed by NM, 7-Sep-2018.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- G = ( glb ` K )   &    |- ( ps <-> ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) )   &    |- ( ph -> K e. V )   =>    |- ( ph -> ( S e. dom G <-> ( S C_ B /\ E! x e. B ps ) ) )
Theorem	glbelss 16290	A member of the domain of the greatest lower bound function is a subset of the base set. (Contributed by NM, 7-Sep-2018.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- G = ( glb ` K )   &    |- ( ph -> K e. V )   &    |- ( ph -> S e. dom G )   =>    |- ( ph -> S C_ B )
Theorem	glbeu 16291*	Unique existence proper of a member of the domain of the greatest lower bound function of a poset. (Contributed by NM, 7-Sep-2018.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- G = ( glb ` K )   &    |- ( ps <-> ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) )   &    |- ( ph -> K e. V )   &    |- ( ph -> S e. dom G )   =>    |- ( ph -> E! x e. B ps )
Theorem	glbval 16292*	Value of the greatest lower bound function of a poset. Out-of-domain arguments (those not satisfying S e. dom U) are allowed for convenience, evaluating to the empty set on both sides of the equality. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- G = ( glb ` K )   &    |- ( ps <-> ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) )   &    |- ( ph -> K e. V )   &    |- ( ph -> S C_ B )   =>    |- ( ph -> ( G ` S ) = ( iota_ x e. B ps ) )
Theorem	glbcl 16293	The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018.)
|- B = ( Base ` K )   &    |- G = ( glb ` K )   &    |- ( ph -> K e. V )   &    |- ( ph -> S e. dom G )   =>    |- ( ph -> ( G ` S ) e. B )
Theorem	glbprop 16294*	Properties of greatest lower bound of a poset. (Contributed by NM, 7-Sep-2018.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- U = ( glb ` K )   &    |- ( ph -> K e. V )   &    |- ( ph -> S e. dom U )   =>    |- ( ph -> ( A. y e. S ( U ` S ) .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ ( U ` S ) ) ) )
Theorem	glble 16295	The greatest lower bound is the least element. (Contributed by NM, 22-Oct-2011.) (Revised by NM, 7-Sep-2018.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- U = ( glb ` K )   &    |- ( ph -> K e. V )   &    |- ( ph -> S e. dom U )   &    |- ( ph -> X e. S )   =>    |- ( ph -> ( U ` S ) .<_ X )
Theorem	joinfval 16296*	Value of join function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) TODO: prove joinfval2 16297 first to reduce net proof size (existence part)?
|- U = ( lub ` K )   &    |- .\/ = ( join ` K )   =>    |- ( K e. V -> .\/ = { <. <. x , y >. , z >. | { x , y } U z } )
Theorem	joinfval2 16297*	Value of join function for a poset-type structure. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.)
|- U = ( lub ` K )   &    |- .\/ = ( join ` K )   =>    |- ( K e. V -> .\/ = { <. <. x , y >. , z >. | ( { x , y } e. dom U /\ z = ( U ` { x , y } ) ) } )
Theorem	joindm 16298*	Domain of join function for a poset-type structure. (Contributed by NM, 16-Sep-2018.)
|- U = ( lub ` K )   &    |- .\/ = ( join ` K )   =>    |- ( K e. V -> dom .\/ = { <. x , y >. | { x , y } e. dom U } )
Theorem	joindef 16299	Two ways to say that a join is defined. (Contributed by NM, 9-Sep-2018.)
|- U = ( lub ` K )   &    |- .\/ = ( join ` K )   &    |- ( ph -> K e. V )   &    |- ( ph -> X e. W )   &    |- ( ph -> Y e. Z )   =>    |- ( ph -> ( <. X , Y >. e. dom .\/ <-> { X , Y } e. dom U ) )
Theorem	joinval 16300	Join value. Since both sides evaluate to (/) when they don't exist, for convenience we drop the { X , Y } e. dom U requirement. (Contributed by NM, 9-Sep-2018.)
|- U = ( lub ` K )   &    |- .\/ = ( join ` K )   &    |- ( ph -> K e. V )   &    |- ( ph -> X e. W )   &    |- ( ph -> Y e. Z )   =>    |- ( ph -> ( X .\/ Y ) = ( U ` { X , Y } ) )