---

Step * 2 of Lemma poset-functor_wf


1. J : Cname List
2. K : Cname List
3. f : name-morph(J;K)
4. ∀x:name-morph(K;[]). ((λx.Ax) = (λx.Ax) ∈ (∀x@0:nameset(J). (↑(f o x) x@0 ≤z (f o x) x@0)))
5. x : name-morph(K;[])
6. y : name-morph(K;[])
7. z : name-morph(K;[])
8. f@0 : ∀x@0:nameset(K). (↑x x@0 ≤z y x@0)
9. g : ∀x:nameset(K). (↑y x ≤z z x)
10. x1 : nameset(J)
⊢ ((f o x) x1) ≤ ((f o z) x1)
BY
{ (RepUR ``name-comp uext`` 0
   THEN (BoolCase ⌜isname(f x1)⌝⋅ THENA Auto)
   THEN (FLemma `assert-isname` [-1] ORELSE FLemma `not-assert-isname` [-1])
   THEN Auto) }

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

---

Latex:

---

Latex:

1.  J  :  Cname  List
2.  K  :  Cname  List
3.  f  :  name-morph(J;K)
4.  \mforall{}x:name-morph(K;[]).  ((\mlambda{}x.Ax)  =  (\mlambda{}x.Ax))
5.  x  :  name-morph(K;[])
6.  y  :  name-morph(K;[])
7.  z  :  name-morph(K;[])
8.  f@0  :  \mforall{}x@0:nameset(K).  (\muparrow{}x  x@0  \mleq{}z  y  x@0)
9.  g  :  \mforall{}x:nameset(K).  (\muparrow{}y  x  \mleq{}z  z  x)
10.  x1  :  nameset(J)
\mvdash{}  ((f  o  x)  x1)  \mleq{}  ((f  o  z)  x1)


By

---

Latex:
(RepUR  ``name-comp  uext``  0
  THEN  (BoolCase  \mkleeneopen{}isname(f  x1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (FLemma  `assert-isname`  [-1]  ORELSE  FLemma  `not-assert-isname`  [-1])
  THEN  Auto)

---

Home Index