---

Step * of Lemma subset-I_set

No Annotations
∀[C:SmallCategory]. ∀[X,Y:ps_context{j:l}(C)].  ∀I:cat-ob(C). (Y(I) ⊆r X(I)) supposing sub_ps_context{j:l}(C; Y; X)
BY
{ (Auto
   THEN Unfold `subtype_rel` 0
   THEN Unfold `sub_ps_context` -2
   THEN (MemTypeHD (-2) THENA Auto)
   THEN Thin (-2)
   THEN Fold `member` (-2)) }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. Y : ps_context{j:l}(C)
4. 1(Y) ∈ A:cat-ob(op-cat(C)) ⟶ (cat-arrow(type-cat{j':l}) (Y A) (X A))
5. I : cat-ob(C)
⊢ λx.x ∈ Y(I) ⟶ X(I)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X,Y:ps\_context\{j:l\}(C)].
    \mforall{}I:cat-ob(C).  (Y(I)  \msubseteq{}r  X(I))  supposing  sub\_ps\_context\{j:l\}(C;  Y;  X)


By

---

Latex:
(Auto
  THEN  Unfold  `subtype\_rel`  0
  THEN  Unfold  `sub\_ps\_context`  -2
  THEN  (MemTypeHD  (-2)  THENA  Auto)
  THEN  Thin  (-2)
  THEN  Fold  `member`  (-2))

---

Home Index