---

Step * 2 of Lemma poset-cat_wf

.....set predicate..... 
1. J : Cname List
⊢ let ob,arrow,id,comp = <name-morph(J;[]), λf,g. ∀x:nameset(J). (↑f x ≤z g x), λf,x. Ax, λf,g,h,p,q,x. Ax> 
  in (∀x,y:ob. ∀f:arrow x y.  (((comp x x y (id x) f) = f ∈ (arrow x y)) ∧ ((comp x y y f (id y)) = f ∈ (arrow x y))))
     ∧ (∀x,y,z,w:ob. ∀f:arrow x y. ∀g:arrow y z. ∀h:arrow z w.
          ((comp x z w (comp x y z f g) h) = (comp x y w f (comp y z w g h)) ∈ (arrow x w)))  
BY
{ (Reduce 0 THEN Auto) }

1
1. J : Cname List
2. x : name-morph(J;[])
3. y : name-morph(J;[])
4. f : ∀x@0:nameset(J). (↑x x@0 ≤z y x@0)
⊢ (λx.Ax) = f ∈ (∀x@0:nameset(J). (↑x x@0 ≤z y x@0))

2
1. J : Cname List
2. ∀x,y:name-morph(J;[]). ∀f:∀x@0:nameset(J). (↑x x@0 ≤z y x@0).
     (((λx.Ax) = f ∈ (∀x@0:nameset(J). (↑x x@0 ≤z y x@0))) ∧ ((λx.Ax) = f ∈ (∀x@0:nameset(J). (↑x x@0 ≤z y x@0))))
3. x : name-morph(J;[])
4. y : name-morph(J;[])
5. z : name-morph(J;[])
6. w : name-morph(J;[])
7. f : ∀x@0:nameset(J). (↑x x@0 ≤z y x@0)
8. g : ∀x:nameset(J). (↑y x ≤z z x)
9. h : ∀x:nameset(J). (↑z x ≤z w x)
10. x1 : nameset(J)
⊢ (x x1) ≤ (w x1)

---

Latex:

---

Latex:
.....set  predicate..... 
1.  J  :  Cname  List
\mvdash{}  let  ob,arrow,id,comp  =  <name-morph(J;[]),  \mlambda{}f,g.  \mforall{}x:nameset(J).  (\muparrow{}f  x  \mleq{}z  g  x),  \mlambda{}f,x.  Ax,  \mlambda{}f,g,h,p,q\000C,x.  Ax> 
    in  (\mforall{}x,y:ob.  \mforall{}f:arrow  x  y.    (((comp  x  x  y  (id  x)  f)  =  f)  \mwedge{}  ((comp  x  y  y  f  (id  y))  =  f)))
          \mwedge{}  (\mforall{}x,y,z,w:ob.  \mforall{}f:arrow  x  y.  \mforall{}g:arrow  y  z.  \mforall{}h:arrow  z  w.
                    ((comp  x  z  w  (comp  x  y  z  f  g)  h)  =  (comp  x  y  w  f  (comp  y  z  w  g  h))))   


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index