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	curf2val 15701	Value of a component of the curry functor natural transformation. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- G = ( <. C , D >. curryF F )   &    |- A = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> F e. ( ( C X.c D ) Func E ) )   &    |- B = ( Base ` D )   &    |- H = ( Hom ` C )   &    |- I = ( Id ` D )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. A )   &    |- ( ph -> K e. ( X H Y ) )   &    |- L = ( ( X ( 2nd ` G ) Y ) ` K )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( L ` Z ) = ( K ( <. X , Z >. ( 2nd ` F ) <. Y , Z >. ) ( I ` Z ) ) )
Theorem	curf2cl 15702	The curry functor at a morphism is a natural transformation. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- G = ( <. C , D >. curryF F )   &    |- A = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> F e. ( ( C X.c D ) Func E ) )   &    |- B = ( Base ` D )   &    |- H = ( Hom ` C )   &    |- I = ( Id ` D )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. A )   &    |- ( ph -> K e. ( X H Y ) )   &    |- L = ( ( X ( 2nd ` G ) Y ) ` K )   &    |- N = ( D Nat E )   =>    |- ( ph -> L e. ( ( ( 1st ` G ) ` X ) N ( ( 1st ` G ) ` Y ) ) )
Theorem	curfcl 15703	The curry functor of a functor F : C X. D --> E is a functor curryF ( F ) : C --> ( D --> E ). (Contributed by Mario Carneiro, 13-Jan-2017.)
|- G = ( <. C , D >. curryF F )   &    |- Q = ( D FuncCat E )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> F e. ( ( C X.c D ) Func E ) )   =>    |- ( ph -> G e. ( C Func Q ) )
Theorem	curfpropd 15704	If two categories have the same set of objects, morphisms, and compositions, then they curry the same functor to the same result. (Contributed by Mario Carneiro, 26-Jan-2017.)
|- ( ph -> ( Hom f ` A ) = ( Hom f ` B ) )   &    |- ( ph -> (compf ` A ) = (compf ` B ) )   &    |- ( ph -> ( Hom f ` C ) = ( Hom f ` D ) )   &    |- ( ph -> (compf ` C ) = (compf ` D ) )   &    |- ( ph -> A e. Cat )   &    |- ( ph -> B e. Cat )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> F e. ( ( A X.c C ) Func E ) )   =>    |- ( ph -> ( <. A , C >. curryF F ) = ( <. B , D >. curryF F ) )
Theorem	uncfval 15705	Value of the uncurry functor, which is the reverse of the curry functor, taking G : C --> ( D --> E ) to uncurryF ( G ) : C X. D --> E. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- F = ( <" C D E "> uncurryF G )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> E e. Cat )   &    |- ( ph -> G e. ( C Func ( D FuncCat E ) ) )   =>    |- ( ph -> F = ( ( D evalF E ) o.func ( ( G o.func ( C 1stF D ) ) ⟨,⟩F ( C 2ndF D ) ) ) )
Theorem	uncfcl 15706	The uncurry operation takes a functor F : C --> ( D --> E ) to a functor uncurryF ( F ) : C X. D --> E. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- F = ( <" C D E "> uncurryF G )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> E e. Cat )   &    |- ( ph -> G e. ( C Func ( D FuncCat E ) ) )   =>    |- ( ph -> F e. ( ( C X.c D ) Func E ) )
Theorem	uncf1 15707	Value of the uncurry functor on an object. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- F = ( <" C D E "> uncurryF G )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> E e. Cat )   &    |- ( ph -> G e. ( C Func ( D FuncCat E ) ) )   &    |- A = ( Base ` C )   &    |- B = ( Base ` D )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X ( 1st ` F ) Y ) = ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` Y ) )
Theorem	uncf2 15708	Value of the uncurry functor on a morphism. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- F = ( <" C D E "> uncurryF G )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> E e. Cat )   &    |- ( ph -> G e. ( C Func ( D FuncCat E ) ) )   &    |- A = ( Base ` C )   &    |- B = ( Base ` D )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. B )   &    |- H = ( Hom ` C )   &    |- J = ( Hom ` D )   &    |- ( ph -> Z e. A )   &    |- ( ph -> W e. B )   &    |- ( ph -> R e. ( X H Z ) )   &    |- ( ph -> S e. ( Y J W ) )   =>    |- ( ph -> ( R ( <. X , Y >. ( 2nd ` F ) <. Z , W >. ) S ) = ( ( ( ( X ( 2nd ` G ) Z ) ` R ) ` W ) ( <. ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` Y ) , ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` W ) >. (comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` Z ) ) ` W ) ) ( ( Y ( 2nd ` ( ( 1st ` G ) ` X ) ) W ) ` S ) ) )
Theorem	curfuncf 15709	Cancellation of curry with uncurry. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- F = ( <" C D E "> uncurryF G )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> E e. Cat )   &    |- ( ph -> G e. ( C Func ( D FuncCat E ) ) )   =>    |- ( ph -> ( <. C , D >. curryF F ) = G )
Theorem	uncfcurf 15710	Cancellation of uncurry with curry. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- G = ( <. C , D >. curryF F )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> F e. ( ( C X.c D ) Func E ) )   =>    |- ( ph -> ( <" C D E "> uncurryF G ) = F )
Theorem	diagval 15711	Define the diagonal functor, which is the functor C --> ( D Func C ) whose object part is x e. C |-> ( y e. D |-> x ). We can define this equationally as the currying of the first projection functor, and by expressing it this way we get a quick proof of functoriality. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.)
|- L = ( CΔfunc D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   =>    |- ( ph -> L = ( <. C , D >. curryF ( C 1stF D ) ) )
Theorem	diagcl 15712	The diagonal functor is a functor from the base category to the functor category. Another way of saying this is that the constant functor ( y e. D |-> X ) is a construction that is natural in X (and covariant). (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.)
|- L = ( CΔfunc D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- Q = ( D FuncCat C )   =>    |- ( ph -> L e. ( C Func Q ) )
Theorem	diag1cl 15713	The constant functor of X is a functor. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.)
|- L = ( CΔfunc D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- A = ( Base ` C )   &    |- ( ph -> X e. A )   &    |- K = ( ( 1st ` L ) ` X )   =>    |- ( ph -> K e. ( D Func C ) )
Theorem	diag11 15714	Value of the constant functor at an object. (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.)
|- L = ( CΔfunc D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- A = ( Base ` C )   &    |- ( ph -> X e. A )   &    |- K = ( ( 1st ` L ) ` X )   &    |- B = ( Base ` D )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( ( 1st ` K ) ` Y ) = X )
Theorem	diag12 15715	Value of the constant functor at a morphism. (Contributed by Mario Carneiro, 6-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.)
|- L = ( CΔfunc D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- A = ( Base ` C )   &    |- ( ph -> X e. A )   &    |- K = ( ( 1st ` L ) ` X )   &    |- B = ( Base ` D )   &    |- ( ph -> Y e. B )   &    |- J = ( Hom ` D )   &    |- .1. = ( Id ` C )   &    |- ( ph -> Z e. B )   &    |- ( ph -> F e. ( Y J Z ) )   =>    |- ( ph -> ( ( Y ( 2nd ` K ) Z ) ` F ) = ( .1. ` X ) )
Theorem	diag2 15716	Value of the diagonal functor at a morphism. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- L = ( CΔfunc D )   &    |- A = ( Base ` C )   &    |- B = ( Base ` D )   &    |- H = ( Hom ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. A )   &    |- ( ph -> F e. ( X H Y ) )   =>    |- ( ph -> ( ( X ( 2nd ` L ) Y ) ` F ) = ( B X. { F } ) )
Theorem	diag2cl 15717	The diagonal functor at a morphism is a natural transformation between constant functors. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- L = ( CΔfunc D )   &    |- A = ( Base ` C )   &    |- B = ( Base ` D )   &    |- H = ( Hom ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. A )   &    |- ( ph -> F e. ( X H Y ) )   &    |- N = ( D Nat C )   =>    |- ( ph -> ( B X. { F } ) e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) )
Theorem	curf2ndf 15718	As shown in diagval 15711, the currying of the first projection is the diagonal functor. On the other hand, the currying of the second projection is x e. C |-> ( y e. D |-> y ), which is a constant functor of the identity functor at D. (Contributed by Mario Carneiro, 15-Jan-2017.)
|- Q = ( D FuncCat D )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> D e. Cat )   =>    |- ( ph -> ( <. C , D >. curryF ( C 2ndF D ) ) = ( ( 1st ` ( QΔfunc C ) ) ` (idfunc ` D ) ) )
8.4.3  Hom functor
Syntax	chof 15719	Extend class notation with the Hom functor.
class HomF
Syntax	cyon 15720	Extend class notation with the Yoneda embedding.
class Yon
Definition	df-hof 15721*	Define the Hom functor, which is a bifunctor (a functor of two arguments), contravariant in the first argument and covariant in the second, from (oppCat ` C ) X. C to SetCat, whose object part is the hom-function Hom, and with morphism part given by pre- and post-composition. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- HomF = ( c e. Cat |-> <. ( Hom f ` c ) , [_ ( Base ` c ) / b ]_ ( x e. ( b X. b ) , y e. ( b X. b ) |-> ( f e. ( ( 1st ` y ) ( Hom ` c ) ( 1st ` x ) ) , g e. ( ( 2nd ` x ) ( Hom ` c ) ( 2nd ` y ) ) |-> ( h e. ( ( Hom ` c ) ` x ) |-> ( ( g ( x (comp ` c ) ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. (comp ` c ) ( 2nd ` y ) ) f ) ) ) ) >. )
Definition	df-yon 15722	Define the Yoneda embedding, which is the currying of the (opposite) Hom functor. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- Yon = ( c e. Cat |-> ( <. c , (oppCat ` c ) >. curryF (HomF ` (oppCat ` c ) ) ) )
Theorem	hofval 15723*	Value of the Hom functor, which is a bifunctor (a functor of two arguments), contravariant in the first argument and covariant in the second, from (oppCat ` C ) X. C to SetCat, whose object part is the hom-function Hom, and with morphism part given by pre- and post-composition. (Contributed by Mario Carneiro, 15-Jan-2017.)
|- M = (HomF ` C )   &    |- ( ph -> C e. Cat )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- .x. = (comp ` C )   =>    |- ( ph -> M = <. ( Hom f ` C ) , ( x e. ( B X. B ) , y e. ( B X. B ) |-> ( f e. ( ( 1st ` y ) H ( 1st ` x ) ) , g e. ( ( 2nd ` x ) H ( 2nd ` y ) ) |-> ( h e. ( H ` x ) |-> ( ( g ( x .x. ( 2nd ` y ) ) h ) ( <. ( 1st ` y ) , ( 1st ` x ) >. .x. ( 2nd ` y ) ) f ) ) ) ) >. )
Theorem	hof1fval 15724	The object part of the Hom functor is the Hom f operation, which is just a functionalized version of Hom. That is, it is a two argument function, which maps X , Y to the set of morphisms from X to Y. (Contributed by Mario Carneiro, 15-Jan-2017.)
|- M = (HomF ` C )   &    |- ( ph -> C e. Cat )   =>    |- ( ph -> ( 1st ` M ) = ( Hom f ` C ) )
Theorem	hof1 15725	The object part of the Hom functor maps X , Y to the set of morphisms from X to Y. (Contributed by Mario Carneiro, 15-Jan-2017.)
|- M = (HomF ` C )   &    |- ( ph -> C e. Cat )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X ( 1st ` M ) Y ) = ( X H Y ) )
Theorem	hof2fval 15726*	The morphism part of the Hom functor, for morphisms <. f , g >. : <. X , Y >. --> <. Z , W >. (which since the first argument is contravariant means morphisms f : Z --> X and g : Y --> W), yields a function (a morphism of SetCat) mapping h : X --> Y to g o. h o. f : Z --> W. (Contributed by Mario Carneiro, 15-Jan-2017.)
|- M = (HomF ` C )   &    |- ( ph -> C e. Cat )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> W e. B )   &    |- .x. = (comp ` C )   =>    |- ( ph -> ( <. X , Y >. ( 2nd ` M ) <. Z , W >. ) = ( f e. ( Z H X ) , g e. ( Y H W ) |-> ( h e. ( X H Y ) |-> ( ( g ( <. X , Y >. .x. W ) h ) ( <. Z , X >. .x. W ) f ) ) ) )
Theorem	hof2val 15727*	The morphism part of the Hom functor, for morphisms <. f , g >. : <. X , Y >. --> <. Z , W >. (which since the first argument is contravariant means morphisms f : Z --> X and g : Y --> W), yields a function (a morphism of SetCat) mapping h : X --> Y to g o. h o. f : Z --> W. (Contributed by Mario Carneiro, 15-Jan-2017.)
|- M = (HomF ` C )   &    |- ( ph -> C e. Cat )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> W e. B )   &    |- .x. = (comp ` C )   &    |- ( ph -> F e. ( Z H X ) )   &    |- ( ph -> G e. ( Y H W ) )   =>    |- ( ph -> ( F ( <. X , Y >. ( 2nd ` M ) <. Z , W >. ) G ) = ( h e. ( X H Y ) |-> ( ( G ( <. X , Y >. .x. W ) h ) ( <. Z , X >. .x. W ) F ) ) )
Theorem	hof2 15728	The morphism part of the Hom functor, for morphisms <. f , g >. : <. X , Y >. --> <. Z , W >. (which since the first argument is contravariant means morphisms f : Z --> X and g : Y --> W), yields a function (a morphism of SetCat) mapping h : X --> Y to g o. h o. f : Z --> W. (Contributed by Mario Carneiro, 15-Jan-2017.)
|- M = (HomF ` C )   &    |- ( ph -> C e. Cat )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> W e. B )   &    |- .x. = (comp ` C )   &    |- ( ph -> F e. ( Z H X ) )   &    |- ( ph -> G e. ( Y H W ) )   &    |- ( ph -> K e. ( X H Y ) )   =>    |- ( ph -> ( ( F ( <. X , Y >. ( 2nd ` M ) <. Z , W >. ) G ) ` K ) = ( ( G ( <. X , Y >. .x. W ) K ) ( <. Z , X >. .x. W ) F ) )
Theorem	hofcllem 15729	Lemma for hofcl 15730. (Contributed by Mario Carneiro, 15-Jan-2017.)
|- M = (HomF ` C )   &    |- O = (oppCat ` C )   &    |- D = ( SetCat ` U )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> U e. V )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   &    |- B = ( Base ` C )   &    |- H = ( Hom ` C )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> W e. B )   &    |- ( ph -> S e. B )   &    |- ( ph -> T e. B )   &    |- ( ph -> K e. ( Z H X ) )   &    |- ( ph -> L e. ( Y H W ) )   &    |- ( ph -> P e. ( S H Z ) )   &    |- ( ph -> Q e. ( W H T ) )   =>    |- ( ph -> ( ( K ( <. S , Z >. (comp ` C ) X ) P ) ( <. X , Y >. ( 2nd ` M ) <. S , T >. ) ( Q ( <. Y , W >. (comp ` C ) T ) L ) ) = ( ( P ( <. Z , W >. ( 2nd ` M ) <. S , T >. ) Q ) ( <. ( X H Y ) , ( Z H W ) >. (comp ` D ) ( S H T ) ) ( K ( <. X , Y >. ( 2nd ` M ) <. Z , W >. ) L ) ) )
Theorem	hofcl 15730	Closure of the Hom functor. Note that the codomain is the category SetCat ` U for any universe U which contains each Hom-set. This corresponds to the assertion that C be locally small (with respect to U). (Contributed by Mario Carneiro, 15-Jan-2017.)
|- M = (HomF ` C )   &    |- O = (oppCat ` C )   &    |- D = ( SetCat ` U )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> U e. V )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   =>    |- ( ph -> M e. ( ( O X.c C ) Func D ) )
Theorem	oppchofcl 15731	Closure of the opposite Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.)
|- O = (oppCat ` C )   &    |- M = (HomF ` O )   &    |- D = ( SetCat ` U )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> U e. V )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   =>    |- ( ph -> M e. ( ( C X.c O ) Func D ) )
Theorem	yonval 15732	Value of the Yoneda embedding. (Contributed by Mario Carneiro, 17-Jan-2017.)
|- Y = (Yon ` C )   &    |- ( ph -> C e. Cat )   &    |- O = (oppCat ` C )   &    |- M = (HomF ` O )   =>    |- ( ph -> Y = ( <. C , O >. curryF M ) )
Theorem	yoncl 15733	The Yoneda embedding is a functor from the category to the category Q of presheaves on C. (Contributed by Mario Carneiro, 17-Jan-2017.)
|- Y = (Yon ` C )   &    |- ( ph -> C e. Cat )   &    |- O = (oppCat ` C )   &    |- S = ( SetCat ` U )   &    |- Q = ( O FuncCat S )   &    |- ( ph -> U e. V )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   =>    |- ( ph -> Y e. ( C Func Q ) )
Theorem	yon1cl 15734	The Yoneda embedding at an object of C is a presheaf on C, also known as the contravariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.)
|- Y = (Yon ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- O = (oppCat ` C )   &    |- S = ( SetCat ` U )   &    |- ( ph -> U e. V )   &    |- ( ph -> ran ( Hom f ` C ) C_ U )   =>    |- ( ph -> ( ( 1st ` Y ) ` X ) e. ( O Func S ) )
Theorem	yon11 15735	Value of the Yoneda embedding at an object. The partially evaluated Yoneda embedding is also the contravariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.)
|- Y = (Yon ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- H = ( Hom ` C )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` Z ) = ( Z H X ) )
Theorem	yon12 15736	Value of the Yoneda embedding at a morphism. The partially evaluated Yoneda embedding is also the contravariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017.)
|- Y = (Yon ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- H = ( Hom ` C )   &    |- ( ph -> Z e. B )   &    |- .x. = (comp ` C )   &    |- ( ph -> W e. B )   &    |- ( ph -> F e. ( W H Z ) )   &    |- ( ph -> G e. ( Z H X ) )   =>    |- ( ph -> ( ( ( Z ( 2nd ` ( ( 1st ` Y ) ` X ) ) W ) ` F ) ` G ) = ( G ( <. W , Z >. .x. X ) F ) )
Theorem	yon2 15737	Value of the Yoneda embedding at a morphism. (Contributed by Mario Carneiro, 17-Jan-2017.)
|- Y = (Yon ` C )   &    |- B = ( Base ` C )   &    |- ( ph -> C e. Cat )   &    |- ( ph -> X e. B )   &    |- H = ( Hom ` C )   &    |- ( ph -> Z e. B )   &    |- .x. = (comp ` C )   &    |- ( ph -> W e. B )   &    |- ( ph -> F e. ( X H Z ) )   &    |- ( ph -> G e. ( W H X ) )   =>    |- ( ph -> ( ( ( ( X ( 2nd ` Y ) Z ) ` F ) ` W ) ` G ) = ( F ( <. W , X >. .x. Z ) G ) )
Theorem	hofpropd 15738	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 15739	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 15740	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 15741	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 15742	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 15743	Lemma for yoneda 15754. (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 15744	Lemma for yoneda 15754. (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 15745*	Lemma for yoneda 15754. (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 15746*	Lemma for yoneda 15754. (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 15747*	Lemma for yoneda 15754. (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 15748*	Lemma for yoneda 15754. (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 15749	Lemma for yoneda 15754. (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 15750*	Lemma for yoneda 15754. (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 15751*	Lemma for yoneda 15754. (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 15752*	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 15753*	Lemma for yonffth 15755. (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 15754*	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 15755	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 15756*	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 15757	Extend class notation with the class of all presets.
class Preset
Syntax	cdrs 15758	Extend class notation with the class of all directed sets.
class Dirset
Definition	df-preset 15759*	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 15760*	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 15761*	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 15762	Lemma for prsref 15763 and prstr 15764. (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 15763	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 15764	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 15765*	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 15766*	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 15767	A directed set is a preset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- ( K e. Dirset -> K e. Preset )
Theorem	drsbn0 15768	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 15769*	Any finite number of elements in a directed set have a common upper bound. Here is where the non-emptiness constraint in df-drs 15760 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 15770*	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 15771	Extend class notation with the class of posets.
class Poset
Syntax	cplt 15772	Extend class notation with less-than for posets.
class lt
Syntax	club 15773	Extend class notation with poset least upper bound.
class lub
Syntax	cglb 15774	Extend class notation with poset greatest lower bound.
class glb
Syntax	cjn 15775	Extend class notation with poset join.
class join
Syntax	cmee 15776	Extend class notation with poset meet.
class meet
Definition	df-poset 15777*	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 3145 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 15778*	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 15779*	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 15780	A poset is a preset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- ( K e. Poset -> K e. Preset )
Theorem	posi 15781	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 15782	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 15783	A poset ordering is reflexive. (Contributed by NM, 11-Sep-2011.) Obsolete version of posref 15782 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 15784	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 15785	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 15786	Technical lemma to simplify the statement of ipopos 15992. The empty set is (rather pathologically) a poset under our definitions, since it has an empty base set (str0 14759) and any relation partially orders an empty set. (Contributed by Stefan O'Rear, 30-Jan-2015.)
|- (/) e. Poset
Theorem	isposd 15787*	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 15788*	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 15789*	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 15790	Define less-than ordering for posets and related structures. Unlike df-base 14724 and df-ple 14807, 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 15791	Value of the less-than relation. (Contributed by Mario Carneiro, 8-Feb-2015.)
|- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   =>    |- ( K e. A -> .< = ( .<_ \ _I ) )
Theorem	pltval 15792	Less-than relation. (df-pss 3477 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 15793	Less-than implies less-than-or-equal. (pssss 3585 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 15794	Less-than relation. (df-pss 3477 analog.) (Contributed by NM, 2-Dec-2011.)
|- .< = ( lt ` K )   =>    |- ( ( K e. A /\ X e. B /\ Y e. C ) -> ( X .< Y -> X =/= Y ) )
Theorem	pltirr 15795	The less-than relation is not reflexive. (pssirr 3590 analog.) (Contributed by NM, 7-Feb-2012.)
|- .< = ( lt ` K )   =>    |- ( ( K e. A /\ X e. B ) -> -. X .< X )
Theorem	pleval2i 15796	One direction of pleval2 15797. (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 15797	Less-than-or-equal in terms of less-than. (sspss 3589 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 15798	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 15799	Alternate expression for less-than relation. (dfpss3 3576 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 15800	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 )